[SwayamInSync]

extent_separation.cpp failed on #93's macOS runner, a change that touches no verifier code:

extent_separation.cpp:61:26: Unresolved: wrong_copy [backend=z3] [reason=solver.timeout] (proof obligation ...::invariant-preserved@...)
Summary: 7 verified, 2 failed, 1 unresolved (solver.timeout 1) in 61.1 s

wrong_copy is the test's negative case: a copy loop that writes the wrong values must fail its invariant. It wrote a[n - 1 - i], a reversed copy, and finding a counterexample to its quantified invariant is a hard search. On a Linux machine, three runs of wrong_copy alone with --jobs=1 took 32.6 s and 41.9 s to fail, and the third ended Unresolved [solver.timeout] after 61.5 s.

The loop now writes zeros (out[i] = 0;). The invariant out[j] == a[j] then fails wherever a holds another value: three runs failed in 1.4 s each, and the whole file takes 0.7 s. The case still shows what it is for: under the separation of extents, a copy that is wrong fails, and copy verifies.

This is the third test of the kind after #106 (cvc5_memory_limit.cpp, spec_post_unfolded.cpp). Together they unblock the stack #93 to #99, whose assertions jobs fail only on cvc5_memory_limit.cpp, and whose macOS jobs failed on this test.

[SwayamInSync]

Moved into #106 (commit ea2843d), so that one CI run covers the three tests that failed on runners.