From fde78f99c36bcb1db78d36164e5b96d73d188697 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Apr 2022 13:27:36 +0200 Subject: [PATCH] fix propagation when variables are assigned Signed-off-by: Nikolaj Bjorner --- src/math/polysat/solver.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 3b1e78231..ada5bc4c2 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -292,9 +292,8 @@ namespace polysat { if (!is_assigned(other_v)) { add_watch(c, other_v); std::swap(c->vars()[idx], c->vars()[i]); - SASSERT(!is_assigned(c->var(0))); - SASSERT(!is_assigned(c->var(1))); - return true; + if (!is_assigned(c->var(1 - idx))) + return true; } } // at most one variable remains unassigned. @@ -437,7 +436,11 @@ namespace polysat { void solver::add_watch(signed_constraint c) { SASSERT(c); - auto const& vars = c->vars(); + auto& vars = c->vars(); + unsigned i = 0, j = 0, sz = vars.size(); + for (; i < sz && j < 2; ++i) + if (!is_assigned(vars[i])) + std::swap(vars[i], vars[j++]); if (vars.size() > 0) add_watch(c, vars[0]); if (vars.size() > 1)