From c62ba26cf4c80a5da121cf7604032ed961ad6e9b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 18 Jan 2023 18:38:44 +0100
Subject: [PATCH] simplify

---
 src/math/polysat/viable.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index dbd738d08..c262dd7c3 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -425,7 +425,8 @@ namespace {
 
         // a * [yil;yih] is the right-most y-interval that is completely in [lo;hi].
         rational const yih = y1h + i * step;
-        rational const a_yih = a*yih + (k - i - 1)*M;
+        rational const a_yih = a_y1h + i * alpha;
+        SASSERT_EQ(a_yih, a*yih + (k - i - 1)*M);
         SASSERT(contained(a_yih));
 
         // The next interval to the right may contain a few more values if alpha > 0