From 93dd0b605447939eb5c9d963f96c773501ed3a91 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 21 Dec 2023 14:34:42 +0100
Subject: [PATCH] interval

---
 src/math/polysat/interval.h | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h
index 7300b04b5..0cf276aa3 100644
--- a/src/math/polysat/interval.h
+++ b/src/math/polysat/interval.h
@@ -71,6 +71,7 @@ namespace polysat {
         SASSERT(mod_value.is_power_of_two());
         SASSERT(0 <= a && a < mod_value);
         SASSERT(0 <= b && b <= mod_value);
+        SASSERT(b != mod_value || a == 0);  // b == mod_value only allowed when a == 0
         rational x = b - a;
         if (x.is_neg())
             x += mod_value;
@@ -113,10 +114,7 @@ namespace polysat {
             SASSERT(0 <= lo && lo < mod_value);
             SASSERT(0 <= hi && hi <= mod_value);
             SASSERT(hi != mod_value || lo == 0);  // hi == mod_value only allowed when lo == 0
-            rational len = hi - lo;
-            if (len.is_neg())
-                len += mod_value;
-            return len;
+            return distance(lo, hi, mod_value);
         }
 
         rational len(rational const& mod_value) const {