Hold z3-solver 5.0.0.0 for a bake period, then re-run the obligation differential

[aallan]

z3-solver 5.0.0.0 (#1119) is held for a bake period rather than merged. This issue carries the reasoning and the re-check procedure so the decision does not have to be reconstructed later.

Why it is held

Not because anything failed — CI is green and the behavioural evidence is strong. Because the evidence does not cover the risk.

5.0.0 published	2026-07-17
Release notes body	13 characters — 5.0.0 release, no documented changes
Commits since 4.16.0	1,699

A major version, 1,699 commits, no published changelog, and days rather than months of field exposure — in the verification core of a language whose premise is proof. #996 is already tracked as a conformance trap that surfaced once in ~960 runs, which is the shape of defect a corpus differential cannot reach. Nothing in Vera needs a 5.0 feature, so waiting costs nothing.

What was already validated (on 2026-07-21, against 4.16.0.0)

• Per-obligation differential, 2,329 obligations, byte-identical. All 39 examples plus all 163 conformance programs, comparing each obligation's kind, status, line, column and description — not summary counts, which would hide a reshuffle.
• Zero tier3 → verified transitions, so 5.0.0 proves nothing 4.16.0 did not. That also covers the soundness direction: a solver regression that proved more would show up here.
• Full suite green on 5.0.0 (8,167 passed), 163 conformance, 39 examples.
• test_rounding_relation_not_proved — the Z3-budget-sensitive test behind #1121 — stable at 0.93s across five runs. No timing drift.

The gap is not in that evidence. It is that "identical on this corpus" says nothing about the paths this corpus does not exercise, and a 1,699-commit change has many.

Re-check procedure

Run this on the current pin, then on 5.0.0.0, and diff. Ten minutes, and it reproduces the result above exactly.

# capture.py — writes one line per obligation
import json, subprocess, pathlib
rows = []
files = (sorted(pathlib.Path("examples").glob("*.vera"))
         + sorted(pathlib.Path("tests/conformance").glob("*.vera")))
for f in files:
    r = subprocess.run(["vera", "verify", "--json", str(f)],
                       capture_output=True, text=True, encoding="utf-8")
    try:
        d = json.loads(r.stdout)
        for o in d.get("obligations", []):
            loc = o.get("location") or {}
            rows.append(f"{f.name}|{o.get('kind')}|{o.get('status')}"
                        f"|{loc.get('line')}|{loc.get('column')}"
                        f"|{(o.get('description') or '')[:60]}")
    except Exception:
        rows.append(f"{f.name}|PARSE_OR_RUN_ERROR")
print("\n".join(rows))

python capture.py > /tmp/ob_base.txt            # on the current pin
pip install 'z3-solver==5.0.0.0'
python capture.py > /tmp/ob_new.txt
diff /tmp/ob_base.txt /tmp/ob_new.txt && echo IDENTICAL
pip install 'z3-solver==4.16.0.0'               # restore

Expect 2,329 rows: 1,627 verified, 697 tier3, 1 violated, 4 blank.

Merge criteria

• The differential is still identical, and
• 5.0.0.x has meaningful field exposure by then (a patch release, or upstream issues quiet), and
• full suite, conformance and examples green.

If the differential has changed, that is a finding worth investigating before merging, not a reason to re-baseline.

Handling in the meantime

Keep #1119 rebased as main moves — @dependabot rebase, never recreate. A recreate can re-resolve to a different version, which would silently invalidate the differential above; the whole point is that a specific version was measured.

Revisit from 2026-07-28.