[SwayamInSync]

confirmation_invariants.cpp failed on the macOS runners of #105 and #110 (2 of 5 macOS runs today): bounded_copy, whose loop invariant i <= 8 is not inductive, ended Unresolved [solver.timeout] after 21 s instead of failing at once. Neither PR touches the test or the solver; the same commit passed on the other runners.

Why

The failing check's query assumes the second invariant, forall j in [0, i). out[j] == a[j], and the loop's heap frame. At i = 8 a counterexample needs a memory in which eight elements are copied, which Z3's model search finds or not depending on its search order. On Linux the search order changes with the variables' names, which reproduces it: of 40 renamings of the test's variables, 2 took the whole 20 s budget and the mean was 4.2 s.

The fix

The invariant fails at i = 0 instead (i <= 0), where the quantified invariant ranges over no element, so any memory is a model. Of the same 40 renamings, none took more than 0.20 s. The budget goes back from 20 s to 5 s, which #104 raised for this failure.

The test still checks what it is for, the early end of the search for an execution that fails a dropped invariant: with that end removed (if (Bound >= 1 && !Unrolled) return Notes; deleted), the confirmation takes 5.2 s at --timeout=5000, and the test's check that it takes under a second fails.