Federico Poli

Where is the timeout set? Edit: [here](https://github.com/viperproject/prusti-dev/pull/811).

It seems to me that the transformation from the first to the second quantifier that you reported is doing a lot of unnecessary stuff. I don't see why we would...

For a similar reason I ended up writing https://github.com/viperproject/jni-gen (undocumented...) Our approach inspects the JVM by reflection at Rust's compile time and generates wrappers for methods listed in a whitelist...

Oh, I got it the other way around. Yes, I meant creating native proxies of Java objects. I just opened an issue to track it (#82). Thanks for the suggestions!

> rustup is installed already and upgraded by this action only if need I'm not sure that would work on MacOS. I just found that on `macos-latest` a manual `rustup...

Thanks for the report! With the workaround it seems that you hit a Prusti bug which originates from the following line: https://github.com/viperproject/prusti-dev/blob/e85739dadbcce2fbee46f8a2f0f904d7c819a618/prusti-viper/src/encoder/type_encoder.rs#L152 @cmatheja have you already seen this? I'll at...

The panic should be fixed by #322.

Wow, thanks for finding and explaining that case @gavinleroy! I cannot find a crate to gracefully terminate a process depending on the platform. What you wrote seems the best short-term...

> @fpoli I could allocate some time in the next day or two to find all the instances in the test suite where something similar to the above is happening...

The Viper parameter is documented here: https://github.com/viperproject/silicon/blob/a8c8bce4967919b2ae652a28857a6be536c8d0f6/src/main/scala/Config.scala#L206-L210 It's then converted to Z3 here: https://github.com/viperproject/silicon/blob/16fd1f6412ab1b3b09d5e2acea637e47b6f4154a/src/main/scala/decider/Z3ProverStdIO.scala#L293 With `PRUSTI_DUMP_DEBUG_INFO=true` you should find at `log/viper/*.smt2` the dump of the commands that Viper sends to...