Federico Poli

For the moment, splitting big predicates into multiple smaller predicates should help. Like: ``` predicate! { pub(super) fn huge(cursor: &Cursor) -> bool { small1(cursor) && small2(cursor) && small3(cursor) } }...

Thanks for reporting that. Which version of Prusti are you using? Using the latest version of the `master` branch this program verifies for me, without the redundant `... result ==...

No need to compile from source; the last nightly release should be enough. I actually found that I had `check_overflows=false` in my `Prusti.toml`; my bad. With overflow checks enabled I...

> @fpoli should it be harmful to use the `check_overflows=false` flag? I am not interested in checking overflows for now. I see that the postconditions are still checked and the...

Could you check if the Viper dumps of Prusti (`dump_viper_program=true`) are deterministic? The `extra_verifier_args` are defined [here](https://github.com/viperproject/silicon/blob/46a822ce1ec4a222ee0b909471550a7a5d1a829f/src/main/scala/Config.scala). I'm not familiar with all of them, but you can at least check...

Related issues: https://github.com/viperproject/prusti-dev/issues/2 and https://github.com/viperproject/prusti-dev/issues/910

Full example: ```rust use prusti_contracts::*; #[extern_spec] impl Option { #[pure] #[ensures(result == match self { Option::Some(_) => true, Option::None => false, })] fn is_some(&self) -> bool; #[requires(self.is_some())] #[ensures(match self{ Option::Some(v)...

Given this encoding ``` // [mir] _2 = std::option::Option::::unwrap(move _3) -> [return: bb1, unwind: bb4] label l1 assert (m_is_some(_3)) && (true) ... inhale (((old[l1](_3.discriminant)) == (0))?(false):((downcast _3 to enum_Some in...

Adding `old(..)` in the postcondition around the argument of `unwrap` avoids the error: ```rust use prusti_contracts::*; #[extern_spec] impl Option { #[pure] #[ensures(result == match self { Option::Some(_) => true, Option::None...

I'm not aware of limitations regarding cargo workspaces. Prusti should just run on each crate that compose the workspace, but not on the crates.io dependencies. The "error: unknown '--json' option...