Vytautas Astrauskas

Consider the following example: ```rust struct A { f: i32 } #[trusted] #[pure] fn get(a: &A) -> i32 { unimplemented!{} } fn do_something(x: &A) { } fn test(a: A) {...

Prusti assumes that everything reachable from a shared reference is immutable as long as that reference is alive. This assumption holds for any code that does not use `UnsafeCell` and...

Pure functions are not allowed to mutate observable state, so we should forbid `old` in the postconditions of pure functions.

> (This would typically manifest itself as seeing the Viper method verify correctly, but then when its inserted as a Viper function in the Viper program for another method, then...

> > This bug should be fixed once we fully migrate to manual axiomatization of functions. > > Ah, thanks! Is this also part of the refactoring or is this...

> Would it be acceptable to put the new encoder behind a configuration flag for now? Yes, as long as it is enabled when running the tests (to avoid introducing...

This looks like a bug. Since `T` is `Copy`, this should work.

A workaround seems to be to extend the lifetime of one of the borrows so that they do not expire at the same time: ```rust use prusti_contracts::*; pub struct Tree...

@Pointerbender FYI: This should be fixed in my refactoring (by completely getting rid of the problematic code). However, I am currently blocked waiting for @Aurel300 to finish his refactoring…

> @vakaras just in case, in the upcoming refactoring, were the only removed optimizations in the `fix_quantifiers` pass, or will other optimizations also be affected? The reason I'm asking is...