Pointerbender

Thanks for the heads up! In that case I'll just apply a temporary hack on my local version of Prusti to disable moving out the `unfolding`s :)

@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 because...

> 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 > ``` For now this panic can be worked...

I'm not sure how feasible this would be, but it might be preferably to hash a relative position (and translate the relative position back to an absolute position for any...

> In other words, the postconditions > > ``` > ensures result ensures 0 ensures result ``` > > should become something like > > ``` > ensures [result ensures...

I've got two more examples related to this issue: ```rust use prusti_contracts::*; #[requires(test(1).a == 1)] fn main() {} #[derive(Clone, Copy)] pub struct A { a: usize } #[pure] #[requires(a A...

I also observed `selection_sort.rs` failing spuriously in the wild on Mac OS X when fetching the latest changes on `master` from upstream to my fork of `prusti-dev`. [This particular commit](https://github.com/Pointerbender/prusti-dev/commit/14a436f9efa93918d82453f0fa1b060912109770)...

I have a running theory of what might be happening: I think the `fix_quantifiers` and/or the `optimize_folding` passes might be altering the user-specified quantifiers in a way that makes it...

In that case I think the best way forward to fix this performance issue is to add triggers to the test case once #812 is resolved and @vakaras' refactorings land....

With PR #876 the `selection_sort.rs` was sped up a little further, but when playing around with quantifier triggers I discovered that code like this doesn't work fully yet: ```rust while...