Internal error for postcondition that uses blocked self

[fpoli]

Prusti reports an internal error ("generating fold-unfold Viper statements failed") when verifying the following program.

The reason is that a postcondition tries to use self while it's blocked by a mutable reference that is returned. The correct way is to write the postcondition using a pledge, but the error message is not helpful.

use std::marker::PhantomData;
use prusti_contracts::*;

pub struct Foo<T>(PhantomData<T>);

impl<T> Foo<T> {
    #[pure]
    #[trusted]
    pub fn len(&self) -> usize {
        unimplemented!()
    }

    #[trusted]
    pub fn get_mut_baz(&mut self, idx: usize) -> &mut T {
        unimplemented!()
    }

    #[ensures(self.len() == old(self.len()) - 1)] // Incorrect
    pub fn get_mut_bar(&mut self, idx: usize) -> &mut T {
        self.get_mut_baz(idx)
    }
}

fn main() {}

[fpoli]

Smaller example:

use prusti_contracts::*;

#[ensures(value === value)]
pub fn get_mut(
    value: &mut i32
) -> &mut i32 {
    value
}

[Prusti internal error] Prusti encountered an unexpected internal error
...
Details: cannot generate fold-unfold Viper statements. The required permission Acc(old[pre](_1.val_ref).val_int, read) cannot be obtained.