From fa4cd37c07e780aecbb2f473fee58b8a3c2f6780 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Mar 2026 13:32:18 -0700 Subject: [PATCH] add the false literal callback Signed-off-by: Nikolaj Bjorner --- src/smt/theory_nseq.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 039bdf4ba..1be2587c9 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -88,11 +88,14 @@ namespace smt { literal lit = ctx.get_literal(e); if (is_not) lit.neg(); - if (ctx.get_assignment(lit) == l_false) + if (ctx.get_assignment(lit) == l_false) { + IF_VERBOSE(1, verbose_stream() << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n"); return lit; + } return sat::null_literal; }; + m_nielsen.set_literal_if_false(literal_if_false); }