Federico Poli

Closing as duplicate of #1149. This issue should now be fixed on master.

Thanks for the report. Crashing is surely a bug. Instead of `old(self).counters[id]` you should use `old(self.counters[id])`, because you want to evaluate `self.counters[id]` in the old state, and not just `self`....

Is the `temp` file there by mistake?

From a quick look the issue is with the closure `|c| c == &params.letter` – closures are not well supported. Prusti should at least report an "unsupported feature" error message...

The error message is now ``` error: [Prusti: unsupported feature] higher-ranked lifetimes and types are not supported --> program.rs:7:12 | 7 | return params.password.chars().filter(|c| c == &params.letter).count(); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ```...

@JonasAlaif feel free to do whatever you want with this PR :)

Thanks for the report! One more minimized example: ```rust use prusti_contracts::*; pub struct T; impl T { #[trusted] #[pure] fn get(&self) -> &T { unimplemented!(); } } pub fn test(m:...

> Is it the case that the dereference operator winds up being represented as a pure function (either through rustc desugaring or in some internal representation in Prusti)? No, the...

Thanks for the report. The Viper encoding of `ParialEq`'s `eq` and `ne` pure functions, in particular the part that restores the permissions of expiring borrows, is incorrect. The MIR code...

The tuple that I'm referring to is `_13` in block 6 of the MIR of `PartialEq::eq`. Block 6: ``` _14 = &(*_1) _15 = &(*_2) _13 = (move _14, move...