Federico Poli

An even simpler example: ```rust use prusti_contracts::*; struct NonCopy(u32); #[trusted] fn non_copy_tuple() -> (NonCopy, NonCopy) { unimplemented!() } #[trusted] fn consume(x: NonCopy) { unimplemented!() } fn main() { let mut...

I don't think this is an issue with the fold-unfold algorithm. The permissions to be used in the loop invariants are computed in a separate module. > The permissions computed...

Thanks for noticing that! I opened https://github.com/viperproject/viper-ide/issues/281, but in the meantime it makes sense to avoid the `$` in Prusti.

Viper fixed this

This is interesting. It seems that the CFG of `increment` that we get from the compiler shouldn't borrow-check. In block `0` the shared reference `_8` is created out of the...

Workaround: ```rust #[ensures(self.counters.lookup(id) == old(self.counters.lookup(id)) + 1)] pub fn increment(&mut self, id: usize) { let x = self.counters.lookup(id); self.counters.modify(id, x + 1); } ```

Thanks! The correct error message should be something like "loops are not allowed in pure functions". Usually you can convert the loop to some recursive call, which is supported.

Could you attach the `.dot` dump of the MIR of `cursor_invariant`? The definition is quite big and I wonder what its CFG looks like.

You could also give a try at some memory profiling tool, like [`heaptrack`](https://github.com/KDE/heaptrack), just to confirm whether there are gigabytes of `vir::Expr` instances. That tool should (hopefully) work out of...

The relevant comment is here :) https://github.com/viperproject/prusti-dev/blob/f8e70f9037b964498e83f58a3bb9387f60c7a454/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs#L54-L56 The encoding of pure expressions currently generates an expression whose size is proportional to the number of paths in the CFG, which means...