Federico Poli

Thanks for the report. A common technique to debug why a property doesn't hold is to manually assert it with `prusti_assert!(...)` at various points in the program. My first guess...

Thank you for the bug report. The panic is due to an `unreachable!()` in `find_impl_of_trait_method_call`: https://github.com/viperproject/prusti-dev/blob/863cd59705a43863eaba75c0dad1f4521de05aff/prusti-interface/src/environment/query.rs#L273-L320 In other words, Prusti fails to find the method that implements the declared `#[pure]...

Thank you for the report!

Smaller example: ```rust use prusti_contracts::*; #[ensures(value === value)] pub fn get_mut( value: &mut i32 ) -> &mut i32 { value } ``` ``` [Prusti internal error] Prusti encountered an unexpected...

Using `prusti-rustc` with the `-O` flag causes the same error. It seems to be a bug in the pure encoder, when overflow checks are *disabled*. `-O` or `--release` should make...

It's like if this line has no effect: https://github.com/viperproject/prusti-dev/blob/a3fd92b08332bd4685cdac62ecbf8ad4695944cb/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs#L1062

> For some reason, when using the same location for multiple refute statements, the verification will fail on those statements. That sounds like a bug in Viper, related to https://github.com/viperproject/prusti-dev/issues/1213....

> Did you mean I should change my code or the error_manager (I made a change in my code now)? The error manager, because (1) the change in your code...

> BTW the issue would show up also when I have multiple refutes with the same line/column but none of them should fail The change to the error manager should...

Thanks for reporting this. As a workaround, does it work to add the flag `-Pserver_address=""` or `-Pserver_address=MOCK` to the tests that need to set configuration flags for the server?