From cd6382f1c86eb3f785443baca643867a95f629fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Feb 2024 22:38:07 -0800
Subject: [PATCH] fix alias bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/bv_sls_eval.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index cc754997f..4dbd4b11f 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1039,6 +1039,7 @@ namespace bv {
         
 
         // x*ta + y*tb = x
+        auto bw = a.bw;
         b.get(y);
         if (parity_b > 0)
             b.shift_right(y, parity_b);
@@ -1047,7 +1048,7 @@ namespace bv {
         a.bw = 8 * sizeof(digit_t) * a.nw;
         // x = 2 ^ b.bw
         a.set_zero(x);
-        a.set(x, b.bw, true);        
+        a.set(x, bw, true);        
 
         a.set_one(ta);
         a.set_zero(tb);
@@ -1072,8 +1073,8 @@ namespace bv {
             a.set(tb, aux);                 // tb := aux
         }
 
-        a.bw = b.bw;
-        a.nw = b.nw;
+        a.bw = bw;
+        a.nw = a.nw - 1;
         // x*a + y*b = 1
     
 #if Z3DEBUG