From df419c137dfdaa6e89831531242ea036df72af8f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 07:47:16 -1000 Subject: [PATCH] fix the test Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 1920d569a..8e6261e70 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2629,21 +2629,21 @@ static void tst_explain_p6236() { s.set_rvalues(counter_as); nlsat::evaluator& ev = s.get_evaluator(); - // Check unsat - bool unsat = true; + // At least one lemma literal must be true at the counterexample for soundness + bool some_true = false; for (unsigned i = 0; i < lemma.size(); ++i) { nlsat::literal lit = lemma[i]; nlsat::atom* a = s.bool_var2atom(lit.var()); if (a == nullptr) continue; - bool sat = ev.eval(a, lit.sign()); + bool v = ev.eval(a, lit.sign()); std::cout << " lit[" << i << "]: "; - s.display(std::cout, lit) << " = " << (sat ? "true" : "false") << "\n"; - if (sat) - unsat = false; + s.display(std::cout, lit) << " = " << (v ? "true" : "false") << "\n"; + if (v) + some_true = true; } - ENSURE(unsat); + ENSURE(some_true); s.dec_ref(root_lt_bvar); s.dec_ref(gt_lit);