proof_for_contract rejects code accepted by proof #3796
Description
I tried this code:
#[kani::requires(true)]
fn foo() {
for _ in 0..2 {
for _ in 0..2 {}
}
}
#[kani::proof_for_contract(foo)]
#[kani::unwind(3)]
fn check_foo_contract() {
foo()
}using the following command line invocation:
cargo kani -Z function-contracts
with Kani version: cargo-kani 0.57.0
I expected to see this happen:
VERIFICATION:- SUCCESSFUL
Instead, this happened:
SUMMARY:
** 1 of 55 failed
Failed Checks: Check that self->start is assignable
File: "/home/runner/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/range.rs", line 767, in <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next
VERIFICATION:- FAILED
Note: Verification using kani::proof works as expected.
#[kani::proof]
#[kani::unwind(3)]
fn check_foo() {
foo()
}