The z3 version is unpinned, and it discharges proof obligations

Recording a divergence rather than a failure. Seam verification shells out to z3, and nothing pins which one.

Observed

Seven years apart. Both currently pass the suite, so this is not biting today.

Why it is worth a ticket anyway

z3 is not a formatter or a linter — it decides proof obligations. src/hir/seam.rs and src/hir/prover.rs spawn it to discharge relaxed transfer-edge obligations in QF_BV, and the answer determines whether a diagnostic fires:

Command::new("z3")

A solver difference does not surface as "z3 disagreed". It surfaces as a missing W1027, or an expected-failure test that passes — which reads as a compiler regression and would be debugged as one. scripts/setup_linux.sh already has a comment saying exactly this about z3 being absent; the same reasoning applies to it being a different version.

QF_BV is decidable and both solvers should agree on satisfiability, so the realistic risks are narrower than "wrong answer":

• a query that times out on one version and not the other;
• reliance on model output whose formatting or variable ordering shifted;
• an incompleteness or bug fixed between 4.8 and 4.15 that changes an edge case.

Suggested

• record the z3 --version alongside the other provenance the suite already captures, so a divergence is visible in the log rather than inferred later;
• decide a minimum version and check it in setup.sh next to the LLVM version check (#365);
• pin it in scripts/setup_linux.sh if a minimum is chosen.

Not proposing to vendor z3. The ask is that the version be recorded and bounded, so that "the solver changed" is a hypothesis someone can rule out in a minute rather than after a day of bisecting the compiler.

Start with the z3 invocations in src/hir/seam.rs and src/hir/prover.rs, then inspect the existing provenance capture and version check in setup.sh and scripts/setup_linux.sh. Compare the setup flow with the LLVM check in #365 and determine where the z3 version should be recorded and bounded. Done means the suite exposes its z3 version and setup enforces the chosen minimum, with relevant checks passing.