mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

fix #8023: don't skip axiom clauses with non-base-level satisfying literals

Browse source 
The add_axiom optimization that skips adding clauses when a literal is
already true was unsound: the satisfying literal could be retracted by
backtracking, leaving the axiom clause missing. This caused the solver
to miss propagations, e.g., not propagating indexof(a,s) = -1 when
contains(a,s) becomes false after backtracking.

Fix: only skip the clause if the satisfying literal is assigned at
base level (scope 0), where it can never be retracted.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-17 07:22:23 -10:00 • committed by Lev Nachmanson
parent 3745bdd43b
commit 09c13a75e3
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_seq.cpp
View file

@ -2976,7 +2976,7 @@ void theory_seq::add_axiom(literal_vector & lits) {
TRACE(seq, ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";);
for (literal lit : lits)
if (ctx.get_assignment(lit) == l_true)
if (ctx.get_assignment(lit) == l_true && ctx.get_assign_level(lit) == 0)
return;
for (literal lit : lits)