Federico Poli

I'm also not an expert, but I just found that ["according to docs, only one thread can use use JVM at a time"](https://stackoverflow.com/a/43699589/2491528). So, it should be possible by using...

@cmatheja

Thanks for the report! This is the same issue as https://github.com/viperproject/prusti-dev/issues/389; there is an overflow check generated by the compiler that breaks the encoding of the loop.

Yes, the general issue is not specific to overflow checks. See https://github.com/viperproject/prusti-dev/issues/389#issuecomment-984449062. Feel free to post any such example.

This might be the same thing that happened in #583. Aurel explained: > We have versions of this test in the test suite. They were disabled with the latest snapshot...

> My only guess is that syntactically changing the program somehow enables Z3 to trigger the quantifier. I'd also compare the change randomizing the Z3 seeds: ``` // Prusti.toml extra_verifier_args...

Implemented in #858 by @Pointerbender. Thanks! @vakaras Do you prefer to keep this issue open because of the following todo, or can I close? > The test prusti-tests/tests/verify/pass/issues/issue-812-4.rs is currently...

Thanks for opening the issue. Drop calls are not supported and not verified by Prusti, because we don't get from the unoptimized MIR the precise condition under which the drop...

In particular, `drop(..)` terminators are transformed into method calls and other statements by [this MIR pass](https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/elaborate_drops.rs), which happens after Prusti gets its version of MIR from the compiler.

What happens is that `prusti-test` *uses* the binaries of `prusti-launch` and `prusti`, but there is no cargo dependency between them because there is no code dependency. (In the old Makefile...