Federico Poli

> Is there anything we can do to fool Z3 into reliably aborting the matching loop early? This seems to verify very fast despite the high `k`: That's already done...

(In your latest example `assert false;` verifies too.)

> playing devil's advocate here That's the right approach :) > So I guess at least it's a trade-off between supporting some (uncommon?) specifications in a user-friendly way and performance...

Thanks for the clarification! Sorry, I didn't notice that your [penultimate comment](https://github.com/viperproject/prusti-dev/issues/721#issuecomment-995205110) was about quantifier 1 instead of 2. Regarding the (planned) quantifier in `ProcedureEncoder::encode_assign_slice`, just changing the triggers from...

Did you install `rustup` via snap? If so, see this answer: https://stackoverflow.com/a/72168145/2491528

I just tried running the latest `cargo-prusti` from the command line of Ubuntu on `procedural-map` and Prusti just complains about (many) unsupported features in `procedural-map`. So, I can't reproduce the...

I was able to reproduce this issue: our `cargo-prusti` was launching the stable version of `cargo`/`rustc` instead of the expected nightly one. The PR https://github.com/viperproject/prusti-dev/pull/1181 should fix the issue. It...

The fix is now available also in the `latestRelease` channel.

Two more examples, from #1205: ```rust fn main() { let mut i = 0; loop { i += 1; if i == 10 { break; } } } ``` ```rust...

> I mean you need to at least change this line to instead give an empty cache: > > ``` > error!("Failed to read cache from \"{}\": {e}", cache_loc.display()), >...