Prusti proves `false` in `tests/verify_overflow/pass/extern-spec/linked-list.rs` about prusti-dev HOT 2 OPEN

A minimized example. This program verifies (with default flags) despite the prusti_assert!(false);:

use prusti_contracts::*;

struct List {
    sz: usize
}

impl List {
    #[trusted]
    #[ensures(result.sz == 0)]
    fn new() -> List { unreachable!() }

    #[trusted]
    #[requires(self.sz == 0)]
    #[ensures(self.sz == 1)]
    #[ensures(old(0 - self.sz) == 0)]
    fn add_to_empty(&mut self) { unreachable!() }
}

fn main() {
    let mut l = List::new();

    l.add_to_empty();

    prusti_assert!(false);
}

If any of the following conditions holds, the program (correctly) doesn't verify:

• passing CHECK_OVERFLOWS=false
• removing the #[ensures(self.sz == 1)] (line 14)
• removing the #[ensures(old(0 - self.sz) == 0)] (line 15)
• changing 0 - self.sz on line 15 to any of: 0, self.sz, or self.sz - 0

from prusti-dev.

Nice catch! It seems that overflow conditions of old expressions are encoded without an old(..) around them. That is, the postcondition old(0 - self.sz) == 0 is being encoded as self.sz == 0 && old(0 - self.sz) == 0 but it should be old(self.sz == 0) && old(0 - self.sz) == 0.

from prusti-dev.