Federico Poli

Good catch! The encoding of `Path::invariant` seems to take 20 seconds (using a debug build of Prusti). This is very unusual, the encoding is very inefficient. All pure functions are...

Regarding the remaining timeouts in the smt2 files, my guess is that they come from other Silicon options, like https://github.com/viperproject/silicon/blob/a8c8bce4967919b2ae652a28857a6be536c8d0f6/src/main/scala/Config.scala#L212-L228 You should be able to set them in `Prusti.toml` with...

> Does something like this seem appropriate? > > ``` > inhale Slice$len__$TY$__Slice$usize$$int$(_2.val_ref) == 64 > inhale (forall i: Int :: > { lookup_pure__$TY$__Array$64$usize$$int$$$int$(_3.val_ref, i) } > { lookup_pure__$TY$__Slice$usize$$int$$$int$(_2.val_ref, i)...

> Is there any way to find out which triggers were inferred by Viper? Not that I'm aware of. (But it would be a useful feature to request. Dafny has...

> Is there some performance to be gained if we make this a single trigger set? Your mental model is correct. A single trigger set would trigger in strictly less...

Note that reducing quantifier instantiations might make verification of some programs slower. For example, a Rust function with a precondition `forall i :: { f(i), g(i), h(i) ... } false`...

> Should we replace it with two inhaled quantifiers? Like so: > > ``` > inhale forall i: Int :: { lookup_pure(array, i) } start forall j: Int :: {...

> ``` > inhale ( > forall j: Int :: { lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) } > start.val_int && j < end.val_int > && j + start.val_int < Slice$len__$TY$__Slice$usize$$int$(_0.val_ref) > ==> lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref,...

Btw, kudos for preparing a complete Viper example! I'm impressed :)

> p.s. if we end up implementing the above solution, then we'd have to use snapshot encoding for the expressions in the quantifiers instead, otherwise programs like these won't be...