mirror of
https://github.com/Z3Prover/z3
synced 2026-07-26 17:02:38 +00:00
24f495f95c
## Problem
egressions/smt2/10220.smt2 (datatype + nonlinear integer arithmetic over
`SBVRational`, expected `unsat`) crashes with an ACCESS_VIOLATION (issue
#10220). The crash only occurs with the default `theory_lra`
(`arith.solver=6`) and is independent of `arith.nl`.
## Root cause
Debug build gives a clean stack: a `SASSERT(n)` violation / null
dereference in `smt::relevancy_propagator_imp::is_relevant_core` reached
from `theory_lra::set_conflict_or_lemma ->
ctx().mark_as_relevant(literal)`. The literal's boolean variable has
`bool_var2expr(v) == nullptr`.
Tracing showed the same nla lemma core being processed twice — first at
scope 6, then, after a backtrack, again at scope 3 — where the bound
atoms internalized to build the lemma had their boolean variables
deleted by the pop:
\\\
SCOL scope=6 core=[32 27 35 30 6 14 ]
SCOL scope=3 core=[32*NULL* 27 35*NULL* 30 6 14 ]
\\\
Commit
|
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||