Skip to content

Native Solver Crash — Evidence Dossier

Development document. Everything below is either a recorded observation with its source, or an explicitly labelled inference. Nothing else belongs here: no hunches, no "probably", no conclusions that outrun their evidence. Sections are separated on purpose — facts, refuted hypotheses, open questions.

Verification: every run/job id refers to https://git.ei.intern.hs-duesseldorf.de/proto/zqel/actions. Kept current as new evidence lands; entries are appended, never rewritten. Live counters: issue #62.

1. Facts — recorded observations

Each row is something that was seen, with the artefact that shows it.

1.1 The hang, caught twice with a full backtrace

Source: run #321, o3-native-diagnosis job, two HANG-after-pass dumps.

Both dumps are identical in structure:

Thread 1 (main): ast_manager::~ast_manager()
                 ← api::context::~context()
                 ← Z3_del_context
                 ← ctypes
Thread 2:        thread_func(scoped_timer_state*) → condition_variable::wait
Thread 4:        thread_func(scoped_timer_state*) → condition_variable::wait

Fact: the process hangs inside Z3 context destruction while exactly two scoped_timer pool threads are sleeping.

1.2 The crash signature

Source: three gdb-captured crashes (runs #303–#315 era), plus the Python-level trace from run #319.

  • Signal: SIGSEGV.
  • Native frame: inside th_rewriter during asserted_formulas::assert_expr from Z3_solver_assert; the exact allocation site varied (small_object_allocator::allocate ×2, obj_map hashtable ×1).
  • Python frame (run #319): Z3_mk_numeral ← RealVal ← zqel/real.py.
  • In every gdb-captured case: two live scoped_timer threads.

Fact: the crash occurs during ordinary term construction/assertion, at varying allocation sites, with the same two timer threads present.

1.3 The timer pool is Z3's own, not ours

Source: run #327, breakpoint backtrace on thread_func(scoped_timer_state*), main-thread stack at the moment of the spawn:

purify_arith_tactic::operator()
  ← and_then_tactical (×12)
  ← try_for_tactical::operator()
  ← or_else_tactical::operator()

Source: local API audit (2026-09-02) — z3.Solver.set and z3.Fixedpoint.set wrapped, every zqel timeout routed through one switchable helper, mode rlimit (no wall-clock timeout armed): no call site armed a timeout, yet the counter still showed timers=1 in every rlimit cell.

Fact: Z3's default solver strategy (try_for inside the portfolio) arms wall-clock timers with its own budget, independent of any parameter zqel sets. A zqel-side "no timers" mode is therefore not achievable with z3.Solver().

1.4 Instrumentation suppresses the crash (heisenbug)

Source: cumulative 2×2 matrix runs v4–v7.

  • Under gdb: ~78 attempts, zero crashes.
  • Uninstrumented, same period: 6 of 7 CI suite runs died at the serial LMFit/LM_Step pair.

Fact: running under ptrace/gdb changes the outcome.

1.5 The thread churn was ours, not Z3's

Source: run #319, churn counters per cell.

watchdog mode thread spawns per attempt
thread 314–352
direct 2

Fact: the ~330 spawns per run came from zqel's own watchdog, not from Z3.

1.6 Two zqel timeout sites were leaking

Source: v4/v5 counters (timers=2 in timeout cells, timers=1 in rlimit cells) plus source scan.

guided_synthesis._new_cdef_solver armed a wall-clock timeout through the kwargs spelling solver.set(timeout=...), which the string scan for set("timeout" did not match. Fixed (PR #37 lineage, merged).

Fact: a source-level scan missed a site that a runtime counter found.

1.7 PI-2 outcomes since the supervisor exists

Source: [supervised] log lines, per run.

run node outcome
#333 reaches_both_backends[LMFit] SOLVER_CRASH (rc=-11) → retry → PASS with recovered teardown livelock
#336 produces_rust[LMFit] SOLVER_CRASH (rc=-11) → retry → recovered
#353 reaches_both_backends[LMFit] SOLVER_CRASH twice (rc=-11, rc=-11) → RED, no third attempt

Fact: the retry recovers sometimes and not always; two of three crashed nodes recovered.

1.8 Crashes occur outside the supervised nodes

Source: run #360 (main, after the #38 merge) and runs

371/#376/#378/#379 (four gates running simultaneously).

  • 360: Fatal Python error: Segmentation fault in the parallel

    suite run, no [supervised] line involved.

  • 371/#376/#378/#379: all four suite jobs stopped mid-run (log ends at

    62–64 %, after ~3 minutes), no test failure printed, no OOM (free: 1 of 8 GB used; dmesg: zero OOM kills on all four runners).

Fact: the crash class is not confined to the four supervised nodes, and four concurrent gates produced four aborted runs.

1.9 Runner and toolchain identity

Source: ci_z3_identity.sh step, plus PI-2 job logs.

Z3 comes from the pinned Nix flake; the identity step records the same library across runs. No run has shown a differing Z3 build.

Fact: the crash reproduces with one pinned Z3 build.

1.10 — Four of 184 example nodes were supervised (2026-09-03)

Raised by Michael Protogerakis, verified against main c15f593c before any change. Each check is a command anyone can repeat:

Check Command Result
PI-1 rim has a production caller grep -rn compile_in_worker Only zqel/isolation.py (definition) and tests/test_pi1_worker_pin.py (its own pins)
The documented isolation switch exists grep -rn ZQEL_ISOLATION Only in docs/adr-process-isolation.md
compile_file has consumers grep -rn compile_file Exactly one: zqel/isolation_worker.py
The CLI batches compiles read zqel/cli.py No loop over files in any subcommand; one compile_source per invocation
The LSP compiles grep -rn compile zqel/lsp/ Only re.compile — the analysis is regex-based
Supervised share of the example block pytest tests/test_examples_coverage.py --collect-only -q 184 nodes collected, 4 supervised

What follows, and what does not. It follows that 180 example compiles ran inside long-lived xdist workers, and that all five unsupervised crashes (§1.9) occurred there. It does not follow that supervising them would have prevented those crashes — a supervised node can crash too; what changes is that the crash is then typed, retried once, and attributed to one node instead of taking a worker's queue with it.

The mitigation history explains how the gap survived: each crash was answered by deselecting the node it hit (LMFit rust-compile, then LMFit backends, then both LM_Step cases). Every one of those was a response to an observed failure, and every subsequent crash moved to a node that was not on the list. The list was never going to converge, because node identity was never the cause.

1.11 — The crash has an upstream cause: a fixed use-after-free in Z3 (2026-09-03)

Raised by Michael Protogerakis. Every element below is verifiable with the command beside it; nothing here is inference.

The upstream fix

Fact Source
Commit 6e1103737, 2026-08-31: "Fix use-after-free in asserted_formulas::assert_expr during preprocessing rewrite (#10707)" gh api repos/Z3Prover/z3/commits/6e1103737
It changes one file, src/solver/assertions/asserted_formulas.cpp, +4/−3 lines same
Upstream's own root cause: "assert_expr called m_rewriter(e, r, pr) and later read e (has_quantifiers(e)), but e could be freed when r was reassigned by the rewriter" commit message
Reported as issue #10704, found by ASan on seq_rewriter/seq_monadic paths commit message
Not in any stable release: 5.0.0 (2026-07-17) and 5.1.0 (2026-08-16) both predate it gh api repos/Z3Prover/z3/releases

That the vulnerable code is what we run

We pin z3-solver==4.16.0 (requirements-dev.txt), released 2026-02-19. Its assert_expr reads verbatim:

151: void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
154:     expr_ref   r(e, m);            // r holds a reference to e
166:         m_rewriter(e, r, pr);      // reassigns r — e may die here
168:         if (e == r)                // reads a possibly dead pointer
176:     m_has_quantifiers |= ::has_quantifiers(e);   // dereferences it

Retrieved with gh api "repos/Z3Prover/z3/contents/src/solver/assertions/asserted_formulas.cpp?ref=z3-4.16.0". Line 176 executes on every call, not only when proofs are enabled.

That this is where our crashes are

The recorded SIGSEGV stacks end in th_rewriter -> asserted_formulas::assert_expr -> Z3_solver_assert (§1.2 and .zqel-handover/findings-register.md). That is the same function, reached through the same rewriter call the upstream commit names as the root cause.

What this explains that nothing else did

These were listed in §4 as open questions. Each follows from a use-after-free, and none of them followed from the teardown-race hypothesis:

  • Three different allocation sites (§1.2). Freed memory is reused by whatever allocates next, so the fault surfaces wherever the reused block is touched — the site is not a property of the bug.
  • The heisenbug (§1.5): ~78 crash-free runs under gdb against 6 of 7 dead uninstrumented suite runs. A debugger changes allocation timing and reuse, which is exactly what decides whether a dangling read hits a recycled block.
  • Load correlation. Contention changes allocation patterns; it does not change a teardown race's window in any way we could name.
  • Content independence (§2): a crash on a Markdown-only PR. The bug is in generic assert-time rewriting, not in any construct of ours.

What this does NOT explain — and a correction

Inference I1 in §3 read: "the hang and the crash are one mechanism, two outcomes (plausible, not proven)". This finding is evidence against it, and it is recorded as such rather than quietly dropped:

  • The crash now has a specific, documented, upstream-confirmed cause in assert_expr, on the assert path.
  • The hang (§1.1) was captured twice with full backtraces: the main thread in ast_manager::~ast_manager() under Z3_del_context, two scoped_timer threads asleep. That is the teardown path, a different phase, and this commit does not touch it.

The honest reading is that we have two phenomena, not one, and that the shared scoped_timer observation linked them by coincidence of context rather than by mechanism. The hang stays open.

Consequences already drawn

  • nix/patches/z3-4.16.0-asserted-formulas-uaf.patch carries the upstream diff, verified to apply cleanly to the pinned 4.16.0 source. Carrying the patch rather than bumping to 5.1.0 keeps Z3's semantic identity fixed: the change adds a scoped expr_ref and reads the guarded reference, and touches no rewriting behaviour.
  • This does not retract PI-2b. A supervised node that crashes is still typed, retried and attributed; the patch removes a cause, the supervision removes the blast radius. Neither substitutes for the other, and until a patched build has run the gates, the patch is a hypothesis about our crashes — a well-supported one, but our own evidence for it is the stack match, not a reproduction.

2. Refuted hypotheses

Listed with what refuted them, so they do not come back.

hypothesis refuted by
Huge rational literals (RealVal on big fractions) drive the crash measured: the atomic-literal branch changed nothing; the crash persisted, and the Python frame varies between runs
Our watchdog abandons a context and corrupts it O3a containment shipped; crashes continued unchanged
Different Z3 builds between runs identity step records one pinned build (§1.9)
A GC race in the Python bindings crash occurs with the same shape when no zqel-side collection is pending
fork() corrupts the parent review: copy-on-write; the parent's heap is not written by the child
The crash is bound to a specific Z3 API or expression content three captures show three different allocation sites (§1.2)
O27 (PRE across composition) caused the recent crashes LMFit.zqel and LM_Step.zqel contain zero PRE occurrences; the fix does not touch their compile path
Memory exhaustion on the runners free and dmesg at the time of four aborts: 1 of 8 GB used, zero OOM kills (§1.8)

3. Inferences — labelled as such

These are not facts. They are the readings the evidence supports, kept separate on purpose.

  • I1 — one mechanism, two outcomes (plausible, not proven). The hang (§1.1) is a teardown race between the timer pool and context destruction; the crash (§1.2) shows the same two timer threads and allocator-adjacent frames. That the two are the same mechanism is the most economical reading, but no capture shows the crash and the destruction in one trace. Superseded 2026-09-03 (§1.11). The crash now has a specific, upstream-confirmed cause on the assert path; the hang sits on the teardown path, which that fix does not touch. The shared scoped_timer observation linked the two by context, not by mechanism. Read as two phenomena; the hang stays open.
  • I2 — contention correlates with crash frequency (supported). The four-way concurrent gate produced four aborts (§1.8); the diagnosis job's removal from ordinary gates (PR #38) was followed by a run of fully green gates. Correlation is well documented; no controlled experiment isolates it.
  • I3 — instrumentation changes timing (supported). §1.4 is consistent with ptrace serialising threads, which would suppress a race. Not independently verified.

4. Open questions

  • ~~What exactly is corrupted, and by whom?~~ Answered upstream (§1.11): asserted_formulas::assert_expr read e after the rewriter could drop its last reference. What stays open is whether that is the cause of our crashes specifically — the stacks match, but we have no reproduction of our own.
  • Why does the hang happen? Untouched by §1.11, still unexplained.
  • Is the crash rate a function of process lifetime, of concurrency, or of the number of solver contexts created? Not measured.
  • Does the crash occur with a strategy-free solver (SimpleSolver)? Not tested — a different solver would be a different verification semantics, so this was deliberately not pursued.

5. What was decided on this evidence

  • ADR PI-1 (process isolation at the compile boundary) — the timer pool cannot be removed from our side (§1.3), so the containment boundary is the process.
  • PI-2 — the four historically crashing nodes run in supervised processes with exactly one retry for SOLVER_CRASH (§1.7).
  • PR #38 — the non-gating diagnosis job left the ordinary gate path (§1.5, I2).
  • Sequential gating (2026-09-03) — after §1.8.
  • PI-2b (PR #80, 2026-09-03) — the whole example block leaves the parallel run and is enumerated node-by-node through the supervisor, after §1.10 showed that 4 of 184 nodes were covered. Proven locally: all 184 nodes green in fresh supervised processes.
  • Z3 patch — MERGED 2026-09-03 (PR #81, issue #79, main 52466082). The pinned 4.16.0 is built from its own tag with the upstream use-after-free fix applied, rather than bumped to 5.1.0, so the semantic authority stays fixed. CI installs it as its own named step and the suite runs with ZQEL_REQUIRE_PATCHED_Z3=1, so a broken install fails the gate instead of passing quietly. The build itself compiled cleanly on Linux at the first real attempt; the four failures on the way there were all integration mistakes of ours (the devShell's LD_LIBRARY_PATH breaking a nested nix call, an unsuppressed installCheckPhase, and twice the wrong store output).
  • The assertion snapshot — MERGED with it. ProofEngine._sat captures the assertion set before the first check and hands that snapshot to the recovery, which previously read the post-check view and therefore reasoned about a subset. See §6.
  • Done, was "next": lift the whole parametrised test_examples_coverage block out of the parallel run and drive each node through the PI-2 supervisor; keep --max-worker-restart=0 for the rest, because a restart would hide a crash rather than report it.

6. A symptom that was NOT this crash family (2026-09-03)

Recorded here because it was suspected to be, and the suspicion shaped a day of work.

TestSolverStateInvariance::test_no_recovery_unknown_leaves_solver_untouched failed intermittently on Linux runners with a shrinking assertion count — assert (0, 0) == (2, 0). A solver that loses its assertions is exactly what a heap use-after-free looks like when it does not segfault, and §1.11 had just named such a bug in the very function our crash stacks end in.

It was not that. The cause, found by Michael Protogerakis in the Z3 sources and then reproduced deterministically with no threads and no wall-clock race: after an unknown verdict Z3's strategic solver reports the remaining tactic goal rather than the assertions that were added, and a neutral push()/pop() restores the view at once — which memory corruption cannot do.

Measured before believing it: the patch does not change that failure rate (14/160 unpatched against 17/160 patched, one machine, back to back).

Two consequences for this dossier:

  • Inference I-B — that this and the segfault family are different problems — moves from supported to confirmed.
  • The methodological point is the one worth keeping: a shared symptom class is not a shared mechanism. The dossier had to make the same correction once before, about its own inference I1.

Full evidence: docs/solver-state-invariance-flake.md.

Nachtrag 2026-09-04: der Eigenbau in diesem Dossier gibt es nicht mehr

Der Text oben beschreibt den Stand seiner Entstehung und bleibt unverändert — er ist Befundprotokoll, nicht Beschreibung des heutigen Aufbaus. Zwei seiner Aussagen gelten aber nicht mehr, und wer ihn liest, soll das hier finden:

Das gepinnte 4.16 wird nicht mehr aus dem eigenen Tag gebaut. Seit #124 kommt Z3 als gepinntes Nightly-Artefakt, das den Upstream-Fix von Haus aus trägt. install_patched_libz3.sh, der CI-Schritt, der Flake-Hook und nix/patches/ sind entfernt. Der Grund war nicht der Absturz — den hat Watchdog v2 beendet —, sondern #121: auf macOS war der Patch nicht baubar, dort lief also die ungepatchte Bibliothek, während CI die gepatchte testete.

Die Assertion-Sicht verhält sich unter 5.1 anders. Der Abschnitt zur Momentaufnahme bleibt richtig in seiner Begründung, aber nach unknown ist die verkürzte Sicht jetzt eine Umschreibung und keine Teilmenge: 5.1 sortiert kommutative Operanden um, sodass die überlebende Formel dieselbe Aussage macht, aber nicht mehr derselbe Term ist. Festgehalten in tests/test_gsc_adversarial.py.

Nachtrag 2026-09-04: die Variable in diesem Dossier gibt es nicht mehr

ZQEL_REQUIRE_PATCHED_Z3 erzwang, dass der Pin auf die selbst gebaute, gepatchte libz3 im Gate nicht übersprungen werden darf. Dieser Eigenbau ist entfallen: Z3 kommt jetzt als gepinntes Nightly-Artefakt, das den Fix upstream trägt, und an die Stelle der Variable ist ZQEL_REQUIRE_PINNED_Z3 getreten.

Der Text oben bleibt unverändert, weil er beschreibt, was damals galt. Er ist Befundprotokoll, keine Beschreibung des heutigen Aufbaus.

Nachtrag 2026-09-04: operativ geschlossen, und wo das Diagnosegerüst liegt

Die Auflage aus #62 — nach dem Watchdog-v2-Merge reguläre Gates beobachten, statt ein A/B im Labor zu bauen, dessen einziger Unterschied der Watchdog ist — ist erfüllt und gemessen, nicht erinnert:

31 vollständig gelaufene grüne Suite-Gates seit dem Watchdog-v2-Merge (78e01820, 2026-09-04 09:28), null native Absturzereignisse. Der jüngste Lauf mit Ereignissen ist Run 680 (#660, 14706035, 09:18:24) — zehn Minuten davor. Die vollständige Tabelle mit Run-IDs, Job-IDs, SHAs und Daten steht als Kommentar in #62; erzeugt hat sie scripts/gate_telemetry.py, mit dem sie jederzeit neu erhoben werden kann.

Die Formulierung, in der das gilt: durch vertragskonforme Threadanordnung beseitigt, historische Einzelcrashes nicht kausal reproduziert. Die z3-5.1-Umstellung (0b8fcebe, 10:41) liegt innerhalb dieses sauberen Fensters und ist dadurch nicht als Ursache belegt; sie war aus einem anderen Grund nötig (#121).

Das Diagnosegerüst wird nicht gemergt. Es hat seinen Zweck erfüllt und gehört nicht in den Hauptzweig — aber es soll auffindbar bleiben, falls die Familie zurückkehrt. Die beiden Zweige sind deshalb als Tags festgehalten und als Zweige gelöscht:

Tag Was darin steht
o3b-thread-diagnostics zählt die Threads des Watchdogs und schaltet einen kontrollierten Vergleichsmodus frei
o3c-soft-timeout macht Z3s Soft-Timeout als Quelle nativer Threads schaltbar, samt der 2×2-Messung unter gdb

Ein Tag statt eines Zweigs, weil ein gelöschter Zweig seine Commits irgendwann unerreichbar macht — „die Historie bewahrt es" stimmt nur, solange etwas darauf zeigt.

Eine Zählregel, die beim Erheben dieser Zahlen nötig wurde. Wer im Log jede Zeile zählt, die einen Absturz erwähnt, überzählt massiv: ein pytest-Traceback druckt die Quellzeile des raise, also erzeugte ein einziger Segfault zwölf Zeilen mit native-solver-abandoned und zehn mit NativeContextPoisoned. Gezählt werden nur Zeilen, die am Ereignis entstehen (rc=-11, CPythons Fatal Python error, ein abgestürzter xdist-Worker); und auch die sind Zeilen, nicht Vorfälle — ein Segfault erscheint normalerweise zweimal, weil CPython ihn meldet und die Aufsicht ihn danach mit Testnamen wiederholt. Zweite Regel: ein Lauf mit Absturz kann trotzdem success sein, weil die Aufsicht einmal wiederholt. Das ist die Recovery-Rate und kein fehlender Absturz.