kani fails to unwind 2 x 1 elements nested loop in firecracker code #1786
Description
I am running the following command
cargo kani -p arch --enable-unstable=mir-linker --harness test_msr_allowlist --restrict-vtable
on this Firecracker version:
firecracker-microvm/firecracker@99f3023
with the attached patch applied, with Kani version: 0.0.1.
I expected for Kani to be able to unwind the nested loop (outer loop is 2 elements, inner loop is 1 element).
Instead, I see the following output:
SUMMARY:
** 1 of 187 failed (186 undetermined)
Failed Checks: unwinding assertion loop 0
File: "/local/home/kalyazin/workspace/firecracker/src/arch/src/x86_64/msr.rs", line 354, in x86_64::msr::tests::test_msr_allowlist
VERIFICATION:- FAILED
[Kani] info: Verification output shows one or more unwinding failures.
[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
Verification Time: 10.091045s