From 74aa47f45899b267842ed1dec65a57fbaa168b8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2019 13:52:27 -0700 Subject: [PATCH] fix #2578 Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6ec48299a..4690472af 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1148,7 +1148,9 @@ namespace nlsat { checkpoint(); if (value(l) == l_false) continue; - CTRACE("nlsat", max_var(l) != m_xk, display(tout); + if (value(l) == l_true) + return true; // could happen if clause is a tautology + CTRACE("nlsat", max_var(l) != m_xk || value(l) != l_undef, display(tout); tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l) << "\n"; display(tout, cls) << "\n";); SASSERT(value(l) == l_undef);