From b1f79656979470982408c4c7e619a3855729500c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Aug 2024 13:40:09 -0700
Subject: [PATCH] fix mul inverse

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/bv_sls_eval.cpp   | 10 ++++++++--
 src/ast/sls/sls_bv_plugin.cpp |  2 +-
 src/ast/sls/sls_valuation.cpp |  2 +-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index f369c67c4..6916e4968 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1002,11 +1002,13 @@ namespace bv {
     * 8*e = a*(2b), then a = 4e*b^-1
     */
     bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
-        verbose_stream() << e << " := " << a << " * " << b << "\n";
+        //verbose_stream() << e << " := " << a << " * " << b << "\n";
         unsigned parity_e = a.parity(e);
         unsigned parity_b = a.parity(b);
 
         if (a.is_zero(b)) {
+            if (a.try_set(e))
+                return true;
             a.get_variant(m_tmp, m_rand);
             if (m_rand(10) != 0)
                 for (unsigned i = 0; i < b.bw - parity_b; ++i)
@@ -1044,14 +1046,18 @@ namespace bv {
 
         // x*ta + y*tb = x
 
+        y.set_bw(a.bw);
         b.copy_to(a.nw, y);
+        //verbose_stream() << "a.nw " << a.nw << " b.nw " << b.nw << " b " << b << " y.nw " << y.nw << " y "   << y << "\n";
         if (parity_b > 0) {
             a.shift_right(y, parity_b);
+            
 #if 0
             for (unsigned i = parity_b; i < b.bw; ++i)
                 y.set(i, m_rand(2) == 0);
 #endif
         }
+        //verbose_stream() << parity_b << " y " << y << "\n";
 
         y[a.nw] = 0;
         x[a.nw] = 0;
@@ -1094,7 +1100,7 @@ namespace bv {
         b.copy_to(a.nw, y);
         if (parity_b > 0)
             a.shift_right(y, parity_b);
-        a.set_mul(m_tmp, tb, y);
+        a.set_mul(m_tmp, tb, y, false);
         SASSERT(a.is_one(m_tmp));
 #endif
         e.copy_to(b.nw, m_tmp2);
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index cef65251b..af12addf7 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -148,7 +148,7 @@ namespace sls {
                 ctx.new_value_eh(e);
         }
         else if (bv.is_bv(e)) {
-            IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));             
+            IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e));             
             m_eval.set_random(e);
             ctx.new_value_eh(e);
         }
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index 264eefbb1..6325cd27a 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -487,7 +487,7 @@ namespace bv {
     void sls_valuation::shift_right(bvect& out, unsigned shift) const {
         SASSERT(shift < bw);
         for (unsigned i = 0; i < bw; ++i)
-            out.set(i, i + shift < bw ? m_bits.get(i + shift) : false);
+            out.set(i, i + shift < bw ? out.get(i + shift) : false);
         SASSERT(well_formed());
     }