SIGSEGV inside the MBQI model checker's auxiliary `context::check` — fault site varies per run (looks like state corruption); regression, 4.16.0 is clean

[headinthebox]

Summary

z3 5.0.0 segfaults on the attached SMT-LIB2 file. The same file, same machine, same options runs to
completion on 4.16.0, so this looks like a regression introduced after 4.16.0.

The file is a sequence of 15 (push 1) … (check-sat) (pop 1) blocks over floating-point arrays with
quantified assertions. Expected behaviour is 15 sat/unsat/unknown answers; actual behaviour is 14
answers followed by SIGSEGV on the 15th.

The part that seems most diagnostic: the crash is deterministic in when it happens — every run
dies on the 15th check-sat, after exactly 14 answers — but not in where. Three consecutive runs
of the identical file produced three different fault sites, each a bad-pointer access of a different
smt::context structure, and all three reached through the same path: MBQI's model checker running
its auxiliary context::check. One of the three is a virtual call through an apparently freed
justification object. That pattern reads like the solver state being corrupted inside the model
checker's auxiliary context, with the process then faulting wherever that state is next touched, rather
than like a single missing null check.

Reproduce

z3 -smt2 smt.random_seed=0 rlimit=40000000 smt.arith.solver=6 repro_z3_500_mbqi_segv.smt2

Deterministic: 3 of 3 runs crash after printing exactly 14 answers.

Expected vs actual

• Expected: 15 lines of sat / unsat / unknown, exit 0.
• Actual: 14 lines, then SIGSEGV (exit 139).

The three fault sites (three consecutive runs, identical input)

Every one of them has this common suffix, which is where I would start looking:

smt::context::check(unsigned int, expr* const*, bool)          <- MBQI's auxiliary check
smt::model_checker::check(quantifier*)
smt::model_checker::check_quantifiers(bool&, unsigned int&)
smt::model_checker::check(proto_model*, obj_map<smt::enode, app*> const&)
smt::default_qm_plugin::check_model(proto_model*, obj_map<smt::enode, app*> const&)
smt::context::restart(lbool&, unsigned int)
smt::context::search()
smt::context::check(unsigned int, expr* const*, bool)
solver_na2as::check_sat_core → combined_solver::check_sat_core → solver::check_sat
cmd_context::check_sat → smt2::parser::parse_check_sat

and they differ only above it:

(1) null expr* in the generation-cache traversal — si_code SEGV_ACCERR, si_addr 0x0c:

smt::context::cache_generation(expr*, unsigned int)      <- faults
smt::context::cache_generation(unsigned int)
smt::context::pop_scope_core(unsigned int)
smt::context::mk_unsat_core(lbool)

Disassembly at the faulting offset (+0x80, 5.0.0 arm64) shows the worklist popped and dereferenced
with no guard:

ldr  x9,  [sp, #0x20]        ; worklist buffer
sub  w8,  w8, #0x1
ldr  x21, [x9, w8, uxtw #3]  ; n = todo[--count]
ldr  w8,  [x21, #0xc]        ; <-- faults; x21 == nullptr, +0xc is the ast id field

si_addr = 0x0c matches that offset exactly.

(2) null enode in boolean propagation — si_addr 0x0:

smt::context::propagate_bool_var_enode(unsigned int)+0x38  <- faults
smt::context::propagate_atoms() → propagate() → bounded_search() → search()

(3) virtual call through an apparently freed justification:

vtable for smt::eq_propagation_justification              <- faults
smt::justification::has_del_eh() const
smt::theory_bv::assign_eh(unsigned int, bool)
smt::context::propagate_atoms() → propagate() → bounded_search() → search()

(3) is the one that makes me think "corrupted/freed state" rather than "missing null check": it is a
dispatch through a vtable pointer, not a read of a container slot.

Version matrix (same machine, same file, same options)

z3	result
5.0.0 (official release binary, arm64 macOS)	SIGSEGV, 3/3
4.16.0 (Homebrew build)	completes normally, all 15 answers

Options that avoid it

option change	result
smt.mbqi=false	no crash
default options (no smt.random_seed / rlimit / smt.arith.solver)	no crash
smt.arith.solver=2	no crash
smt.random_seed=1	still crashes — not seed-specific
no rlimit	no crash

smt.mbqi=false avoiding it is consistent with the stack: every crashing path goes through the MBQI
model checker's auxiliary context.

Environment

• macOS 26.5.2 (build 25F84), Darwin 25.5.0, arm64 (Mac15,14).
• z3 5.0.0: the official release binary z3-5.0.0-arm64-osx-13.3 (statically linked). The same crash,
  same stack, also occurs in the libz3.dylib from that same release when driven through the C API.
• z3 4.16.0: Homebrew z3 4.16.0.

Notes on the repro

• It is 1-minimal at block granularity: delta-debugged to a fixpoint, and removing any single one of
  the remaining 15 (push … check-sat … pop) blocks makes the crash disappear. It is not reducible
  further by dropping checks.
• It is sensitive to symbol names: alpha-renaming the declarations suppresses it (25 renamings tried, 0
  reproduced), which suggests the trigger is a particular hash/term ordering rather than anything
  special about the formulas — consistent with an internal invariant that is violated only on some
  orderings.
• I could not get it under a debugger on this machine (attach is blocked by the OS), so the fault
  detail above comes from the OS crash reports plus disassembly, not from a live session. Three crash
  reports are attached, one per fault site.
• Found while developing an SMT-based program verifier; the file is machine-generated verification
  conditions, reduced.

[chadbrewbaker]

Fable suggested debug plan. SASSERT, rlimit, and ASAN all seem sane. Ping me if this gets hairy and I will throw more resources at it.

---

Dug into this by diffing z3-4.16.0..z3-5.0.0 restricted to the code under the three crash stacks. This is static analysis (we haven't caught it under a sanitizer yet), but it narrows the search enough to make a debug build fail fast at the root cause instead of 40M instructions later. Line numbers below are against the z3-5.0.0 tag.

One housekeeping note first: the linked draft PR #10392's only commit ("Initial plan", 9b54e8a) contains no file changes — flagging so nobody assumes a fix is already in flight.

Where the diff and the crashes intersect

The dominant 4.16→5.0 change under the crashing stacks is the move of instantiation generations from per-enode storage onto congruence-class roots, tracked through merges/unmerges (m_r1_parent_generations, merge_cgc_generations, set_generation_sticky, get_generation(e) = get_cg_root(e)->m_generation). Three spots in that machinery are unguarded in release builds and each is capable of producing exactly the "state corrupted, faults at next touch" pattern reported above:

1. Positional replay of parent generations can desync (release-mode OOB + cg_table double-insert).
remove_parents_from_cg_table records (parent, generation) pairs in iteration order ([smt_context.cpp#L626](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L626)); reinsert_parents_into_cg_table consumes them positionally with unchecked indexing:

// smt_context.cpp:695
auto [p, g] = m_r1_parent_generations[generation_cache_idx++];
SASSERT(p == parent);   // line 696 — only order check, debug-only

The record/replay correspondence hangs entirely on enode mark bits being perfectly balanced between the two passes. If a mark ever leaks (see point 3), the replay pass consumes entries that were never recorded → out-of-bounds read, a garbage value written into parent->m_generation, and m_cg_table.insert(parent) on a node that was never erased — corrupting the congruence table itself. A corrupted cg_table then manifests exactly as observed: null expr* in the cache_generation worklist (fault 1), null enode in propagate_bool_var_enode (fault 2), garbage justification vtable (fault 3). The sibling loop in undo_add_eq is bounds-guarded and carries a dummy_generation = 100000 sentinel with a "would be hell to debug" comment ([L1042–L1047](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L1042-L1047)), which suggests the delicacy of this choreography is already known.

2. get_cg_root dereferences a possible-null find result — including on a write path.

// smt_context.h:1231
enode * get_cg_root(enode * n) const {
    ...
    auto r = m_cg_table.find(n);   // returns nullptr on miss
    SASSERT(r != nullptr);         // line 1239 — debug-only
    return r;
}

get_generation reads ->m_generation through this unchecked, and set_generation (smt_internalizer.cpp:117) writes 4 bytes through it. If the "every non-cgr node has a table entry" invariant slips even transiently, the write path scribbles into whatever the stale/garbage pointer aims at. New in 5.0 — 4.16 never chased the table for generations.

3. The add_eq abort path now discards generation trails and leaks marks.
The catch (...) { m_trail_stack.shrink(old_trail_size); throw; } rollback ([L482](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L482), [L592](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L592)) predates 5.0, but 5.0 changed what it drops: reinsert_parents_into_cg_table now pushes merge_cgc_generations_trails, and add_eq_trail is deliberately pushed after reinsert. An exception between remove_parents_from_cg_table and the end of reinsert now (a) discards the trails that restore class generations and (b) leaves parent marks set, arming the desync in point 1 for every later merge touching those parents.

Why this matches the reported repro conditions

• rlimit required, crash on the 15th block: cancellation-driven exceptions start unwinding through hot paths only when the limit is nearly exhausted — that's the arming mechanism for point 3.
• Alpha-renaming suppresses it: cg_table hash/iteration order determines which parents collide and in which order the record/replay runs.
• smt.mbqi=false avoids it: the MBQI auxiliary context does the heaviest merge/backtrack churn (push/check/pop per quantifier per round, one context reused across all 15 blocks).
• Fault 1's exact location: cache_generation(new_lvl) is the first statement of pop_scope_core ([L2536](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L2536)), reached via mk_unsat_core → pop_to_base_lvl ([L3581](https://github.com/Z3Prover/z3/blob/z3-5.0.0/src/smt/smt_context.cpp#L3581)) on every unsat aux round — it's simply the first code to walk the already-corrupted structures after the search.

(We also audited the sticky-generation table lifecycle — insert at smt_internalizer.cpp:111, erase in undo_mk_enode at :1162 — and the trail-stack scope refactor in push_scope/pop_scope_core; both look balanced.)

SASSERTs to watch in a debug build

Running the attached repro on an assertion build should fire one of these near the true root cause, in rough priority order:

1. SASSERT(p == parent) — smt_context.cpp:696 (replay desync)
2. SASSERT(r != nullptr) — smt_context.h:1239 (get_cg_root miss)
3. SASSERT(m_cg_table.contains_ptr(parent)) — smt_context.cpp:704 / :1000 / :1042 (table membership invariants)

Suggested instrumented runs

# assertions
cmake -B build-dbg -DCMAKE_BUILD_TYPE=Debug -G Ninja && ninja -C build-dbg
# assertions + ASan/UBSan
cmake -B build-asan -DCMAKE_BUILD_TYPE=Debug -G Ninja \
  -DCMAKE_CXX_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer" && ninja -C build-asan
ASAN_OPTIONS=abort_on_error=1:detect_stack_use_after_return=1 \
  ./build-asan/z3 -smt2 smt.random_seed=0 rlimit=40000000 smt.arith.solver=6 repro_z3_500_mbqi_segv.smt2

Corpus, in order of expected yield:

1. The attached repro as-is, on both builds.
2. rlimit × seed sweep of the repro — since cancellation timing appears to be the arming mechanism, sweep rlimit around the reported value (e.g., 30M–45M in 1M steps) × smt.random_seed 0–20 under ASan. Debug builds burn the rlimit differently, so the crash point will shift; the sweep re-finds it.
3. If the repro won't fire under instrumentation (order-sensitive): z3test regressions plus SMT-LIB quantified array/FP benchmarks, driven incrementally with (push)/(check-sat)/(pop) blocks, smt.mbqi=true smt.arith.solver=6, and a per-file rlimit binary-searched to land just below completion — i.e., deliberately forcing cancellation mid-MBQI, which is the regime this repro lives in.

Happy to test candidate patches against the repro. A cheap diagnostic hardening that converts the corruption into fail-fast (useful even before the real fix): bounds-check + VERIFY(p == parent) at smt_context.cpp:695, null-check in get_cg_root, and clearing parent marks in the add_eq catch block.

[NikolajBjorner]

Can Cebeci (@CanCebeci) - did you get a chance to look at this?

Pushing a PR with auto-generated fix, we can compare notes with above.

Implemented the #10385 fix in  smt_context : parent generations are now keyed by enode instead of replayed positionally, preventing stale marks from causing out-of-bounds reads and congruence-table corruption.

Note though:

The issue’s referenced SMT2 attachment is unavailable, so the exact reproducer could not be run.

The issue mentions a repro file, but I couldn't find it either.

[NikolajBjorner]

auto fix suggests parent generations need dedup to align vector and table views.

[NikolajBjorner]

headinthebox

z3 5.0.0 segfaults on the attached SMT-LIB2 file

There is no attached file (?)

[CanCebeci]

This looks tricky and I'm not sure the auto-suggested fix is enough (or needed). Using a table instead of a vector does not make the desync go away, it just prevents the segfault. It seems the root cause to address is that the add_eq abort leaks marks.

I'll take a deeper look as soon as I get the chance. The reproducer would be very helpful.

[chadbrewbaker]

This looks tricky

Very, I had to annotate it with some model checking software.

Sorry I corrupted the Opus 5 context window and would have to bring it up in a new VM to test, but here was the artifacts it generated if they are of any use. I will try to take another look tomorrow.

#!/usr/bin/env python3
"""Generate a pigeonhole-principle instance: PHP(n+1, n), unsat, and
exponential for CDCL.  Used only to make z3 run long enough to time out.

    python3 gen_php.py 12 > php.smt2
"""
import sys

n = int(sys.argv[1]) if len(sys.argv) > 1 else 12
pigeons, holes = n + 1, n

out = ["(set-logic QF_UF)", "(set-option :produce-models false)"]
for p in range(pigeons):
    for h in range(holes):
        out.append(f"(declare-const p{p}_{h} Bool)")
# every pigeon in some hole
for p in range(pigeons):
    out.append("(assert (or " + " ".join(f"p{p}_{h}" for h in range(holes)) + "))")
# no hole holds two pigeons
for h in range(holes):
    for a in range(pigeons):
        for b in range(a + 1, pigeons):
            out.append(f"(assert (or (not p{a}_{h}) (not p{b}_{h})))")
out.append("(check-sat)")
print("\n".join(out))

#!/usr/bin/env bash
# Regression test for: z3 exits 0 on timeout and on SIGXCPU.
#
#   ./test_timeout_exit_code.sh /path/to/z3
#
# Exit 0 if all cases pass.  Each case prints PASS/FAIL and the observed status.
# Before the patch, cases 1 and 2 FAIL (both observe exit 0).  After the patch,
# case 1 observes 102 (ERR_TIMEOUT) and case 2 dies by SIGXCPU (128+24 = 152 as
# reported by bash).
set -u
Z3=${1:-z3}
HERE=$(cd "$(dirname "$0")" && pwd)
WORK=$(mktemp -d); trap 'rm -rf "$WORK"' EXIT
fails=0

pass() { echo "PASS  $1"; }
fail() { echo "FAIL  $1"; fails=$((fails+1)); }

python3 "$HERE/gen_php.py" 12 > "$WORK/php.smt2"
: > "$WORK/trivial.smt2"
printf '(declare-const x Bool)\n(assert x)\n(check-sat)\n' > "$WORK/trivial.smt2"

# --- case 1: -T:n must not report success -----------------------------------
out=$(timeout 60 "$Z3" -T:3 "$WORK/php.smt2" 2>&1); rc=$?
if [ "$rc" -eq 0 ]; then
  fail "case 1  -T:3 exited 0 (expected non-zero; ERR_TIMEOUT=102).  stdout: $out"
elif [ "$rc" -eq 102 ]; then
  pass "case 1  -T:3 exited 102 (ERR_TIMEOUT)"
else
  fail "case 1  -T:3 exited $rc (expected 102)"
fi

# --- case 2: SIGXCPU must not report success --------------------------------
# Sent explicitly rather than via `ulimit -t`, which many containers refuse to
# lower.  This exercises the same handler (on_sigxcpu) with no privileges.
"$Z3" "$WORK/php.smt2" >"$WORK/x.out" 2>&1 &
pid=$!
sleep 2
kill -XCPU "$pid" 2>/dev/null
wait "$pid"; rc=$?
if [ "$rc" -eq 0 ]; then
  fail "case 2  SIGXCPU exited 0 (expected death by signal: 152 = 128+SIGXCPU)"
elif [ "$rc" -eq 152 ]; then
  pass "case 2  SIGXCPU killed the process (152 = 128+24)"
else
  fail "case 2  SIGXCPU produced exit $rc (expected 152)"
fi

# --- case 2b: the rlimit path, when the environment allows it ---------------
if ( ulimit -H -t 3 ) 2>/dev/null; then
  rc=$( ( ulimit -H -t 3; "$Z3" "$WORK/php.smt2" >/dev/null 2>&1; echo $? ) )
  if [ "$rc" -eq 0 ]; then
    fail "case 2b ulimit -t exited 0"
  else
    pass "case 2b ulimit -t exited $rc"
  fi
else
  echo "SKIP  case 2b  this environment will not lower RLIMIT_CPU"
fi

# --- case 3: control, an unrelated error code still flows through -----------
"$Z3" "$WORK/nope.smt2" >/dev/null 2>&1; rc=$?
if [ "$rc" -eq 108 ]; then
  pass "case 3  missing file exited 108 (ERR_OPEN_FILE)"
else
  fail "case 3  missing file exited $rc (expected 108)"
fi

# --- case 4: control, a normal run still exits 0 ----------------------------
"$Z3" "$WORK/trivial.smt2" >/dev/null 2>&1; rc=$?
if [ "$rc" -eq 0 ]; then
  pass "case 4  ordinary sat run exited 0"
else
  fail "case 4  ordinary sat run exited $rc (expected 0)"
fi

echo "---"
if [ "$fails" -eq 0 ]; then echo "all cases passed"; else echo "$fails case(s) failed"; fi
exit $((fails > 0))

diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index c8dbf56..7fe6861 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -33,7 +33,8 @@ bool g_display_model = false;
 static void on_timeout() {
     std::cout << "% SZS status Timeout\n";
     std::cout.flush();
-    _Exit(0);
+    // Non-zero: a timeout is not a successful run.  See util/error_codes.h.
+    _Exit(ERR_TIMEOUT);
 }
 
 namespace {
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 5599b15..70690d4 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -109,7 +109,10 @@ static void display_statistics() {
 
 static void on_timeout() {
     display_statistics();
-    _Exit(0);
+    // Non-zero: a timeout is not a successful run.  ERR_TIMEOUT is 102
+    // (util/error_codes.h) and was already the project's designated code for
+    // this condition; it simply had no path that reached the parent.
+    _Exit(ERR_TIMEOUT);
 }
 
 static void STD_CALL on_ctrl_c(int) {
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index c1bc41b..11d1675 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -56,7 +56,10 @@ static void display_statistics() {
 
 static void on_timeout() {
     display_statistics();
-    _Exit(0);
+    // Non-zero: a timeout is not a successful run.  ERR_TIMEOUT is 102
+    // (util/error_codes.h) and was already the project's designated code for
+    // this condition; it simply had no path that reached the parent.
+    _Exit(ERR_TIMEOUT);
 }
 
 static void STD_CALL on_ctrl_c(int) {
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 8813ed4..8cd5ee2 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -86,7 +86,10 @@ static void STD_CALL on_ctrl_c(int) {
 
 static void on_timeout() {
     display_statistics();
-    _Exit(0);
+    // Non-zero: a timeout is not a successful run.  ERR_TIMEOUT is 102
+    // (util/error_codes.h) and was already the project's designated code for
+    // this condition; it simply had no path that reached the parent.
+    _Exit(ERR_TIMEOUT);
 }
 
 static unsigned parse_opt(std::istream& in, opt_format f) {
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 008142c..c21f087 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -63,7 +63,10 @@ static void display_model() {
 
 static void on_timeout() {
     display_statistics();
-    _Exit(0);
+    // Non-zero: a timeout is not a successful run.  ERR_TIMEOUT is 102
+    // (util/error_codes.h) and was already the project's designated code for
+    // this condition; it simply had no path that reached the parent.
+    _Exit(ERR_TIMEOUT);
 }
 
 static void STD_CALL on_ctrl_c(int) {
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index f640db1..6320989 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -20,6 +20,9 @@ Revision History:
 --*/
 #include<iostream>
 #include<signal.h>
+#ifndef _WINDOWS
+#include<unistd.h>
+#endif
 #include "util/util.h"
 #include "util/timeout.h"
 #include "util/error_codes.h"
@@ -39,9 +42,24 @@ static void do_timeout() {
 
 #ifdef SIGXCPU
 // React to SIGXCPU (an external CPU limit, e.g. ulimit -t) like a -T timeout.
+//
+// This is a real signal handler, so it must be async-signal-safe.  It used to
+// call do_timeout(), which writes to std::cout and then calls g_on_timeout() --
+// and every shipped frontend's g_on_timeout walks live solver state to print
+// statistics and then calls _Exit(0).  None of that is async-signal-safe, and
+// the _Exit(0) meant the raise() below was unreachable, so a CPU-limit kill was
+// reported to the parent as a successful run.
+//
+// Restore the default disposition and re-raise, so the parent's waitpid()
+// reports WIFSIGNALED(SIGXCPU).  Only write(2), signal(2) and raise(3) are used
+// here; all three are async-signal-safe.  Nothing after raise() runs.
 static void STD_CALL on_sigxcpu(int) {
+#ifndef _WINDOWS
+    static const char msg[] = "timeout\n";
+    ssize_t n = write(STDOUT_FILENO, msg, sizeof(msg) - 1);
+    (void)n;
+#endif
     signal(SIGXCPU, SIG_DFL);
-    do_timeout();
     raise(SIGXCPU);
 }
 #endif
@@ -52,7 +70,19 @@ public:
     void operator()(event_handler_caller_t caller_id) override {
         m_caller_id = caller_id;
         do_timeout();
-        throw z3_error(ERR_TIMEOUT);
+        // do_timeout() normally does not return: every shipped frontend
+        // registers an on_timeout that ends the process.  It must end it with a
+        // NON-ZERO status -- see the frontends, which now use ERR_TIMEOUT.
+        //
+        // A `throw z3_error(ERR_TIMEOUT)` used to sit here.  It could never
+        // work: operator() is invoked from the scoped_timer's own thread
+        // (scoped_timer.cpp, thread_func), so the exception would unwind that
+        // thread, reach no handler, and call std::terminate().  The throw has
+        // been removed rather than left as a contradicted intention.
+        //
+        // If no frontend hook is registered we still must not fall through and
+        // let the run look successful.
+        _Exit(ERR_TIMEOUT);
     }
 };
 }

[headinthebox]

Apologies — the attachment did not survive the original filing. Here it is, with the crash reports:

https://gist.github.com/headinthebox/409af2e7feaa61b02e5d913c2865423b

• repro_z3_500_mbqi_segv.smt2 — the 1-minimal file (15 push … check-sat … pop blocks; removing any single block makes the crash disappear)
• stack_standalone_z3.txt — backtraces from three runs, one per observed fault site
• crash_report_2052{33,44,57}.ips — the corresponding macOS crash reports

Invocation:

z3 -smt2 smt.random_seed=0 rlimit=40000000 smt.arith.solver=6 repro_z3_500_mbqi_segv.smt2

Observed on z3 5.0.0, macOS arm64. Same file, same options, same machine runs to completion on 4.16.0. The fault site varies per run (three distinct sites captured above), which is what made this look like state corruption rather than a single bad dereference — consistent with Can Cebeci (@CanCebeci)'s read that the vector→table change masks a desync rather than fixing it.

Happy to re-run against a patched build.

[NikolajBjorner]

This looks tricky

Very, I had to annotate it with some model checking software.

Sorry I corrupted the Opus 5 context window and would have to bring it up in a new VM to test, but here was the artifacts it generated if they are of any use. I will try to take another look tomorrow.

#!/usr/bin/env python3
"""Generate a pigeonhole-principle instance: PHP(n+1, n), unsat, and
exponential for CDCL. Used only to make z3 run long enough to time out.

python3 gen_php.py 12 > php.smt2

"""
import sys

n = int(sys.argv[1]) if len(sys.argv) > 1 else 12
pigeons, holes = n + 1, n

out = ["(set-logic QF_UF)", "(set-option :produce-models false)"]
for p in range(pigeons):
for h in range(holes):
out.append(f"(declare-const p{p}_{h} Bool)")

every pigeon in some hole

for p in range(pigeons):
out.append("(assert (or " + " ".join(f"p{p}_{h}" for h in range(holes)) + "))")

no hole holds two pigeons

for h in range(holes):
for a in range(pigeons):
for b in range(a + 1, pigeons):
out.append(f"(assert (or (not p{a}{h}) (not p{b}{h})))")
out.append("(check-sat)")
print("\n".join(out))
#!/usr/bin/env bash

Regression test for: z3 exits 0 on timeout and on SIGXCPU.

./test_timeout_exit_code.sh /path/to/z3

Exit 0 if all cases pass. Each case prints PASS/FAIL and the observed status.

Before the patch, cases 1 and 2 FAIL (both observe exit 0). After the patch,

case 1 observes 102 (ERR_TIMEOUT) and case 2 dies by SIGXCPU (128+24 = 152 as

reported by bash).

set -u
Z3=${1:-z3}
HERE=$(cd "$(dirname "$0")" && pwd)
WORK=$(mktemp -d); trap 'rm -rf "$WORK"' EXIT
fails=0

pass() { echo "PASS $1"; }
fail() { echo "FAIL $1"; fails=$((fails+1)); }

python3 "$HERE/gen_php.py" 12 > "$WORK/php.smt2"
: > "$WORK/trivial.smt2"
printf '(declare-const x Bool)\n(assert x)\n(check-sat)\n' > "$WORK/trivial.smt2"

--- case 1: -T:n must not report success -----------------------------------

out=$(timeout 60 "$Z3" -T:3 "$WORK/php.smt2" 2>&1); rc=$?
if [ "$rc" -eq 0 ]; then
fail "case 1 -T:3 exited 0 (expected non-zero; ERR_TIMEOUT=102). stdout: $out"
elif [ "$rc" -eq 102 ]; then
pass "case 1 -T:3 exited 102 (ERR_TIMEOUT)"
else
fail "case 1 -T:3 exited $rc (expected 102)"
fi

--- case 2: SIGXCPU must not report success --------------------------------

Sent explicitly rather than via ulimit -t, which many containers refuse to

lower. This exercises the same handler (on_sigxcpu) with no privileges.

"$Z3" "$WORK/php.smt2" >"$WORK/x.out" 2>&1 &
pid=$!
sleep 2
kill -XCPU "$pid" 2>/dev/null
wait "$pid"; rc=$?
if [ "$rc" -eq 0 ]; then
fail "case 2 SIGXCPU exited 0 (expected death by signal: 152 = 128+SIGXCPU)"
elif [ "$rc" -eq 152 ]; then
pass "case 2 SIGXCPU killed the process (152 = 128+24)"
else
fail "case 2 SIGXCPU produced exit $rc (expected 152)"
fi

--- case 2b: the rlimit path, when the environment allows it ---------------

if ( ulimit -H -t 3 ) 2>/dev/null; then
rc=$( ( ulimit -H -t 3; "$Z3" "$WORK/php.smt2" >/dev/null 2>&1; echo $? ) )
if [ "$rc" -eq 0 ]; then
fail "case 2b ulimit -t exited 0"
else
pass "case 2b ulimit -t exited $rc"
fi
else
echo "SKIP case 2b this environment will not lower RLIMIT_CPU"
fi

--- case 3: control, an unrelated error code still flows through -----------

"$Z3" "$WORK/nope.smt2" >/dev/null 2>&1; rc=$?
if [ "$rc" -eq 108 ]; then
pass "case 3 missing file exited 108 (ERR_OPEN_FILE)"
else
fail "case 3 missing file exited $rc (expected 108)"
fi

--- case 4: control, a normal run still exits 0 ----------------------------

"$Z3" "$WORK/trivial.smt2" >/dev/null 2>&1; rc=$?
if [ "$rc" -eq 0 ]; then
pass "case 4 ordinary sat run exited 0"
else
fail "case 4 ordinary sat run exited $rc (expected 0)"
fi

echo "---"
if [ "$fails" -eq 0 ]; then echo "all cases passed"; else echo "$fails case(s) failed"; fi
exit $((fails > 0))
diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index c8dbf56..7fe6861 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -33,7 +33,8 @@ bool g_display_model = false;
static void on_timeout() {
std::cout << "% SZS status Timeout\n";
std::cout.flush();

• _Exit(0);

• // Non-zero: a timeout is not a successful run. See util/error_codes.h.
• _Exit(ERR_TIMEOUT);
  }

namespace {
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 5599b15..70690d4 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -109,7 +109,10 @@ static void display_statistics() {

static void on_timeout() {
display_statistics();

• _Exit(0);

• // Non-zero: a timeout is not a successful run. ERR_TIMEOUT is 102
• // (util/error_codes.h) and was already the project's designated code for
• // this condition; it simply had no path that reached the parent.
• _Exit(ERR_TIMEOUT);
  }

static void STD_CALL on_ctrl_c(int) {
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index c1bc41b..11d1675 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -56,7 +56,10 @@ static void display_statistics() {

static void on_timeout() {
display_statistics();

• _Exit(0);

• // Non-zero: a timeout is not a successful run. ERR_TIMEOUT is 102
• // (util/error_codes.h) and was already the project's designated code for
• // this condition; it simply had no path that reached the parent.
• _Exit(ERR_TIMEOUT);
  }

static void STD_CALL on_ctrl_c(int) {
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 8813ed4..8cd5ee2 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -86,7 +86,10 @@ static void STD_CALL on_ctrl_c(int) {

static void on_timeout() {
display_statistics();

• _Exit(0);

• // Non-zero: a timeout is not a successful run. ERR_TIMEOUT is 102
• // (util/error_codes.h) and was already the project's designated code for
• // this condition; it simply had no path that reached the parent.
• _Exit(ERR_TIMEOUT);
  }

static unsigned parse_opt(std::istream& in, opt_format f) {
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 008142c..c21f087 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -63,7 +63,10 @@ static void display_model() {

static void on_timeout() {
display_statistics();

• _Exit(0);

• // Non-zero: a timeout is not a successful run. ERR_TIMEOUT is 102
• // (util/error_codes.h) and was already the project's designated code for
• // this condition; it simply had no path that reached the parent.
• _Exit(ERR_TIMEOUT);
  }

static void STD_CALL on_ctrl_c(int) {
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index f640db1..6320989 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -20,6 +20,9 @@ Revision History:
--*/
#include
#include<signal.h>
+#ifndef _WINDOWS
+#include<unistd.h>
+#endif
#include "util/util.h"
#include "util/timeout.h"
#include "util/error_codes.h"
@@ -39,9 +42,24 @@ static void do_timeout() {

#ifdef SIGXCPU
// React to SIGXCPU (an external CPU limit, e.g. ulimit -t) like a -T timeout.
+//
+// This is a real signal handler, so it must be async-signal-safe. It used to
+// call do_timeout(), which writes to std::cout and then calls g_on_timeout() --
+// and every shipped frontend's g_on_timeout walks live solver state to print
+// statistics and then calls _Exit(0). None of that is async-signal-safe, and
+// the _Exit(0) meant the raise() below was unreachable, so a CPU-limit kill was
+// reported to the parent as a successful run.
+//
+// Restore the default disposition and re-raise, so the parent's waitpid()
+// reports WIFSIGNALED(SIGXCPU). Only write(2), signal(2) and raise(3) are used
+// here; all three are async-signal-safe. Nothing after raise() runs.
static void STD_CALL on_sigxcpu(int) {
+#ifndef _WINDOWS

• static const char msg[] = "timeout\n";
• ssize_t n = write(STDOUT_FILENO, msg, sizeof(msg) - 1);
• (void)n;
  +#endif
  signal(SIGXCPU, SIG_DFL);

• do_timeout();
  raise(SIGXCPU);
  }
  #endif
  @@ -52,7 +70,19 @@ public:
  void operator()(event_handler_caller_t caller_id) override {
  m_caller_id = caller_id;
  do_timeout();

•    throw z3_error(ERR_TIMEOUT);
  

•    // do_timeout() normally does not return: every shipped frontend
  

•    // registers an on_timeout that ends the process.  It must end it with a
  

•    // NON-ZERO status -- see the frontends, which now use ERR_TIMEOUT.
  

•    //
  

•    // A `throw z3_error(ERR_TIMEOUT)` used to sit here.  It could never
  

•    // work: operator() is invoked from the scoped_timer's own thread
  

•    // (scoped_timer.cpp, thread_func), so the exception would unwind that
  

•    // thread, reach no handler, and call std::terminate().  The throw has
  

•    // been removed rather than left as a contradicted intention.
  

•    //
  

•    // If no frontend hook is registered we still must not fall through and
  

•    // let the run look successful.
  

•    _Exit(ERR_TIMEOUT);
  

  }
  };
  }

Thanks for engaging!
Quite a firehose of AI generated investigation.
I can see it includes changes to tptp_frontend.cpp which is entirely unrelated to this bug.
It is highly likely the tptp_frontend can use several more iterations of agent fixups. That code was so far entirely agent created (the TPTP format itself is overloaded with features so using an automatic harness is more productive and less failure prone than manual coding on my side). That is not to say the tptp_frontend AI-slop code that got created along the way had to be heavily revised.