Closed as duplicate of#3697
Description
Requested feature: History expression support for loop contracts
Use case: old(var) refer to the value of var upon the entrance of the loop.
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167
Test case:
#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]
#[kani::proof]
fn simple_while_loop_with_old_harness() {
let mut x: u8 = kani::any_where(|i| *i >= 2);
let mut y: u8 = x;
#[kani::loop_invariant(x >= 2 && y <= old(y)]
while x > 2 {
x = x - 1;
if x == 5 {
y = y - 1;
}
}
assert!(x == 2);
}