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

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)

Options that avoid it

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.