From 6071797ba988f08b4a32ffca931e31e88c56cc8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 May 2019 12:11:43 +0200 Subject: [PATCH] fix again Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_evaluator.cpp | 2 +- src/nlsat/nlsat_solver.cpp | 5 +---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 2cbf80849..7f353c7db 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -385,7 +385,7 @@ namespace nlsat { // TODO: check if it is useful to cache results SASSERT(m_assignment.is_assigned(max_var(p))); int r = m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); - return r > 0 ? +1 : (r < 0 ? 0 : -1); + return r > 0 ? +1 : (r < 0 ? -1 : 0); } bool satisfied(int sign, atom::kind k) { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index fae9a1c69..cc6cedac7 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2102,10 +2102,7 @@ namespace nlsat { del_ill_formed_lemmas(); TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); reinit_cache(); - for (var x = 0; x < num_vars(); x++) { - if (new_assignment.is_assigned(x)) - m_assignment.set(x, new_assignment.value(x)); - } + m_assignment.swap(new_assignment); reattach_arith_clauses(m_clauses); reattach_arith_clauses(m_learned); TRACE("nlsat_reorder", tout << "solver after variable reorder\n"; display(tout); display_vars(tout););