"UNKNOWN" vs "FAIL" for k-induction vs --loop-invariant-check #6095

@LukeW1999: Could you please check this issue?

Hi @MarkAA-uw, thanks — and thanks @lucasccordeiro for the ping. Yes, this is expected, and it comes down to the same BMC-vs-k-induction distinction as #6092.

--loop-invariant-check runs as standalone plain BMC (see #6092): with no invariant to cut the loop, it unrolls the loop until it naturally terminates. This loop terminates after 5 iterations (idx: 10 -> 1 -> 8 -> 3 -> 6 -> 5), so BMC reaches the __ESBMC_assert(false, ...) after it and reports FAILED — correct.

--loop-invariant runs k-induction, and here you capped it with --max-k-step 2. Reaching that assertion needs the base case unrolled to k = 6, so at k = 2 the base case finds no violation, and neither the forward condition nor the inductive step can close the proof. Having exhausted the bound without a conclusion, k-induction reports UNKNOWN — i.e. "within k = 2 I can neither find a bug nor prove safety". That is sound (inconclusive), not a wrong answer.

Bump the bound past the required depth and it reports FAILED again — --max-k-step 6 (or higher, and the default of 50) all give VERIFICATION FAILED / "Bug found (k = 6)". So same theme as #6092, just with a --max-k-step smaller than the unwinding depth the bug needs.

@LukeW1999 -
Thank you for the explanation. It really clarifies the induction strategies.
-mark