From bbddeffe0bbb941ff940b02b1d464fe4e393c2d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Jan 2022 15:07:05 +0100 Subject: [PATCH] check for 0 Signed-off-by: Nikolaj Bjorner --- src/math/polysat/viable.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 1b8c2f99c..7aef1cbf3 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -206,10 +206,6 @@ namespace polysat { return floor((e->interval.hi_val() - coeff_val - 1) / e->coeff); }; -// TODO: looks like there's an infinite loop for: -// [match_linear3] a1 = 3; b1 = 0; e1 = 0 -// [match_linear3] a2 = 3; b2 = -2; e2 = -2 - // naive widening. TODO: can we accelerate this? // condition e->interval.hi_val() < coeff_val is // to ensure that widening is performed on the same interval @@ -232,7 +228,10 @@ namespace polysat { break; if (e->interval.lo_val() > coeff_val) break; - lo -= delta_l(coeff_val); + rational d = delta_l(coeff_val); + if (d.is_zero()) + break; + lo -= d; } }; do {