Pointerbender

Cool! I'll set the flag to globally enabled by default and selectively disable it for the regression test for this Github issue and #729 (together with a FIXME for when...

I created PR #1008 to fix the bug from this issue, but perhaps it's best to leave this issue open until the regression test also passes under the new encoder...

Thanks for the suggested work-around, that works nicely :) The only change I had to make was: ```rust #[pure] pub const fn len(&self) -> usize { self.inner.len() } #[pure] #[ensures(forall(|i:...

I have another variation of the example program that fails verification with a similar Viper error message `Assert might fail. Assertion m_invariant__$TY$__Snap$struct$m_A$$bool$(snap$__$TY$__struct$m_A$Snap$struct$m_A(_old$pre$0)) might not hold. (lib.rs_A::[email protected])` ```rust pub struct A...

I get the same error in Prusti as you describe (I was already on that commit luckily :smile: ). However, I hope I'm understanding correctly what Prusti expects in terms...

That's a great suggestion, I'll give that a try, thanks!

Sorry to report back so soon :sweat_smile: This simplified program (signatures adjusted, moved out of `impl A`): ```rust #[pure] #[requires(index < inner.len())] pub fn is_valid(inner: &[usize; 4], index: usize) ->...

The suggested minimal example gives a different error for me (`internal error: entered unreachable code: Tuple([])`, the one from #298). An even more minimal example which triggers `assertion failed: perm_amount.is_valid_for_specs()`...

Created #734 :) Thanks!

> I gave a better look at this bug. It's not exactly an instance of #364. It turns out that the fold-unfold algorithm generates the correct expression, but then the...