Modifies property points to a temporary variable

[celinval]

I tried this code:

// File global_fail.rs from the regression.
static mut PTR: u32 = 0;

#[kani::requires(PTR < 100)]
unsafe fn modify() {
    PTR += 1;
}

#[kani::proof_for_contract(modify)]
fn main() {
    unsafe {
        modify();
    }
}

using the following command line invocation:

kani -Z function-contracts global_fail.rs

with Kani version:

I expected to see this happen: Ideally a failure pointing due to PTR not being assignable.

Instead, this happened: The error message mentions a temporary variable leaving the user to do manual inspection of their code.

Failed Checks: Check that *var_3 is assignable