Pointerbender

> 1. Something is wrong in those quantifiers. Probably a `j == i + ... &&` condition is missing. > 2. It should be possible to merge the two inhale...

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 able...

> I'm afraid a matching loop is there, but in your case it terminates quickly just because the instantiations (bounded in depth by some Z3 parameter: smt.qi.eager_threshold and smt.qi.lazy_threshold) happen...

This is a really fun exercise so far :) I have a another idea. Instead of the quantifier used for slicing an array: ``` inhale (forall i: Int, j: Int...

p.s. to elaborate a bit further on why I chose `{ lookup_pure__$TY$__Slice$usize$$int$$$int$(_0.val_ref, i) }` as the trigger and not `{ lookup_pure__$TY$__Array$127$usize$$int$$$int$(array.val_ref, j) }` as the only trigger: If we were...

Nice example! Please allow me to try and dissect it a bit :) > The difference should be observable in a program that calls a trusted method that converts a...

Thank you for the great explanation! :smile: > Regarding the (planned) quantifier in `ProcedureEncoder::encode_assign_slice`, just changing the triggers from `{ pure_lookup_array(array, i) } { pure_lookup_slice(slice, i) }` to `{ pure_lookup_slice(slice,...

@sporksmith Could you please try if the code from PR #297 fixes the issue you are describing?

I did a bit of investigation. I was not able to resolve it yet, but here is some additional information about the underlying issue. The `beforeResolve` stage resolves without an...

Actually, after sleeping on it for a night, I think I have a nicer idea: I can just translate the `PResultLit` to a new custom `PAdtResultLit` whenever it references an...