From 3ca960d679f5362cd25030e03ca45cd7b88f409b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2026 10:49:09 -0700 Subject: [PATCH] test that there is a model Signed-off-by: Nikolaj Bjorner --- src/smt/theory_nseq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 5948c2696..e24554cf0 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -543,7 +543,7 @@ namespace smt { // All literals that were needed to build a model could be assigned to true. // There is an existing nielsen graph with a satisfying assignment. - if (!m_nielsen_literals.empty() && + if (!m_nielsen_literals.empty() && m_nielsen.sat_node() != nullptr && all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) { IF_VERBOSE(1, verbose_stream() << "nseq final_check: satifiable state revisited\n"); return FC_DONE;