[SwayamInSync]

Fix the macOS flake of extent_separation.cpp: on #122's macOS job, wrong_copy ended Unresolved [reason=solver.timeout] after its whole 120 s budget, where the test expects its certified failure (it takes 1.7 s on Linux). Its query is the one main builds; whether model search finds the counterexample through the loop invariant over a framed heap depends on the solver's search order, which varies from run to run (Z3 hashes some objects by address).

The function's point is that separating valid(p, n) extents does not hide a real failure: a copy that writes zeros must fail where a holds anything else. A copy of two cells shows the same without a loop, and its counterexample needs no search: wrong_copy now fails its postcondition in milliseconds, and the test passes.

The quantified loop invariants over memory keep their own false cases in the loop tests.