Kani fails to detect for loop bound after upgrade to nightly-2024-03-15

[celinval]

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.

[OliverKillane]

This appears to also affect incredibly simple cases like:

#[kani::proof]
fn check() {
  for _ in 0..1 {}
}

Note 0..0 still works

[tautschnig]

With apologies for not actually posting on this issue: diffblue/cbmc#8247 fixes this problem on the CBMC side. We just need to get this merged plus a new CBMC release to be produced.