Pointerbender

> 3. Disallow calling `ne` Even though option 1 was chosen, I'm just commenting here to leave a use case as a data point on why having a `ne` method...

> @Pointerbender: thanks for the info. If I've understood correctly you are saying there are cases where hand-writing both `eq` and `ne` is useful? If so, that's presumably an argument...

By the way, will this functionality also work for items that are both in `core` and `std`? For example, the method `core::mem::swap` is also re-exported as `std::mem::swap` by the standard...

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 ( forall i: Int ::...

> 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), write)` statements in...

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 (forall i: Int :: { lookup_pure__$TY$__Array$3$usize$usize$(old[l8](_1), i) }...

> Is this the original code? No, I have some local changes to Prusti that generates that version (and verifies). The original statements (as currently generated from the `master` branch...

> _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 mean by "havoc",...

In case it helps, this small hand-crafted example which does not use `old[l8](_1)` in the trigger verifies okay: ``` method example() { var _1: Ref var _33: Int _1 :=...

> > My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier. > > I'd also compare the change randomizing the Z3 seeds: >...