From c45eb2a87044efdbdf2f4384911fe7ab1cec1f78 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 14 Dec 2023 16:19:35 +0100 Subject: [PATCH] Fix assertion --- src/math/polysat/viable.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 29c74da3e..43b4c3ba4 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1781,9 +1781,10 @@ namespace polysat { 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(val, cover_hi) = " << (to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : 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)); + SASSERT_EQ((to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : distance(val, to_cover_hi, mod_value)), to_cover_len - progress); + SASSERT((to_cover_len == mod_value && val == to_cover_lo ? to_cover_len : distance(val, to_cover_hi, mod_value)) >= distance(next_val, to_cover_hi, mod_value)); if (result == l_true) return l_true; // done