From 0ada7f8e405b719217867adf1babd36bffd31c40 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 8 Feb 2024 14:20:26 +0100
Subject: [PATCH] bug with sizes

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

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 22838c6c6..6d97f6315 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -702,9 +702,10 @@ namespace polysat {
         unsigned const w_sz = c.size(w);
         unsigned const z_sz = offset;
         unsigned const y_sz = std::min(w_sz, v_sz - z_sz);
-        unsigned const x_sz = v_sz - y_sz;
+        unsigned const x_sz = v_sz - y_sz - z_sz;
         rational const& w_shift = rational::power_of_two(w_sz - y_sz);
         verbose_stream() << "v_sz " << v_sz << " w_sz " << w_sz << " / x_sz " << x_sz << " y_sz " << y_sz << " z_sz " << z_sz << "\n";
+        SASSERT_EQ(v_sz, x_sz + y_sz + z_sz);
 
         SASSERT(!e->interval.is_full());
         rational const& lo = e->interval.lo_val();