From 531bda39ac7f97656c831b1b6ed18f1ceb232ad5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Mar 2024 10:15:14 -0800
Subject: [PATCH] fix alias bug

---
 src/ast/sls/bv_sls_eval.cpp   | 21 +++++++++++++++------
 src/ast/sls/sls_valuation.cpp | 24 ++++++++++++------------
 src/ast/sls/sls_valuation.h   | 11 ++++++-----
 3 files changed, 33 insertions(+), 23 deletions(-)

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index cc5911905..a70bc7261 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1043,8 +1043,16 @@ namespace bv {
         if (b.is_zero()) {
             a.get_variant(m_tmp, m_rand);
             return a.set_repair(random_bool(), m_tmp);            
-        }
-        
+        }      
+
+#if 0
+        verbose_stream() << "solve for " << e << "\n";
+
+        rational r = e.get_value(e.nw);
+        rational root;
+        verbose_stream() << r.is_int_perfect_square(root) << "\n";
+#endif
+                
         
         auto& x = m_tmp;
         auto& y = m_tmp2;
@@ -1055,7 +1063,8 @@ namespace bv {
         auto& nexta = m_nexta;
         auto& nextb = m_nextb;
         auto& aux = m_aux;
-        
+        auto bw = b.bw;
+       
 
         // x*ta + y*tb = x
 
@@ -1071,10 +1080,11 @@ namespace bv {
         y[a.nw] = 0;
         x[a.nw] = 0;
 
+        
         a.set_bw((a.nw + 1)* 8 * sizeof(digit_t));
         y.set_bw(a.bw); // enable comparisons        
         a.set_zero(x);
-        x.set(b.bw, true); // x = 2 ^ b.bw       
+        x.set(bw, true); // x = 2 ^ b.bw       
 
         a.set_one(ta);
         a.set_zero(tb);
@@ -1099,11 +1109,10 @@ namespace bv {
             a.set(tb, aux);                 // tb := aux
         }
 
-        a.set_bw(b.bw);
+        a.set_bw(bw);
         y.set_bw(0);
         // x*a + y*b = 1
     
-        tb.set_bw(b.bw);
         tb.set_bw(0);
 #if Z3DEBUG
         b.get(y);
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index b656a341b..aeeb392e2 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -74,6 +74,15 @@ namespace bv {
         return out;
     }
 
+    rational bvect::get_value(unsigned nw) const {
+        rational p(1), r(0);
+        for (unsigned i = 0; i < nw; ++i) {
+            r += p * rational((*this)[i]);
+            p *= rational::power_of_two(8 * sizeof(digit_t));
+        }
+        return r;
+    }
+
     sls_valuation::sls_valuation(unsigned bw) {
         set_bw(bw);
         m_lo.set_bw(bw);
@@ -347,7 +356,7 @@ namespace bv {
                     dst.set(i, true);        
         }
         else {
-            for (unsigned i = 0; i < bw && !in_range(dst); ++i)
+            for (unsigned i = 0; !in_range(dst) && i < bw; ++i)
                 if (!fixed.get(i) && !dst.get(i))
                     dst.set(i, true);
             for (unsigned i = bw; !in_range(dst) && i-- > 0;)
@@ -398,15 +407,6 @@ namespace bv {
         clear_overflow_bits(bits);
     }
 
-    rational sls_valuation::get_value(bvect const& bits) const {
-        rational p(1), r(0);
-        for (unsigned i = 0; i < nw; ++i) {
-            r += p * rational(bits[i]);
-            p *= rational::power_of_two(8 * sizeof(digit_t));
-        }
-        return r;
-    }
-
     void sls_valuation::get(bvect& dst) const {
         m_bits.copy_to(nw, dst);
     }
@@ -479,8 +479,8 @@ namespace bv {
             set_value(m_hi, h);
         }
         else {            
-            auto old_lo = get_value(m_lo);
-            auto old_hi = get_value(m_hi);
+            auto old_lo = lo();
+            auto old_hi = hi();
             if (old_lo < old_hi) {
                 if (old_lo < l && l < old_hi)
                     set_value(m_lo, l),
diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h
index cbe1a35a4..e79ac959c 100644
--- a/src/ast/sls/sls_valuation.h
+++ b/src/ast/sls/sls_valuation.h
@@ -60,6 +60,8 @@ namespace bv {
             return bw;
         }
 
+        rational get_value(unsigned nw) const;
+
         friend bool operator==(bvect const& a, bvect const& b);
         friend bool operator<(bvect const& a, bvect const& b);
         friend bool operator>(bvect const& a, bvect const& b);
@@ -96,7 +98,6 @@ namespace bv {
         bvect m_lo, m_hi;        // range assignment to bit-vector, as wrap-around interval
 
         unsigned mask;
-        rational get_value(bvect const& bits) const;
         bool round_up(bvect& dst) const;
         bool round_down(bvect& dst) const;
 
@@ -131,10 +132,10 @@ namespace bv {
 
         void set_value(bvect& bits, rational const& r);
 
-        rational get_value() const { return get_value(m_bits); }
-        rational get_eval() const { return get_value(eval); }
-        rational lo() const { return get_value(m_lo); }
-        rational hi() const { return get_value(m_hi); }
+        rational get_value() const { return m_bits.get_value(nw); }
+        rational get_eval() const { return eval.get_value(nw); }
+        rational lo() const { return m_lo.get_value(nw); }
+        rational hi() const { return m_hi.get_value(nw); }
 
 
         void get(bvect& dst) const;