I tried this code:

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

#[kani::requires(true)]
fn simple_loop_with_loop_contracts() {
    let mut x: u64 = kani::any_where(|i| *i >= 1);

    #[kani::loop_invariant(x >= 1)]
    while x > 1 {
        x = x - 1;
    }

    assert!(x == 1);
}


#[kani::proof_for_contract(simple_loop_with_loop_contracts)]
fn foo() {
    simple_loop_with_loop_contracts()
}

using the following command line invocation:

cargo kani -Z function-contracts -Z loop contracts

with Kani version: 0.59

I expected to see this happen: verification succeeds

Instead, this happened: the loop invariant is ignored, so the loop unwinds forever.

I find it confusing that we call it a "loop contract" and yet we can't use a "proof for contract" for it.

The same unwinding behavior happens if I change the harness to be a #[kani::proof]--it appears we can't prove invariants at all in the presence of other contracts.