From 5d3a5a94e8233156930a8220a5fcf3c77429d7d3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Nov 2023 13:31:36 +0100 Subject: [PATCH] update progress --- src/math/polysat/viable.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index ff5b59df3..5dd3b9bbf 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1732,7 +1732,9 @@ namespace polysat { return l_false; // conflict // replace lower bits of 'val' by 'a' - val = val + distance(lower_cover_lo, a, lower_mod_value); + rational const dist = distance(lower_cover_lo, a, lower_mod_value); + val += dist; + progress += dist; 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));