From 193a99da296f697ffd5fdabcadc6ced0b58b0cba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Mar 2020 09:46:32 +0100 Subject: [PATCH] fix #3152 Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_explain.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 856089abe..672b732ee 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1441,7 +1441,7 @@ namespace nlsat { // literal l must be in the core core.push_back(l); new_todo.swap(todo); - return true; + return !todo.empty(); } else { new_todo.push_back(l); @@ -1459,11 +1459,11 @@ namespace nlsat { todo.reset(); core.reset(); todo.append(num, ls); while (true) { - TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core);); + TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";); if (!minimize_core(todo, core)) break; std::reverse(todo.begin(), todo.end()); - TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core);); + TRACE("nlsat_minimize", tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";); if (!minimize_core(todo, core)) break; }