Vytautas Astrauskas

> Actually, it turns out that the snap encoding is not needed after all! Instead of these 2 statements: > > ``` > inhale (let _LET_4 == (old[l8](_33)) in (...

> > Wait… Is the only difference between the examples `_1` being replaced with `old[l8](_1)` via `_LET_4`? > > Yup, that's the only change. I suspect that the `exhale/inhale acc(Array$3$usize(_1),...

> Full relevant code section without `LET`: > > ``` > // [mir] _1[_33] = move _32 > label l8 > exhale acc(Array$3$usize(_1), write) > inhale acc(Array$3$usize(_1), write) > inhale...

> > `old[l8](_1)` inside the trigger looks very suspicious to me: triggers are syntactic rules, so it is possible that the quantifier is not triggered because of that unnecessary old....

> > _1 is not havocked because there is no assignment to it and that is why I am confused. > > Apologies :) For better context about what I...

I looked into the Viper encoding for a bit, but I, unfortunately, do not see what is going wrong here. Coming back to: > Would it be desirable to implement...

This sounds more and more like a bug in the Viper backend. However, the examples are way too large to ask the backend developers to look into. Would be nice...

> > Would be nice to get a repro on a 20 or so lines example. > > I'll see if I can whip up something during the weekend :)...

> > I'll see if I can whip up something during the weekend :) > > This is the smallest version I could come up with: [lib.rs_prusti_example::foo 20220228 small.vpr.txt](https://github.com/viperproject/prusti-dev/files/8151574/lib.rs_prusti_example.foo.20220228.small.vpr.txt) >...

Thanks! This code is likely to be rewritten during the refactoring, but I think it would be still worth trying to figure out how to actually do it.