[SwayamInSync]

The release dry run (S2, run 40818283399) failed one test on Linux: suite/certified_failure_attribution.cpp took more than its 40 s bound with the archive's cpp-verify, while every Linux CI job passes it in about 2 s. The archive is built in two stages, so its Z3 is built by Clang; CI's Linux release job builds Z3 with GCC.

What depends on the build

The test guards one scheduling property: when the complete query of a module is refuted, the failure is reported at once, the obligations only choosing which failure within the complete query's probe (6 million units), instead of waiting for an obligation whose own search does not end (60 s). Its function failed a postcondition whose own query does not end and which the complete query refuted within the probe, but only with a GCC-built Z3:

cpp-verify	Z3 built by	--jobs=1	--jobs=3
main, GCC	GCC	1.8 s (5 of 5)	1.7 s (5 of 5)
main, GCC, relinked with Clang 18's libz3.a	Clang 18	62 s (2 of 3), once over 120 s	3.7 s (2 of 3), once Unresolved after 62 s
TSan session's Clang 18 build	Clang 18	67 s, once over 120 s	7.8 s, once Unresolved after 64 s

The relinked binary differs from main's only in Z3's compiler, and its Layer 4 query is byte for byte the same, so the difference is in Z3's search. Over every test program (the Z3 gate's differential.py, one job per file), the two Z3 builds decided differently only here (lost) and in llvm_uleb128.cpp, where the Clang-built Z3 proved decode_uleb128_canonical (and so roundtrip_uleb128) and the GCC-built one timed out; total 2501 s and 2492 s. So neither build is worse; this test's input relied on one build's search order, as its UNSUPPORTED: system-darwin (Apple's Clang builds Z3 there) already said.

I tried two scheduling changes before settling on the test. Restarting the complete query in turns of growing length did not help, since a fresh start in the same process mostly repeats the same search (Clang-built Z3, --jobs=1: 3.8 s, 49 s, and twice over 150 s). Probing with four random seeds instead of one (as F*'s --retry does) did not either (--jobs=1: 62 s, 5 of 5). Neither is in this PR.

Change

The test's function is now refuted through a check any Z3 refutes at once, after a check whose search ends in no Z3:

void cubes(int a, int b, int c)
  cppverify::pre(0 < a && a < 1000 && 0 < b && b < 1000 && 0 < c && c < 1000)
{
  cppverify::check(a * a * a + b * b * b != c * c * c);
  cppverify::check(a < 0);
}

• The first check alone ends solver.timeout with either Z3 (20 s timeout: 41 s, both).
• The test as written: 1.1 to 1.2 s in 20 of 20 runs, 5 each with one job and three jobs, with either Z3; it reports 5:22: error: verification failed: cubes [assertion].
• Mutant (the obligations that choose the failure get the full timeout instead of the probe's budget): 60.1 s with one job and three, so the 40 s bound catches it.
• It no longer needs UNSUPPORTED: system-darwin.

ARCHITECTURE.md's probe paragraph no longer says the probe's stopping point is independent of the build; it says it depends on Z3's own build, with these numbers.