Pointerbender

> type invariants, is something we used to support in Prusti. The syntax would be `#[invariant(...)]` attached to the `struct`. However, this was broken (by the recent compiler upgrade I...

I've also noticed this when pressing CTRL+C when running a `cargo_verify` test case: ```shell ./x.py test -p prusti-tests --test cargotest ``` This leaves `prusti-driver` instances running in the background.

> Is this easily reproducible for you? If so, maybe you could post some more information about it. It takes a few steps, but I think I was able to...

Thank you for the pointers! I ran the example in different configurations to see what's in the `*.smt2` files. For all runs I used the following basic `Prusti.toml` configuration: ```toml...

Fun additional detail, when I comment out the lines related to calling `.len()` on an array inside `pub fn invariant()`, its Viper pure function body shrinks to a mere 488...

> You should be able to set them in Prusti.toml Nice! I'll give this a try. Although my guess would be that the default parameters would suffice once the encoding...

> Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix. > ``` > forall i: Int :: 0 lookup_pure__$TY$__Array$64$usize$$int$$$int$(_9.val_ref,...

> It looks good to me :+1: Thanks! > I've noticed in another place that no explicit triggers are used for the inhale statement. Is there a reason for that?...

Great, thank you! I will proceed with the smaller set for the trigger in that case: ``` { lookup_pure__$TY$__Slice$usize$$int$$$int$(_9.val_ref, i), lookup_pure__$TY$__Array$127$usize$$int$$$int$(_10.val_ref, j) } ``` Revisiting the [other forall quantifier](https://github.com/viperproject/prusti-dev/issues/721#issuecomment-989650542), we...

That makes total sense now, thank you for the clear examples! :smile: > However, it might be less complete, [...] In this case both quantifiers would never be instantiated because...