jthomme1

The following program fails to verify: ```rust use prusti_contracts::*; predicate!{fn magic(i: i64) -> i64 { i+1 }} #[ensures(magic(1) == 2)] fn main() { } ``` with the following error message:...

The following example program results in `Consistency error: Local variable _0_quant_0 not found.`: ```rust use prusti_contracts::*; fn main() { } #[requires(forall(|a:i32| exists(|b:i32| b == 5 ==> b < a)))] fn...