The solver-state invariance failure — evidence¶

Subject: tests/test_gsc_adversarial.py::TestSolverStateInvariance::test_no_recovery_unknown_leaves_solver_untouched

Status: RESOLVED 2026-09-03. The cause is Z3 behaviour, not a defect in zqel and not memory corruption. Sections 1–4 are the investigation as it ran; section 7 states the answer and what was wrong along the way. The document is kept in full rather than rewritten, because the refuted readings are the useful part: two of them were confident and wrong.

Original status line: open. Cause not established. This document records what was measured, what was refuted, and what is still unknown. Sections 1 and 2 are observations with the command or run that produced them; section 3 lists hypotheses that were tested and refuted; section 4 states what is not known. Nothing here is inference unless it is labelled as such in section 5.

Written 2026-09-03 after the failure turned main red.

1. What the test asserts, and how it fails¶

ProofEngine._sat carries an explicit state contract, stated in its own docstring (zqel/proof.py:299):

Never modifies the caller's assertion set or scope depth; only solver parameters (timeout, random_seed) are adjusted.

The contract exists because prove_contract_modular reuses one solver across queries. The test measures it with

def _snapshot(self, s):
    return (len(s.assertions()), s.num_scopes())

taking a snapshot before and after _sat, and comparing. The body builds a fresh context, adds exactly two assertions — a quantified array property and a nonlinear real equation — and pins the timeouts to 1 ms so the query is guaranteed to come back unknown:

monkeypatch.setattr(ProofEngine, "FIRST_TIMEOUT_MS", 1)
monkeypatch.setattr(ProofEngine, "TIMEOUT_MS", 1)
monkeypatch.setattr(ProofEngine, "SEED_RETRIES", 1)
...
s.add(z3.ForAll([v], z3.Select(a, v) * z3.Select(a, v) >= 0))
s.add(x * x * x + z3.Select(a, _bv(0, ctx)) * x == z3.Q(1, 7, ctx=ctx))
before = self._snapshot(s)
ProofEngine._sat(s)
assert self._snapshot(s) == before

The observed failure (forgejo run 426, main a828cfaf, worker gw2, Linux):

assert (0, 0) == (2, 0)

The solver came back with zero assertions where it had two. Suite totals for that run: 1 failed, 4933 passed, 146 skipped in 660.37s.

2. Measurements¶

All container measurements: LXC 128 zqel-z3-lab, Debian 13, 8 cores, 16 GB, Python 3.13.5, z3-solver==4.16.0.

2.1 The rate depends on system load¶

Same node, same machine, same binary, back to back:

Condition	Failures
Idle container	0 / 30
8 concurrent CPU-burn processes	1 / 30
While solver work (an example soak) was still draining	13 / 60 and 15 / 60

The failure does not occur at all on an idle machine and is common under solver-heavy load.

2.2 It does not reproduce on macOS¶

10 consecutive runs on the development machine (aarch64-darwin, z3-solver==4.16.0 wheel), including runs with 8 CPU-burn processes alongside: 0 failures. Every reproduction to date is on Linux.

2.3 Where the assertion set is lost¶

An instrumented rebuild of the test (probe_invariance.py) takes a snapshot after each step of _sat separately — after the first check(), after the constant-select recovery, and after the seed-diversified retry. Under load, 200 attempts in one process:

failures: 12/200
  attempt  0: before=(2,0) after_first_check=(1,0) after_nlsat=(1,0) after_seed=(1,0)
  attempt  6: before=(2,0) after_first_check=(0,0) after_nlsat=(0,0) after_seed=(0,0)
  attempt  7: before=(2,0) after_first_check=(2,0) after_nlsat=(2,0) after_seed=(0,0)
  attempt 18: before=(2,0) after_first_check=(0,0) after_nlsat=(0,0) after_seed=(1,0)
first divergence: {'first_check': 6, 'nlsat': 0, 'seed': 6}

Three observations follow directly from this table:

The loss happens inside solver.check(), not in zqel's recovery logic: six of twelve failures already diverge after the first check, and the remaining six after the seed retry — which is also a check().
The constant-select recovery is not involved. after_nlsat never differs from after_first_check ('nlsat': 0). This is consistent with its implementation, which reads solver.assertions() and builds a separate side solver.
The count is not monotonic. Attempt 18 goes 2 → 0 → 1. A solver that had genuinely lost its assertions could not report more of them afterwards. Whatever len(s.assertions()) reads is not a stable quantity at that moment.

2.4 The count that is read¶

z3.unknown was the verdict (r1=unknown) in every recorded failure, as the 1 ms timeout intends. So the failure occurs on the path the test was written to exercise, not on an unexpected one.

3. Hypotheses tested and refuted¶

3.1 "It is the Z3 use-after-free" — REFUTED¶

The obvious first guess: a lost assertion set is what a heap use-after-free does when it does not happen to segfault, and issue #79 documents exactly such a bug in asserted_formulas::assert_expr, the function every recorded SIGSEGV stack ends in.

Tested by running both libraries on the same machine, back to back:

Library	Failures
Unpatched wheel libz3 (`7d8507589c3f5cd1`)	13 / 60, then 1 / 100
Patched build, same tag (`f903ac0b20002ddc`)	15 / 60, then 2 / 100

Totals: 14/160 unpatched, 17/160 patched. The patch does not change this failure rate. Whatever causes it, it is not the use-after-free that patch fixes.

3.2 "The watchdog thread is not joined" — REFUTED¶

_watchdog_check (zqel/proof.py:262) runs solver.check() in a daemon thread and never joins it:

t = _th.Thread(target=_run, daemon=True)
t.start()
if not done.wait(hard_budget_ms / 1000.0):
    ...

After done.wait() returns, the worker thread is still finishing — and as it exits, its local references drop, which releases Z3 AST objects. If the main thread reads s.assertions() at that moment, two threads touch one Z3 context, which Z3 does not support.

Tested by adding t.join(30.0) before reading box[0] and rerunning the probe under the same load: 10/200 with the join, 12/200 without. Within noise. The join was reverted.

3.3 "It is `pytest-randomly` reordering or reseeding" — REFUTED¶

pip list in the container shows pytest-xdist 3.8.0 and no pytest-randomly. The plugin that was suspected is not installed.

3.4 "It is the pytest process boundary" — REFUTED¶

The instrumented probe was run 40 times as 40 separate processes (one attempt each) on an idle machine: 0 failures. The same probe run 40 times inside one process: 0 failures. Neither the process boundary nor process reuse reproduces it on its own; load does.

4. What is not known¶

The mechanism. Section 2.3 localises the loss to solver.check() and shows the count is unstable, but nothing here identifies what corrupts or misreports it.
Whether the failure predates 2026-09-03. Eight earlier forgejo runs were searched for the test name and none contains it — but four of those eight (runs 412–424) died in the libz3 install step before the suite ran at all, so they are not evidence of absence. The remaining four ran the suite without this failure, which at the rates in §2.1 is unremarkable either way.
Whether PI-2b made it more likely. PI-2b moved 184 example nodes out of the parallel run into a supervised block. That changes what runs concurrently with what, and §2.1 shows the rate depends on load — but no measurement here compares the suite's load profile before and after.
Whether the same effect can corrupt a proof result. The test detects the loss because it asks. Nothing was measured about what a caller would observe if its solver silently lost assertions between queries.

5. Labelled inference¶

I-A (supported, not proven). The failure is a symptom of shared-state corruption around a Z3 context under load, not a logic error in ProofEngine._sat. Support: the recovery path is provably uninvolved (§2.3), the count is non-monotonic (§2.3), and the rate scales with load (§2.1). Against: no mechanism identified, and the two most concrete corruption candidates were refuted (§3.1, §3.2).
I-B (supported). This failure and the segfault family of issue #79 are different problems. Support: the patch that removes the use-after-free leaves this rate unchanged (§3.1). This is the same kind of correction the crash dossier had to make about its own inference I1 — a shared symptom class is not a shared mechanism.

6. Consequence for the gate¶

At the rates in §2.1 this test can fail a suite run that is otherwise green, and it did so on main a828cfaf. It is a real assertion about a real contract — prove_contract_modular does reuse one solver — so it must not be weakened to make the gate quiet. Until the mechanism is known, a red run whose only failure is this test should be read as "the environment, again", not as "the change under review is broken", and re-run.

Related: docs/native-crash-dossier.md (the segfault family, a different problem per I-B), issue #79 (the Z3 patch).

7. Resolution — the cause, and what the investigation got wrong¶

Found by Michael Protogerakis in the Z3 sources, then reproduced here deterministically on macOS, with no threads and no wall-clock race:

s.add(f1); s.add(f2)          # f1 quantified, f2 nonlinear
len(s.assertions())           # 2
s.set("rlimit", 20)
s.check()                     # unknown
len(s.assertions())           # 1      <- the whole mystery
s.push(); s.pop()
len(s.assertions())           # 2      <- restored, instantly

After an unknown verdict Z3's strategic solver (tactic2solver) reports the remaining tactic goal rather than the assertions that were added. The surviving entry is the original f2, unmodified; the quantified f1 is simply not in the view. A neutral push()/pop() brings both back.

This explains every measurement in sections 2 and 3:

The counts 2 → 0 → 1 (§2.3). Each retry runs internally against the original two formulas, and each unknown replaces only the public view with whatever tactic goal is left. Non-monotonic counts are then expected, not impossible.
The load dependence (§2.1). Load decides how far the tactic pipeline gets before the budget expires, which decides what remains in the view.
The platform dependence (§2.2) and why the patch changed nothing (§3.1) — this was never a memory bug.

rlimit is worth a sentence of its own, because it appeared in the segfault hunt too: it is a tool, never a cause. It replaces a scheduler race with a deterministic bound, which is exactly what turned an unreproducible flake into a two-line demonstration.

What this investigation got wrong¶

"State corruption" (I-A). Refuted. A push/pop restores the view; no corruption does that. The inference was labelled as unproven, which was right, but it steered a day of work toward memory bugs.
"The loss happens inside solver.check(), not in zqel's recovery" (§2.3). True as stated but misleading in effect: nothing was lost. The measurement was correct, the word "loss" was not.
The threading-contract violation in _watchdog_check was real and is fixed — Z3 permits only Context.interrupt() across threads — but it was not this cause. Measured before and after: 13/700 attempts against 12/700.

Inference I-B stands and is now confirmed: this and the segfault family of issue #79 are different problems, with different causes and different fixes.

Consequences in the code¶

ProofEngine._sat captures the assertion set before the first check and hands that snapshot to _const_select_nlsat. The recovery previously read the post-check view and therefore reasoned about a subset — sound, since an unsat subset implies an unsat whole, but needlessly incomplete. It is the only place in zqel/ that reads solver.assertions(); the proof-cache key is built from to_smt2() before the check and is unaffected.
The invariance test no longer forces unknown with a 1 ms timeout. A timeout is a race, not a fixture.
Z3's view switch is pinned as behaviour (TestZ3AssertionViewAfterUnknown), so a future Z3 that changes it reports here rather than breaking something downstream.
tests/test_z3_state_under_load.py keeps asking the question that is still worth asking — whether a real check under contention costs the solver its state — by normalising the view with push()/pop() first.