From 09c13a75e386aa5eda4bcae5681080159f0fc383 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Mar 2026 07:22:23 -1000 Subject: [PATCH] fix #8023: don't skip axiom clauses with non-base-level satisfying literals 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> --- src/smt/theory_seq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7732bc683..58b166ac6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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)