[SwayamInSync]

Plan item D1 (a current Z3, adopted only through the gate) and exit criterion 9. The gate existed as a private script over the sequence benchmark and a 20-file corpus. This makes it a CI job over every Verify test program, runs it for the newest Z3, 5.3.2 (2026-10-25), and records the verdict: 0.2 keeps Z3 4.13.4.

The gate (clang/utils/cppverify-z3-gate)

gate.sh BASE CANDIDATE, given two cpp-verify builds that differ in their Z3:

• Stage 1, the sequence benchmark (seqbench.py, from the study that chose cpp-verify's sequence encoding): every valid and false claim, in cpp-verify's encoding (NT) and in the plain sequence theory (N), solved by both Z3 binaries. A claim counts as the verifier decides it: by NT with one job, and by NT or N with more, where the two race. The old script failed a candidate for losing a claim in any encoding, including encodings the verifier never runs alone.
• Stage 2, every Verify test program (differential.py, 462 files), verified by both builds at one job. Each function whose verdict changed is LOST (a proof or certified failure of the base the candidate does not give), FLIPPED (Verified in one and Failed in the other: someone is wrong), GAINED, or CHANGED; time changes over 2x and 5 s are listed.
• A LOST or FLIPPED result fails the gate.

.github/workflows/cppverify-z3-gate.yml builds cpp-verify with the vendored Z3 and with the candidate (cloned at its tag, -DCPPVERIFY_Z3_SOURCE_DIR) in parallel, then runs gate.sh. It runs every Monday for Z3's newest release, by hand for any tag (z3_tag), and on a pull request that changes it, so this PR runs it for 5.3.2.

Z3 5.3.2

Run locally (base: main with 4.13.4; candidate: main with 5.3.2):

== stage 1: the sequence benchmark
one job   base: 22 proofs, 23 models
one job   cand: 23 proofs, 23 models
more jobs base: 22 proofs, 24 models
more jobs cand: 23 proofs, 24 models
GAINED e6_sub_sub.ok
== stage 2: every Verify test program
LOST clang/test/Verify/suite/certified_failure_attribution.cpp break_heap_wrong
TIME clang/test/Verify/suite/certified_failure_attribution.cpp base 1.9 s new 66.4 s
CHANGED clang/test/Verify/suite/certified_quantifier_ranges.cpp first_positive_bitwise
TIME clang/test/Verify/suite/certified_quantifier_ranges.cpp base 0.4 s new 31.1 s
LOST clang/test/Verify/suite/induction_mutual_recursion.cpp even_mod
TIME clang/test/Verify/suite/induction_mutual_recursion.cpp base 3.8 s new 11.0 s
TIME clang/test/Verify/suite/llvm_uleb128_errors.cpp base 11.5 s new 4.2 s
LOST clang/test/Verify/suite/sequence_induction.cpp count_reverse
TIME clang/test/Verify/suite/sequence_induction.cpp base 15.1 s new 150.5 s
TIME clang/test/Verify/suite/spec_post_unfolded.cpp base 4.5 s new 12.7 s
462 files: 3 lost, 0 flipped, 0 gained, 1 changed, 6 with a time change; total 2412 s -> 2656 s
gate: FAIL

5.3.2 no longer loses the 50-push chain's model that sank 5.1.0 in stage 1, and gains a proof there; on the test programs it loses what 4.16.0 and 5.1.0 lost (even_mod, count_reverse, break_heap_wrong), and nothing flips. A second run gave the same results. Per decision Q4 (the newest release that passes the gate), 0.2 keeps 4.13.4; the weekly job says when one passes.

Docs

• third_party/README.md, "Upgrading Z3";
• ARCHITECTURE ("Regression and Coverage");
• release notes ("Z3 releases pass a gate", with the verdict on 5.3.2).

Not done

• Whether the three losses are our encoding's: the plan asks to investigate before the freeze. They are the same three functions with every release since 4.13.4.