While upgrading to nightly-2024-03-15, we had to add a few #[kani::unwind] attributes to harnesses with for loops with simple integer ranges. We need to investigate why this is no longer the case, and hopefully improve the loop bound detection algorithm.

Here is an example of a test case (tests/expected/iterator/main.rs):

#[kani::proof]
#[kani::unwind(4)] // Kani will unwind forever if we remove this attribute.
fn main() {
    let mut z = 1;
    for i in 1..4 {
        z *= i;
    }
    assert!(z == 6);
}

using the following command line invocation:

kani main.rs

with Kani version: #3084

I expected to see this happen: Kani should be able to automatically detect the loop bound.

Instead, this happened: Kani requires an unwind attribute.