From 179da493793eb3a2d7f1fb033affb4f1bf297751 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Nov 2023 13:23:51 +0100 Subject: [PATCH] fix --- src/math/polysat/viable.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 918bdd921..ff5b59df3 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1732,7 +1732,7 @@ namespace polysat { return l_false; // conflict // replace lower bits of 'val' by 'a' - val = val - lower_cover_lo + a; + val = val + distance(lower_cover_lo, a, lower_mod_value); LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value)); LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value)); SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value)); @@ -1743,9 +1743,6 @@ namespace polysat { SASSERT(result == l_undef); // TODO: continue with intervals at current level - // TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up? - // we only have to chase intervals from the beginning if ec.cur has become inactive - NOT_IMPLEMENTED_YET(); return l_undef; }