mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-03 02:18:58 +00:00
Code Activity

test that there is a model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-02 10:49:09 -07:00
parent b0a4a15c98
commit 3ca960d679
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_nseq.cpp
View file

@ -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;