Federico Poli

> Would it be helpful if I add the failing example program to `verify_partial` as a regression test for when the snapshot encoding is updated? Yes, thanks. Since we decided...

I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the `fix_quantifiers`...

Could you try updating Prusti? With `Prusti version: commit 53f8dc4 2021-10-27 16:11:40 UTC, built on 2021-10-27 16:18:35 UTC` I don't get that error, and I recently fixed a bunch of...

> I get the same error in Prusti as you describe (I was already on that commit luckily ). However, I hope I'm understanding correctly what Prusti expects in terms...

Mmm, the latest error seems to be a bug in the encoding of the expiration of shared references. Maybe shared references of slice types are handled incorrectly. It's definitely a...

Minimal example: ```rust use prusti_contracts::*; #[pure] #[trusted] pub fn foo(inner: &[usize; 4]) {} #[pure] pub fn bar(inner: &[usize; 4]) -> bool { foo(inner); foo(inner); true } #[trusted] fn main() {}...

> Shall I also create a new Github issue for this one? Yes, thanks! (I didn't get that error because I was on #732, good point.)

The program in the first message now panics: ``` thread 'rustc' panicked at 'not yet implemented', prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs:34:5 ```

The easiest thing in my opinion is that the hash used for caching should also include the positions, instead of ignoring them.

The `line` and `column` fields of `Position` do not affect Prusti's error reporting. They are just there to help debugging some internal errors. (I personally never benefit from them and...