From 6b66e818975e22fcbb2ed2d612edf06f9ce8a44c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 30 Aug 2024 17:41:50 -0700
Subject: [PATCH] Refactor bv_sls files to sls_bv with namespace and class name
 adjustments

---
 src/ast/ast.cpp                  |   2 +-
 src/ast/rewriter/bv_rewriter.h   |   2 +-
 src/ast/sls/CMakeLists.txt       |   8 +-
 src/ast/sls/sls_bv_eval.cpp      | 174 +++++++++++++++++--------------
 src/ast/sls/sls_bv_eval.h        |  40 +++----
 src/ast/sls/sls_bv_fixed.cpp     |  28 ++---
 src/ast/sls/sls_bv_fixed.h       |  17 +--
 src/ast/sls/sls_bv_plugin.cpp    |   3 +-
 src/ast/sls/sls_bv_plugin.h      |   8 +-
 src/ast/sls/sls_bv_terms.cpp     |  16 +--
 src/ast/sls/sls_bv_terms.h       |   8 +-
 src/ast/sls/sls_bv_valuation.cpp |  77 +++++++-------
 src/ast/sls/sls_bv_valuation.h   |  20 ++--
 src/ast/sls/sls_context.cpp      |  11 +-
 src/ast/sls/sls_context.h        |   2 +-
 src/test/sls_test.cpp            |  12 +--
 16 files changed, 226 insertions(+), 202 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index e1e3efe99..4295e9ec5 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1709,7 +1709,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();        
 
-//    track_id(*this, n, 77);
+  //  track_id(*this, n, 9213);
     
 //    TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 1adee41e6..0fb4cdd99 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -222,7 +222,7 @@ public:
 
 #define MK_BV_BINARY(OP)                         \
     expr_ref OP(expr* a, expr* b) {              \
-        expr_ref result(m);                      \
+        expr_ref result(m), _a(a, m), _b(b, m);  \
         if (BR_FAILED == OP(a, b, result))       \
             result = m_util.OP(a, b);            \
         return result;                           \
diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt
index 35f936e01..3ee51a028 100644
--- a/src/ast/sls/CMakeLists.txt
+++ b/src/ast/sls/CMakeLists.txt
@@ -1,19 +1,19 @@
 z3_add_component(ast_sls
   SOURCES
     bvsls_opt_engine.cpp
-    bv_sls_eval.cpp
-    bv_sls_fixed.cpp
-    bv_sls_terms.cpp  
     sat_ddfw.cpp
     sls_arith_base.cpp
     sls_arith_plugin.cpp
     sls_basic_plugin.cpp
+    sls_bv_eval.cpp
+    sls_bv_fixed.cpp
     sls_bv_plugin.cpp
+    sls_bv_terms.cpp
+    sls_bv_valuation.cpp
     sls_context.cpp
     sls_engine.cpp
     sls_euf_plugin.cpp
     sls_smt_solver.cpp
-    sls_valuation.cpp
   COMPONENT_DEPENDENCIES
     ast
     converters
diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index 4f2b31480..08b9e6baf 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2024 Microsoft Corporation
 
 Module Name:
 
-    bv_sls_eval.cpp
+    sls_bv_eval.cpp
 
 Author:
 
@@ -13,12 +13,12 @@ Author:
 
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
-#include "ast/sls/bv_sls_eval.h"
+#include "ast/sls/sls_bv_eval.h"
 #include "ast/rewriter/th_rewriter.h"
 
-namespace bv {
+namespace sls {
 
-    sls_eval::sls_eval(sls_terms& terms, sls::context& ctx): 
+    bv_eval::bv_eval(sls::bv_terms& terms, sls::context& ctx): 
         m(ctx.get_manager()),
         ctx(ctx),
         terms(terms),
@@ -27,7 +27,7 @@ namespace bv {
     {}   
 
 
-    void sls_eval::register_term(expr* e) {
+    void bv_eval::register_term(expr* e) {
         if (!is_app(e))
             return;
         app* a = to_app(e);
@@ -46,7 +46,7 @@ namespace bv {
         }
     }
 
-    void sls_eval::add_bit_vector(app* e) {
+    void bv_eval::add_bit_vector(app* e) {
         if (!bv.is_bv(e))
             return;
         m_values.reserve(e->get_id() + 1);
@@ -64,9 +64,9 @@ namespace bv {
         return;
     }
 
-    sls_valuation* sls_eval::alloc_valuation(app* e) {
+    sls::bv_valuation* bv_eval::alloc_valuation(app* e) {
         auto bit_width = bv.get_bv_size(e);
-        auto* r = alloc(sls_valuation, bit_width);
+        auto* r = alloc(sls::bv_valuation, bit_width);
         while (m_tmp.size() < 2 * r->nw) {
             m_tmp.push_back(0);
             m_tmp2.push_back(0);           
@@ -87,12 +87,12 @@ namespace bv {
     }
 
 
-    void sls_eval::init_eval_bv(app* e) {
+    void bv_eval::init_eval_bv(app* e) {
         if (bv.is_bv(e)) 
             eval(e).commit_eval();               
     }
     
-    bool sls_eval::can_eval1(app* e) const {
+    bool bv_eval::can_eval1(app* e) const {
         expr* x, * y;
         if (m.is_eq(e, x, y))
             return bv.is_bv(x);
@@ -116,7 +116,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_eval::bval1_bv(app* e) const {
+    bool bv_eval::bval1_bv(app* e) const {
         SASSERT(m.is_bool(e));
         SASSERT(e->get_family_id() == bv.get_fid());
 
@@ -191,7 +191,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_eval::bval1(app* e) const {
+    bool bv_eval::bval1(app* e) const {
         if (e->get_family_id() == bv.get_fid())
             return bval1_bv(e);
         expr* x, * y;
@@ -203,17 +203,17 @@ namespace bv {
         return false;
     }
 
-    sls_valuation& sls_eval::eval(app* e) const {
+    sls::bv_valuation& bv_eval::eval(app* e) const {
         auto& val = *m_values[e->get_id()];        
         eval(e, val);
         return val;        
     }
 
-    void sls_eval::set(expr* e, sls_valuation const& val) {
+    void bv_eval::set(expr* e, sls::bv_valuation const& val) {
         m_values[e->get_id()]->set(val.bits());
     }
 
-    void sls_eval::eval(app* e, sls_valuation& val) const {
+    void bv_eval::eval(app* e, sls::bv_valuation& val) const {
         SASSERT(bv.is_bv(e));
         if (m.is_ite(e)) {
             SASSERT(bv.is_bv(e->get_arg(1)));
@@ -630,12 +630,12 @@ namespace bv {
         val.clear_overflow_bits(val.eval);
     }
 
-    digit_t sls_eval::random_bits() {
-        return sls_valuation::random_bits(m_rand);
+    digit_t bv_eval::random_bits() {
+        return sls::bv_valuation::random_bits(m_rand);
     }
 
 
-    bool sls_eval::is_uninterpreted(app* e) const {
+    bool bv_eval::is_uninterpreted(app* e) const {
         if (is_uninterp(e))
             return true;
         if (e->get_family_id() != bv.get_family_id())
@@ -656,7 +656,7 @@ namespace bv {
         }
     }
     
-    bool sls_eval::repair_down(app* e, unsigned i) {      
+    bool bv_eval::repair_down(app* e, unsigned i) {      
         expr* arg = e->get_arg(i);
         if (m.is_value(arg))
             return false;
@@ -673,7 +673,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_eval::try_repair_bv(app* e, unsigned i) {
+    bool bv_eval::try_repair_bv(app* e, unsigned i) {
         switch (e->get_decl_kind()) {
         case OP_BAND:
             SASSERT(e->get_num_args() >= 2);
@@ -845,7 +845,7 @@ namespace bv {
         }
     }
 
-    bool sls_eval::try_repair_eq(app* e, unsigned i) {
+    bool bv_eval::try_repair_eq(app* e, unsigned i) {
         auto child = e->get_arg(i);        
         auto is_true = bval0(e);
         if (bv.is_bv(child)) {
@@ -856,7 +856,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {
             if (m_rand(20) != 0) 
                 if (a.try_set(b.bits()))
@@ -884,7 +884,7 @@ namespace bv {
         }
     }
 
-    void sls_eval::fold_oper(bvect& out, app* t, unsigned i, std::function<void(bvect&, bvval const&)> const& f) {
+    void bv_eval::fold_oper(bvect& out, app* t, unsigned i, std::function<void(bvect&, bvval const&)> const& f) {
         auto i2 = i == 0 ? 1 : 0;
         auto const& c = wval(t->get_arg(i2));
         for (unsigned j = 0; j < c.nw; ++j)
@@ -904,13 +904,13 @@ namespace bv {
     // e[i] = 0 & b[i] = 0 -> a[i] = random
     // a := e[i] | (~b[i] & a[i])
 
-    bool sls_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = ~a.fixed[i] & (e[i] | (~b.bits()[i] & random_bits()));
         return a.set_repair(random_bool(), m_tmp);
     }
 
-    bool sls_eval::try_repair_band(app* t, unsigned i) {
+    bool bv_eval::try_repair_band(app* t, unsigned i) {
         bvect const& e = assign_value(t);
         auto f = [&](bvect& out, bvval const& c) {
             for (unsigned j = 0; j < c.nw; ++j)
@@ -930,13 +930,13 @@ namespace bv {
     // set a[i] to 1 where b[i] = 0, e[i] = 1
     // set a[i] to 0 where e[i] = 0, a[i] = 1
     //     
-    bool sls_eval::try_repair_bor(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_bor(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = e[i] & (~b.bits()[i] | random_bits());
         return a.set_repair(random_bool(), m_tmp);
     }
 
-    bool sls_eval::try_repair_bor(app* t, unsigned i) {
+    bool bv_eval::try_repair_bor(app* t, unsigned i) {
         bvect const& e = assign_value(t);
         auto f = [&](bvect& out, bvval const& c) {
             for (unsigned j = 0; j < c.nw; ++j)
@@ -945,12 +945,12 @@ namespace bv {
         fold_oper(m_tmp2, t, i, f);
         bvval& a = wval(t, i);
         for (unsigned j = 0; j < a.nw; ++j)
-            m_tmp[j] = e[i] & (~m_tmp2[i] | random_bits());
+            m_tmp[j] = e[j] & (~m_tmp2[j] | random_bits());
 
         return a.set_repair(random_bool(), m_tmp);
     }
 
-    bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = e[i] ^ b.bits()[i];
         return a.set_repair(random_bool(), m_tmp);
@@ -958,7 +958,7 @@ namespace bv {
 
 
 
-    bool sls_eval::try_repair_bxor(app* t, unsigned i) {
+    bool bv_eval::try_repair_bxor(app* t, unsigned i) {
         bvect const& e = assign_value(t);
         auto f = [&](bvect& out, bvval const& c) {
             for (unsigned j = 0; j < c.nw; ++j)
@@ -968,7 +968,7 @@ namespace bv {
 
         bvval& a = wval(t, i);
         for (unsigned j = 0; j < a.nw; ++j)
-            m_tmp[j] = e[i] ^ m_tmp2[i];
+            m_tmp[j] = e[j] ^ m_tmp2[j];
 
         return a.set_repair(random_bool(), m_tmp);
     }
@@ -978,7 +978,7 @@ namespace bv {
     // first try to set a := e - b
     // If this fails, set a to a random value
     // 
-    bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
         if (m_rand(20) != 0) {
             a.set_sub(m_tmp, e, b.bits());
             if (a.try_set(m_tmp))
@@ -987,7 +987,7 @@ namespace bv {
         return a.set_random(m_rand);        
     }
 
-    bool sls_eval::try_repair_add(app* t, unsigned i) {
+    bool bv_eval::try_repair_add(app* t, unsigned i) {
         bvval& a = wval(t, i);
         bvect const& e = assign_value(t);
         if (m_rand(20) != 0) {
@@ -1002,7 +1002,7 @@ namespace bv {
         return a.set_random(m_rand);     
     }
 
-    bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
+    bool bv_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
         if (m_rand(20) != 0) {
             if (i == 0) 
                 // e = a - b -> a := e + b
@@ -1021,7 +1021,7 @@ namespace bv {
     * e = a*b, then a = e * b^-1
     * 8*e = a*(2b), then a = 4e*b^-1
     */
-    bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
+    bool bv_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
         //verbose_stream() << e << " := " << a << " * " << b << "\n";
         unsigned parity_e = a.parity(e);
         unsigned parity_b = a.parity(b);
@@ -1133,14 +1133,14 @@ namespace bv {
         return a.set_random(m_rand);
     }
 
-    bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
+    bool bv_eval::try_repair_bnot(bvect const& e, bvval& a) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = ~e[i];        
         a.clear_overflow_bits(m_tmp);
         return a.try_set(m_tmp);
     }
 
-    bool sls_eval::try_repair_bneg(bvect const& e, bvval& a) {
+    bool bv_eval::try_repair_bneg(bvect const& e, bvval& a) {
         a.set_sub(m_tmp, m_zero, e); 
         return a.try_set(m_tmp);
     }
@@ -1154,7 +1154,7 @@ namespace bv {
     // infeasible if b + 1 = p2
     // solve for x >=s b + 1
     // 
-    bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
         auto& p2 = m_b;
         b.set_zero(p2);
         p2.set(b.bw - 1, true);
@@ -1180,7 +1180,7 @@ namespace bv {
     // infeasible if b = 0
     // solve for x <=s b - 1
     // 
-    bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
         auto& p2 = m_b;
         b.set_zero(p2);
         p2.set(b.bw - 1, true);
@@ -1211,7 +1211,7 @@ namespace bv {
     // or
     // x := random p2 <= x <= b       if c < p2  (b >= p2)
     // 
-    bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) {
+    bool bv_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) {
         bool r = false;
         if (b < p2) {
             bool coin = m_rand(2) == 0;
@@ -1236,7 +1236,7 @@ namespace bv {
     // x := random b <= x or x < p2   if d < p2
     //  
 
-    bool sls_eval::try_repair_sge(bvval& a, bvect const& b, bvect const& p2) {
+    bool bv_eval::try_repair_sge(bvval& a, bvect const& b, bvect const& p2) {
         auto& p2_1 = m_tmp4;
         a.set_sub(p2_1, p2, m_one);
         p2_1.set_bw(a.bw);
@@ -1258,14 +1258,14 @@ namespace bv {
         return r;
     }
 
-    void sls_eval::add_p2_1(bvval const& a, bvect& t) const {
+    void bv_eval::add_p2_1(bvval const& a, bvect& t) const {
         m_zero.set(a.bw - 1, true);
         a.set_add(t, a.bits(), m_zero);
         m_zero.set(a.bw - 1, false);
         a.clear_overflow_bits(t);
     }
 
-    bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
         //verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n";
         if (e) {
             // a <= t
@@ -1281,7 +1281,7 @@ namespace bv {
         }           
     }
 
-    bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
         //verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
         if (e) {
             // a >= t
@@ -1297,11 +1297,11 @@ namespace bv {
         }    
     }
 
-    bool sls_eval::try_repair_bit2bool(bvval& a, unsigned idx) {       
+    bool bv_eval::try_repair_bit2bool(bvval& a, unsigned idx) {       
         return a.try_set_bit(idx, !a.get_bit(idx));
     }
 
-    bool sls_eval::try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0) {
             unsigned sh = b.to_nat(b.bw);
             if (sh == 0) 
@@ -1324,23 +1324,39 @@ namespace bv {
             }
         }
         else {
-            // NB. blind sub-range of possible values for b
             SASSERT(i == 1);
-            unsigned sh = m_rand(a.bw + 1);
-            b.set(m_tmp, sh);
-            return b.try_set(m_tmp);
+            if (a.is_zero())
+                return b.set_random(m_rand);
+
+            unsigned start = m_rand();
+            for (unsigned j = 0; j <= a.bw; ++j) {
+                unsigned sh = (j + start) % (a.bw + 1);
+                m_tmp.set_bw(a.bw);
+                m_tmp2.set_bw(a.bw);
+                b.set(m_tmp, sh);
+                if (!b.can_set(m_tmp))
+                    continue;
+                m_tmp2.set_shift_left(a.bits(), m_tmp);
+                if (m_tmp2 == e && b.try_set(m_tmp)) 
+                    return true;                
+            }
+            
+            if (m_rand(2) == 0)
+                return false;
+
+            return b.set_random(m_rand);
         }
         return false;
     }
 
-    bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
         if (i == 0)
             return try_repair_ashr0(e, a, b);
         else
             return try_repair_ashr1(e, a, b);
     }
 
-    bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0)
             return try_repair_lshr0(e, a, b);
         else
@@ -1354,7 +1370,7 @@ namespace bv {
     *   - e = 0 -> a := random 
     *   - e > 0 -> a := random with msb(a) >= msb(e)
     */
-    bool sls_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) {
         
         auto& t = m_tmp;
         // t := e << b
@@ -1433,7 +1449,7 @@ namespace bv {
     * - e = 0:  b := random
     * - e > 0:  b := random >= clz(e)
     */
-    bool sls_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) {
+    bool bv_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) {
 
         auto& t = m_tmp;
         auto clza = a.clz(a.bits());
@@ -1487,7 +1503,7 @@ namespace bv {
     * weak:
     *   
     */
-    bool sls_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) {
+    bool bv_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) {
         auto& t = m_tmp;
         t.set_bw(b.bw);
         auto n = b.msb(b.bits());
@@ -1548,7 +1564,7 @@ namespace bv {
     * - e > 0:  b := random >= clz(e)
     */
 
-    bool sls_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) {
+    bool bv_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) {
 
         auto& t = m_tmp;
         auto clza = a.clz(a.bits());
@@ -1590,7 +1606,7 @@ namespace bv {
         return b.set_repair(random_bool(), t);
     }
 
-    bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {
         SASSERT(e[0] == 0 || e[0] == 1);
         SASSERT(e.bw == 1);
         return try_repair_eq(e[0] == 1, i == 0 ? a : b, i == 0 ? b : a);
@@ -1601,7 +1617,7 @@ namespace bv {
     // b = 0 => e = -1        // nothing to repair on a
     // e != -1 => max(a) >=u e
 
-    bool sls_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0) {
             if (a.is_zero(e) && a.is_ones(a.fixed) && a.is_ones())
                 return false;            
@@ -1666,7 +1682,7 @@ namespace bv {
     //      (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0)
 
 
-    bool sls_eval::try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i) {
 
         if (i == 0) {
             if (b.is_zero()) {
@@ -1711,21 +1727,21 @@ namespace bv {
         }
     }
 
-    bool sls_eval::add_overflow_on_fixed(bvval const& a, bvect const& t) {
+    bool bv_eval::add_overflow_on_fixed(bvval const& a, bvect const& t) {
         a.set(m_tmp3, m_zero);
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp3[i] = a.fixed[i] & a.bits()[i];
         return a.set_add(m_tmp4, t, m_tmp3);
     }
 
-    bool sls_eval::mul_overflow_on_fixed(bvval const& a, bvect const& t) {
+    bool bv_eval::mul_overflow_on_fixed(bvval const& a, bvect const& t) {
         a.set(m_tmp3, m_zero);
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp3[i] = a.fixed[i] & a.bits()[i];
         return a.set_mul(m_tmp4, m_tmp3, t);
     }
 
-    bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const {
+    bool bv_eval::try_repair_rotate_left(bvect const& e, bvval& a, unsigned n) const {
         // a := rotate_right(e, n)
         n = (a.bw - n) % a.bw;
         for (unsigned i = a.bw - n; i < a.bw; ++i)
@@ -1735,7 +1751,7 @@ namespace bv {
         return a.set_repair(true, m_tmp);       
     }
 
-    bool sls_eval::try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_rotate_left(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0) {
             rational n = b.get_value();
             n = mod(n, rational(b.bw));
@@ -1749,7 +1765,7 @@ namespace bv {
         }       
     }
 
-    bool sls_eval::try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_rotate_right(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0) {
             rational n = b.get_value();
             n = mod(b.bw - n, rational(b.bw));
@@ -1763,7 +1779,7 @@ namespace bv {
         }
     }
 
-    bool sls_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) {
+    bool bv_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) {
         if (e) {
             // maximize
             if (i == 0) {
@@ -1792,7 +1808,7 @@ namespace bv {
     // prefix of e must be 1s or 0 and match bit position of last bit in a.
     // set a to suffix of e, matching signs.
     //  
-    bool sls_eval::try_repair_sign_ext(bvect const& e, bvval& a) {
+    bool bv_eval::try_repair_sign_ext(bvect const& e, bvval& a) {
         for (unsigned i = a.bw; i < e.bw; ++i)
             if (e.get(i) != e.get(a.bw - 1))
                 return false;
@@ -1806,7 +1822,7 @@ namespace bv {
     // 
     // prefix of e must be 0s.
     // 
-    bool sls_eval::try_repair_zero_ext(bvect const& e, bvval& a) {
+    bool bv_eval::try_repair_zero_ext(bvect const& e, bvval& a) {
         for (unsigned i = a.bw; i < e.bw; ++i)
             if (e.get(i))
                 return false;
@@ -1817,7 +1833,7 @@ namespace bv {
         return a.try_set(m_tmp);
     }
 
-    bool sls_eval::try_repair_concat(app* e, unsigned idx) {
+    bool bv_eval::try_repair_concat(app* e, unsigned idx) {
         unsigned bw = 0;
         auto& ve = assign_value(e);
         for (unsigned j = e->get_num_args() - 1; j > idx; --j)
@@ -1834,7 +1850,7 @@ namespace bv {
     // for the randomized assignment, 
     // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
     // 
-    bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
+    bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
         if (m_rand(m_config.m_prob_randomize_extract)  <= 100) {
             a.get_variant(m_tmp, m_rand);
             if (0 == (m_rand(2))) {
@@ -1857,7 +1873,7 @@ namespace bv {
         return a.set_random(m_rand);
     }
 
-    bool sls_eval::try_repair_int2bv(bvect const& e, expr* arg) {
+    bool bv_eval::try_repair_int2bv(bvect const& e, expr* arg) {
         rational r = e.get_value(e.nw);
         arith_util a(m);
         expr_ref intval(a.mk_int(r), m);
@@ -1865,7 +1881,7 @@ namespace bv {
         return true;
     }
 
-    void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
+    void bv_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
         bvect& quot, bvect& rem) const {
         unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t));
         unsigned bnw = nw;
@@ -1885,7 +1901,7 @@ namespace bv {
         }
     }
 
-    bool sls_eval::repair_up(expr* e) {
+    bool bv_eval::repair_up(expr* e) {
         if (!is_app(e) || !can_eval1(to_app(e)))
             return false;
         if (m.is_bool(e)) {
@@ -1913,13 +1929,13 @@ namespace bv {
         return false;
     }
 
-    sls_valuation& sls_eval::wval(expr* e) const { 
+    sls::bv_valuation& bv_eval::wval(expr* e) const { 
         // if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n";  
         return *m_values[e->get_id()]; 
     }
 
 
-    void sls_eval::commit_eval(app* e) {
+    void bv_eval::commit_eval(app* e) {
         if (!bv.is_bv(e))
             return;
         //
@@ -1927,12 +1943,12 @@ namespace bv {
         VERIFY(wval(e).commit_eval());
     }
 
-    void sls_eval::set_random(app* e) {
+    void bv_eval::set_random(app* e) {
         if (bv.is_bv(e))
             eval(e).set_random(m_rand);
     }
 
-    bool sls_eval::eval_is_correct(app* e) {
+    bool bv_eval::eval_is_correct(app* e) {
         if (!can_eval1(e))
             return false;
         if (m.is_bool(e))
@@ -1947,7 +1963,7 @@ namespace bv {
         return false;
     }
 
-    expr_ref sls_eval::get_value(app* e) {
+    expr_ref bv_eval::get_value(app* e) {
         if (m.is_bool(e))
             return expr_ref(m.mk_bool_val(bval0(e)), m);
         else if (bv.is_bv(e)) {
@@ -1958,7 +1974,7 @@ namespace bv {
         return expr_ref(m);
     }
 
-    std::ostream& sls_eval::display(std::ostream& out) const {
+    std::ostream& bv_eval::display(std::ostream& out) const {
         auto& terms = ctx.subterms();
         for (expr* e : terms) {
             if (!bv.is_bv(e))
@@ -1971,7 +1987,7 @@ namespace bv {
         return out;
     }
 
-    std::ostream& sls_eval::display_value(std::ostream& out, expr* e) const {
+    std::ostream& bv_eval::display_value(std::ostream& out, expr* e) const {
         if (bv.is_bv(e)) 
             return out << wval(e);
         return out << "?";
diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h
index 6661acbfc..bdbf00a49 100644
--- a/src/ast/sls/sls_bv_eval.h
+++ b/src/ast/sls/sls_bv_eval.h
@@ -17,27 +17,31 @@ Author:
 #pragma once
 
 #include "ast/ast.h"
-#include "ast/sls/sls_valuation.h"
-#include "ast/sls/bv_sls_fixed.h"
+#include "ast/sls/sls_bv_valuation.h"
+#include "ast/sls/sls_bv_fixed.h"
 #include "ast/sls/sls_context.h"
 #include "ast/bv_decl_plugin.h"
 
-namespace bv {
+ 
+namespace sls {
 
-    class sls_terms;
+    class bv_terms;
 
-    class sls_eval {
+
+    using bvect = sls::bvect;
+
+    class bv_eval {
         struct config {
             unsigned m_prob_randomize_extract = 50;
         };
 
-        friend class sls_fixed;
+        friend class sls::bv_fixed;
         friend class sls_test;
         ast_manager&        m;
         sls::context&       ctx;
-        sls_terms&          terms;
+        sls::bv_terms&      terms;
         bv_util             bv;
-        sls_fixed           m_fix;
+        sls::bv_fixed       m_fix;
         mutable mpn_manager mpn;
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
@@ -45,12 +49,12 @@ namespace bv {
         bool_vector         m_fixed;
         
 
-        scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation
+        scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
 
         mutable bvect m_tmp, m_tmp2, m_tmp3, m_tmp4, m_mul_tmp, m_zero, m_one, m_minus_one;
         bvect m_a, m_b, m_nextb, m_nexta, m_aux;
 
-        using bvval = sls_valuation;
+        using bvval = sls::bv_valuation;
 
         void init_eval_bv(app* e);
        
@@ -59,7 +63,7 @@ namespace bv {
         * Return true if not already registered, false if already registered.
         */
         void add_bit_vector(app* e);
-        sls_valuation* alloc_valuation(app* e);
+        sls::bv_valuation* alloc_valuation(app* e);
 
         bool bval1_bv(app* e) const;  
 
@@ -120,13 +124,12 @@ namespace bv {
         digit_t random_bits();
         bool random_bool() { return m_rand() % 2 == 0; }
 
-        sls_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); }
+        sls::bv_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); }
 
-        void eval(app* e, sls_valuation& val) const;
+        void eval(app* e, sls::bv_valuation& val) const;
 
         bvect const& assign_value(app* e) const { return wval(e).bits(); }
 
-        bool bval0(expr* e) const { return ctx.is_true(e); }
 
         /**
          * Retrieve evaluation based on immediate children.
@@ -137,7 +140,7 @@ namespace bv {
         void commit_eval(app* e);
 
     public:
-        sls_eval(sls_terms& terms, sls::context& ctx);
+        bv_eval(sls::bv_terms& terms, sls::context& ctx);
 
         void init() { m_fix.init(); }
 
@@ -149,13 +152,13 @@ namespace bv {
          * wval - Word (bit-vector) values
          */        
 
-        sls_valuation& wval(expr* e) const;
+        sls::bv_valuation& wval(expr* e) const;
 
-        void set(expr* e, sls_valuation const& val);
+        void set(expr* e, sls::bv_valuation const& val);
 
         bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
         
-        sls_valuation& eval(app* e) const;
+        sls::bv_valuation& eval(app* e) const;
 
         void set_random(app* e);
 
@@ -165,6 +168,7 @@ namespace bv {
 
         expr_ref get_value(app* e);
 
+        bool bval0(expr* e) const { return ctx.is_true(e); }
         bool bval1(app* e) const;
       
         /*
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index 16492f2b3..f72186b67 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -13,13 +13,13 @@ Author:
 
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
-#include "ast/sls/bv_sls_fixed.h"
-#include "ast/sls/bv_sls_terms.h"
-#include "ast/sls/bv_sls_eval.h"
+#include "ast/sls/sls_bv_fixed.h"
+#include "ast/sls/sls_bv_terms.h"
+#include "ast/sls/sls_bv_eval.h"
 
-namespace bv {
+namespace sls {
 
-    sls_fixed::sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx):
+    bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx):
         ev(ev),
         terms(terms),
         m(ev.m),
@@ -27,7 +27,7 @@ namespace bv {
         ctx(ctx)
     {}
 
-    void sls_fixed::init() {
+    void bv_fixed::init() {
         for (auto e : ctx.subterms())
             set_fixed(e);
 
@@ -44,7 +44,7 @@ namespace bv {
             propagate_range_up(e);    
     }
 
-    void sls_fixed::propagate_range_up(expr* e) {
+    void bv_fixed::propagate_range_up(expr* e) {
         expr* t, * s;
         rational v;
         if (bv.is_concat(e, t, s)) {
@@ -81,7 +81,7 @@ namespace bv {
 
     // s <=s t           <=> s + K <= t + K,   K = 2^{bw-1}
 
-    bool sls_fixed::init_range(app* e, bool sign) {
+    bool bv_fixed::init_range(app* e, bool sign) {
         expr* s, * t, * x, * y;
         rational a, b;
         unsigned idx;
@@ -149,7 +149,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_fixed::init_eq(expr* t, rational const& a, bool sign) {        
+    bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {        
         unsigned lo, hi;
         rational b(0);
         // verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n";
@@ -213,7 +213,7 @@ namespace bv {
     // a < x + b         <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [         a != -1
     // x + a < x + b     <=> ! (x + b <= x + a) <=> x in [-a, -b [                                  a != b
     // 
-    bool sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
+    bool bv_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
         if (!x && !y)
             return false;
         if (!x) 
@@ -225,7 +225,7 @@ namespace bv {
         return false;
     }
 
-    bool sls_fixed::add_range(expr* e, rational lo, rational hi, bool sign) {
+    bool bv_fixed::add_range(expr* e, rational lo, rational hi, bool sign) {
         auto& v = ev.wval(e);
         lo = mod(lo, rational::power_of_two(bv.get_bv_size(e)));
         hi = mod(hi, rational::power_of_two(bv.get_bv_size(e)));
@@ -252,7 +252,7 @@ namespace bv {
         return true;
     }
 
-    void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) {
+    void bv_fixed::get_offset(expr* e, expr*& x, rational& offset) {
         expr* s, * t;
         x = e;
         offset = 0;
@@ -275,13 +275,13 @@ namespace bv {
             x = nullptr;
     }
 
-    bool sls_fixed::is_fixed1(app* e) const {
+    bool bv_fixed::is_fixed1(app* e) const {
         if (is_uninterp(e))
             return false;
         return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); });
     }
     
-    void sls_fixed::set_fixed(expr* _e) {
+    void bv_fixed::set_fixed(expr* _e) {
         if (!is_app(_e))
             return;
         auto e = to_app(_e);
diff --git a/src/ast/sls/sls_bv_fixed.h b/src/ast/sls/sls_bv_fixed.h
index f0dfcd43e..cc1c1597a 100644
--- a/src/ast/sls/sls_bv_fixed.h
+++ b/src/ast/sls/sls_bv_fixed.h
@@ -17,18 +17,19 @@ Author:
 #pragma once
 
 #include "ast/ast.h"
-#include "ast/sls/sls_valuation.h"
+#include "ast/sls/sls_bv_valuation.h"
 #include "ast/sls/sls_context.h"
 #include "ast/bv_decl_plugin.h"
 
-namespace bv {
 
-    class sls_eval;
-    class sls_terms;
+namespace sls {
+
+    class bv_terms;
+    class bv_eval;
     
-    class sls_fixed {
-        sls_eval&           ev;
-        sls_terms&          terms;
+    class bv_fixed {
+        typename bv_eval&           ev;
+        typename bv_terms&          terms;
         ast_manager&        m;
         bv_util&            bv;
         sls::context&       ctx;
@@ -44,7 +45,7 @@ namespace bv {
         void set_fixed(expr* e);
 
     public:
-        sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx);
+        bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx);
         void init();
     };
 }
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 3a8da088d..fe4972ec2 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -57,7 +57,6 @@ namespace sls {
             return;
         auto a = to_app(e);
 
-        // verbose_stream() << "propagate " << mk_bounded_pp(e, m) << " " << m_eval.eval_is_correct(a) << "\n";
         if (!m_eval.eval_is_correct(a))
             ctx.new_value_eh(e);
     }
@@ -201,7 +200,7 @@ namespace sls {
         //        unsigned value = 0;
         // if (bv.is_bv(e))
         //    value = svector_hash<unsigned_hash>()(m_eval.wval(e).bits());
-        IF_VERBOSE(2, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F");
+        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F");
                    // if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e).bits();
                    verbose_stream() << "\n");
     }
diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h
index f85a741ca..a185c5ef3 100644
--- a/src/ast/sls/sls_bv_plugin.h
+++ b/src/ast/sls/sls_bv_plugin.h
@@ -18,15 +18,15 @@ Author:
 
 #include "ast/sls/sls_context.h"
 #include "ast/bv_decl_plugin.h"
-#include "ast/sls/bv_sls_terms.h"
-#include "ast/sls/bv_sls_eval.h"
+#include "ast/sls/sls_bv_terms.h"
+#include "ast/sls/sls_bv_eval.h"
 
 namespace sls {
 
     class bv_plugin : public plugin {
         bv_util             bv;
-        bv::sls_terms       m_terms;
-        bv::sls_eval        m_eval;
+        sls::bv_terms       m_terms;
+        bv_eval             m_eval;
         bv::sls_stats       m_stats;
         bool                m_initialized = false;
 
diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp
index 7c489960c..a21ac1be9 100644
--- a/src/ast/sls/sls_bv_terms.cpp
+++ b/src/ast/sls/sls_bv_terms.cpp
@@ -16,25 +16,25 @@ Author:
 --*/
 
 #include "ast/ast_ll_pp.h"
-#include "ast/sls/bv_sls_terms.h"
+#include "ast/sls/sls_bv_terms.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/bv_rewriter.h"
 
-namespace bv {
+namespace sls {
 
-    sls_terms::sls_terms(sls::context& ctx):
+    bv_terms::bv_terms(sls::context& ctx):
         ctx(ctx),
         m(ctx.get_manager()), 
         bv(m),
         m_axioms(m) {}
 
-    void sls_terms::register_term(expr* e) {
+    void bv_terms::register_term(expr* e) {
         auto r = ensure_binary(e);
         if (r != e)
             m_axioms.push_back(m.mk_eq(e, r));
     }
 
-    expr_ref sls_terms::ensure_binary(expr* e) {
+    expr_ref bv_terms::ensure_binary(expr* e) {
 
         app* a = to_app(e);
         auto arg = [&](unsigned i) {
@@ -64,7 +64,7 @@ namespace bv {
         return r;
     }
 
-    expr_ref sls_terms::mk_sdiv(expr* x, expr* y) {
+    expr_ref bv_terms::mk_sdiv(expr* x, expr* y) {
         // d = udiv(abs(x), abs(y))
         // y = 0, x >= 0 -> -1
         // y = 0, x < 0 -> 1
@@ -92,7 +92,7 @@ namespace bv {
         return r;
     }
 
-    expr_ref sls_terms::mk_smod(expr* x, expr* y) {
+    expr_ref bv_terms::mk_smod(expr* x, expr* y) {
         // u := umod(abs(x), abs(y))
         // u = 0 ->  0
         // y = 0 ->  x
@@ -116,7 +116,7 @@ namespace bv {
         return r;
     }
 
-    expr_ref sls_terms::mk_srem(expr* x, expr* y) {
+    expr_ref bv_terms::mk_srem(expr* x, expr* y) {
         // y = 0 -> x
         // else x - sdiv(x, y) * y
         expr_ref r(m);
diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h
index 8f1e477f0..9fc71ba0e 100644
--- a/src/ast/sls/sls_bv_terms.h
+++ b/src/ast/sls/sls_bv_terms.h
@@ -23,12 +23,12 @@ Author:
 #include "ast/bv_decl_plugin.h"
 #include "ast/sls/sls_stats.h"
 #include "ast/sls/sls_powers.h"
-#include "ast/sls/sls_valuation.h"
+#include "ast/sls/sls_bv_valuation.h"
 #include "ast/sls/sls_context.h"
 
-namespace bv {
+namespace sls {
 
-    class sls_terms {
+    class bv_terms {
         sls::context&       ctx;
         ast_manager&        m;
         bv_util             bv;
@@ -41,7 +41,7 @@ namespace bv {
         expr_ref mk_srem(expr* x, expr* y);
 
     public:
-        sls_terms(sls::context& ctx);       
+        bv_terms(sls::context& ctx);       
 
         void register_term(expr* e);
 
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
index 6325cd27a..65a6ac4a9 100644
--- a/src/ast/sls/sls_bv_valuation.cpp
+++ b/src/ast/sls/sls_bv_valuation.cpp
@@ -18,9 +18,9 @@ Author:
     
 --*/
 
-#include "ast/sls/sls_valuation.h"
+#include "ast/sls/sls_bv_valuation.h"
 
-namespace bv {
+namespace sls {
 
     void bvect::set_bw(unsigned bw) {
         this->bw = bw;
@@ -138,6 +138,7 @@ namespace bv {
         set_bw(a.bw);
         SASSERT(a.bw == b.bw);
         unsigned shift = b.to_nat(b.bw);
+
         if (shift == 0)
             a.copy_to(a.nw, *this);
         else if (shift >= a.bw)
@@ -148,7 +149,7 @@ namespace bv {
         return *this;
     }
 
-    sls_valuation::sls_valuation(unsigned bw) {
+    bv_valuation::bv_valuation(unsigned bw) {
         set_bw(bw);
         m_lo.set_bw(bw);
         m_hi.set_bw(bw);
@@ -162,7 +163,7 @@ namespace bv {
         fixed[nw - 1] = ~mask;
     }
 
-    void sls_valuation::set_bw(unsigned b) {
+    void bv_valuation::set_bw(unsigned b) {
         bw = b;
         nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
         mask = (1 << (bw % (8 * sizeof(digit_t)))) - 1;
@@ -170,7 +171,7 @@ namespace bv {
             mask = ~(digit_t)0;
     }
 
-    bool sls_valuation::commit_eval() { 
+    bool bv_valuation::commit_eval() { 
         for (unsigned i = 0; i < nw; ++i)
             if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))                 
                 return false;
@@ -184,7 +185,7 @@ namespace bv {
         return true;
     }
 
-    bool sls_valuation::in_range(bvect const& bits) const {
+    bool bv_valuation::in_range(bvect const& bits) const {
         mpn_manager m;
         auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw);
         SASSERT(!has_overflow(bits));
@@ -207,7 +208,7 @@ namespace bv {
     // largest dst <= src and dst is feasible
     //
 
-    bool sls_valuation::get_at_most(bvect const& src, bvect& dst) const {
+    bool bv_valuation::get_at_most(bvect const& src, bvect& dst) const {
         SASSERT(!has_overflow(src));
         src.copy_to(nw, dst);
         sup_feasible(dst);
@@ -227,7 +228,7 @@ namespace bv {
 
     //
     // smallest dst >= src and dst is feasible with respect to this.
-    bool sls_valuation::get_at_least(bvect const& src, bvect& dst) const {
+    bool bv_valuation::get_at_least(bvect const& src, bvect& dst) const {
         SASSERT(!has_overflow(src));
         src.copy_to(nw, dst);
         dst.set_bw(bw);
@@ -244,7 +245,7 @@ namespace bv {
         return true;
     }
 
-    bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
+    bool bv_valuation::set_random_at_most(bvect const& src, random_gen& r) {
         m_tmp.set_bw(bw);
         if (!get_at_most(src, m_tmp))
             return false;
@@ -258,7 +259,7 @@ namespace bv {
         return (can_set(m_tmp) || get_at_most(src, m_tmp)) && m_tmp <= src && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) {
+    bool bv_valuation::set_random_at_least(bvect const& src, random_gen& r) {
         m_tmp.set_bw(bw);
         if (!get_at_least(src, m_tmp))
             return false;
@@ -272,7 +273,7 @@ namespace bv {
         return (can_set(m_tmp) || get_at_least(src, m_tmp)) && src <= m_tmp && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
+    bool bv_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
         bvect& tmp = m_tmp;
         if (0 == r(2)) {
             if (!get_at_least(lo, tmp))
@@ -299,27 +300,27 @@ namespace bv {
         return false;
     }
 
-    void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {      
+    void bv_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {      
         for (unsigned i = bw; !is_feasible(dst) && i-- > 0; )
             if (!fixed.get(i) && dst.get(i))
                 dst.set(i, false);      
         repair_sign_bits(dst);
     }
 
-    void sls_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
+    void bv_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
         for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i)
             if (!fixed.get(i) && !dst.get(i))
                 dst.set(i, true);
         repair_sign_bits(dst);
     }
 
-    void sls_valuation::set_random_above(bvect& dst, random_gen& r) {
+    void bv_valuation::set_random_above(bvect& dst, random_gen& r) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = dst[i] | (random_bits(r) & ~fixed[i]);
         repair_sign_bits(dst);
     }
 
-    void sls_valuation::set_random_below(bvect& dst, random_gen& r) {
+    void bv_valuation::set_random_below(bvect& dst, random_gen& r) {
         if (is_zero(dst))
             return;
         unsigned n = 0, idx = UINT_MAX;
@@ -336,7 +337,7 @@ namespace bv {
         repair_sign_bits(dst);
     }
 
-    bool sls_valuation::set_repair(bool try_down, bvect& dst) {
+    bool bv_valuation::set_repair(bool try_down, bvect& dst) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
         clear_overflow_bits(dst);
@@ -372,7 +373,7 @@ namespace bv {
         return repaired;
     }
 
-    void sls_valuation::min_feasible(bvect& out) const {
+    void bv_valuation::min_feasible(bvect& out) const {
         if (m_lo < m_hi) 
             m_lo.copy_to(nw, out);        
         else {
@@ -383,7 +384,7 @@ namespace bv {
         SASSERT(!has_overflow(out));
     }
 
-    void sls_valuation::max_feasible(bvect& out) const {
+    void bv_valuation::max_feasible(bvect& out) const {
         if (m_lo < m_hi) {
             m_hi.copy_to(nw, out);
             sub1(out);
@@ -396,7 +397,7 @@ namespace bv {
         SASSERT(!has_overflow(out));
     }
 
-    unsigned sls_valuation::msb(bvect const& src) const {
+    unsigned bv_valuation::msb(bvect const& src) const {
         SASSERT(!has_overflow(src));
         for (unsigned i = nw; i-- > 0; )
             if (src[i] != 0)
@@ -404,7 +405,7 @@ namespace bv {
         return bw;
     }
 
-    unsigned sls_valuation::clz(bvect const& src) const {
+    unsigned bv_valuation::clz(bvect const& src) const {
         SASSERT(!has_overflow(src));
         unsigned i = bw;
         for (; i-- > 0; )
@@ -414,36 +415,36 @@ namespace bv {
     }
 
 
-    void sls_valuation::set_value(bvect& bits, rational const& n) {
+    void bv_valuation::set_value(bvect& bits, rational const& n) {
         for (unsigned i = 0; i < bw; ++i)
             bits.set(i, n.get_bit(i));
         clear_overflow_bits(bits);
     }
 
-    void sls_valuation::get(bvect& dst) const {
+    void bv_valuation::get(bvect& dst) const {
         m_bits.copy_to(nw, dst);
     }
 
-    digit_t sls_valuation::random_bits(random_gen& rand) {
+    digit_t bv_valuation::random_bits(random_gen& rand) {
         digit_t r = 0;
         for (digit_t i = 0; i < sizeof(digit_t); ++i)
             r ^= rand() << (8 * i);
         return r;
     }
 
-    void sls_valuation::get_variant(bvect& dst, random_gen& r) const {
+    void bv_valuation::get_variant(bvect& dst, random_gen& r) const {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
         repair_sign_bits(dst);
         clear_overflow_bits(dst);
     }
 
-    bool sls_valuation::set_random(random_gen& r) {
+    bool bv_valuation::set_random(random_gen& r) {
         get_variant(m_tmp, r);
         return set_repair(r(2) == 0, m_tmp);
     }
 
-    void sls_valuation::repair_sign_bits(bvect& dst) const {
+    void bv_valuation::repair_sign_bits(bvect& dst) const {
         if (m_signed_prefix == 0)
             return;
         bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1);
@@ -469,7 +470,7 @@ namespace bv {
     // 0 = (new_bits ^ bits) & fixedf
     // also check that new_bits are in range
     //
-    bool sls_valuation::can_set(bvect const& new_bits) const {
+    bool bv_valuation::can_set(bvect const& new_bits) const {
         SASSERT(!has_overflow(new_bits));
         for (unsigned i = 0; i < nw; ++i)
             if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i]))
@@ -477,21 +478,21 @@ namespace bv {
         return in_range(new_bits);
     }
 
-    unsigned sls_valuation::to_nat(unsigned max_n) const {
+    unsigned bv_valuation::to_nat(unsigned max_n) const {
 
         bvect const& d = m_bits;
         SASSERT(!has_overflow(d));
         return d.to_nat(max_n);
     }
 
-    void sls_valuation::shift_right(bvect& out, unsigned shift) const {
+    void bv_valuation::shift_right(bvect& out, unsigned shift) const {
         SASSERT(shift < bw);
         for (unsigned i = 0; i < bw; ++i)
             out.set(i, i + shift < bw ? out.get(i + shift) : false);
         SASSERT(well_formed());
     }
 
-    void sls_valuation::add_range(rational l, rational h) {   
+    void bv_valuation::add_range(rational l, rational h) {   
 
         l = mod(l, rational::power_of_two(bw));
         h = mod(h, rational::power_of_two(bw));
@@ -550,7 +551,7 @@ namespace bv {
     // update bits based on ranges
     //
 
-    unsigned sls_valuation::diff_index(bvect const& a) const {
+    unsigned bv_valuation::diff_index(bvect const& a) const {
         unsigned index = 0;
         for (unsigned i = nw; i-- > 0; ) {
             auto diff = fixed[i] & (m_bits[i] ^ a[i]);
@@ -560,7 +561,7 @@ namespace bv {
         return index;
     }
 
-    void sls_valuation::inf_feasible(bvect& a) const {
+    void bv_valuation::inf_feasible(bvect& a) const {
         unsigned lo_index = diff_index(a);
         
         if (lo_index != 0) {
@@ -583,7 +584,7 @@ namespace bv {
         }
     }
 
-    void sls_valuation::sup_feasible(bvect& a) const {
+    void bv_valuation::sup_feasible(bvect& a) const {
         unsigned hi_index = diff_index(a);
         if (hi_index != 0) {
             hi_index--;
@@ -605,7 +606,7 @@ namespace bv {
         }
     }
 
-    void sls_valuation::tighten_range() {
+    void bv_valuation::tighten_range() {
         
         if (m_lo == m_hi)
             return;
@@ -691,13 +692,13 @@ namespace bv {
         SASSERT(well_formed());
     }
 
-    void sls_valuation::set_sub(bvect& out, bvect const& a, bvect const& b) const {
+    void bv_valuation::set_sub(bvect& out, bvect const& a, bvect const& b) const {
         digit_t c;
         mpn_manager().sub(a.data(), nw, b.data(), nw, out.data(), &c);
         clear_overflow_bits(out);
     }
 
-    bool sls_valuation::set_add(bvect& out, bvect const& a, bvect const& b) const {
+    bool bv_valuation::set_add(bvect& out, bvect const& a, bvect const& b) const {
         digit_t c;
         mpn_manager().add(a.data(), nw, b.data(), nw, out.data(), nw + 1, &c);
         bool ovfl = out[nw] != 0 || has_overflow(out);
@@ -705,7 +706,7 @@ namespace bv {
         return ovfl;
     }
 
-    bool sls_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const {
+    bool bv_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const {
         out.reserve(2 * nw);
         SASSERT(out.size() >= 2 * nw);
         mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
@@ -719,7 +720,7 @@ namespace bv {
         return ovfl;
     }
 
-    bool sls_valuation::is_power_of2(bvect const& src) const {
+    bool bv_valuation::is_power_of2(bvect const& src) const {
         unsigned c = 0;
         for (unsigned i = 0; i < nw; ++i)
             c += get_num_1bits(src[i]);
diff --git a/src/ast/sls/sls_bv_valuation.h b/src/ast/sls/sls_bv_valuation.h
index cb1a478c3..393880698 100644
--- a/src/ast/sls/sls_bv_valuation.h
+++ b/src/ast/sls/sls_bv_valuation.h
@@ -3,7 +3,7 @@ Copyright (c) 2024 Microsoft Corporation
 
 Module Name:
 
-    sls_valuation.h
+    sls_bv_valuation.h
 
 Abstract:
 
@@ -20,12 +20,10 @@ Author:
 #include "util/params.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/uint_set.h"
-#include "ast/ast.h"
-#include "ast/sls/sls_stats.h"
-#include "ast/sls/sls_powers.h"
-#include "ast/bv_decl_plugin.h"
+#include "util/mpz.h"
+#include "util/rational.h"
 
-namespace bv {
+namespace sls {
 
     class bvect : public svector<digit_t> {
     public:
@@ -106,7 +104,7 @@ namespace bv {
     inline bool operator!=(bvect const& a, bvect const& b) { return !(a == b); }
     std::ostream& operator<<(std::ostream& out, bvect const& v);
 
-    class sls_valuation {
+    class bv_valuation {
     protected:
         bvect m_bits;
         bvect m_lo, m_hi;        // range assignment to bit-vector, as wrap-around interval
@@ -124,8 +122,8 @@ namespace bv {
         bvect fixed;                     // bit assignment and don't care bit
         bvect eval;                      // current evaluation
 
-
-        sls_valuation(unsigned bw);
+        
+        bv_valuation(unsigned bw);
 
         void set_bw(unsigned bw);
         void set_signed(unsigned prefix) { m_signed_prefix = prefix; }
@@ -176,7 +174,7 @@ namespace bv {
         bool in_range(bvect const& bits) const;
         bool can_set(bvect const& bits) const;
 
-        bool eq(sls_valuation const& other) const { return eq(other.m_bits); }
+        bool eq(bv_valuation const& other) const { return eq(other.m_bits); }
         bool eq(bvect const& other) const { return other == m_bits; }
 
         bool is_zero() const { return is_zero(m_bits); }
@@ -343,6 +341,6 @@ namespace bv {
 
     };
 
-    inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); }
+    inline std::ostream& operator<<(std::ostream& out, bv_valuation const& v) { return v.display(out); }
 
 }
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index d4ac62b00..87f4d5890 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -36,7 +36,8 @@ namespace sls {
         m_gd(*this),
         m_ld(*this),
         m_repair_down(m.get_num_asts(), m_gd),
-        m_repair_up(m.get_num_asts(), m_ld) {
+        m_repair_up(m.get_num_asts(), m_ld),
+        m_todo(m) {
         register_plugin(alloc(euf_plugin, *this));
         register_plugin(alloc(arith_plugin, *this));
         register_plugin(alloc(bv_plugin, *this));
@@ -417,6 +418,8 @@ namespace sls {
                 m_todo.pop_back();            
             else if (is_app(e)) {
                 if (all_of(*to_app(e), [&](expr* arg) { return is_visited(arg); })) {
+                    expr_ref _e(e, m);
+                    m_todo.pop_back();
                     for (expr* arg : *to_app(e)) {
                         m_parents.reserve(arg->get_id() + 1);
                         m_parents[arg->get_id()].push_back(e);
@@ -425,7 +428,6 @@ namespace sls {
                         mk_literal(e);
                     register_term(e);
                     visit(e);
-                    m_todo.pop_back();
                 }
                 else {
                     for (expr* arg : *to_app(e)) 
@@ -433,9 +435,10 @@ namespace sls {
                 }
             }
             else {
+                expr_ref _e(e, m);
+                m_todo.pop_back();
                 register_term(e);
                 visit(e);
-                m_todo.pop_back();
             }
         }
     }
@@ -452,6 +455,8 @@ namespace sls {
 
         m_repair_down.reserve(e->get_id() + 1);
         m_repair_up.reserve(e->get_id() + 1);
+        if (!term(e->get_id()))
+            verbose_stream() << "no term " << mk_bounded_pp(e, m) << "\n";
         SASSERT(e == term(e->get_id()));
         if (!m_repair_down.contains(e->get_id()))
             m_repair_down.insert(e->get_id());
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 0b8ded614..4df41b315 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -124,7 +124,7 @@ namespace sls {
         void register_plugin(plugin* p);
 
         void init();
-        ptr_vector<expr> m_todo;
+        expr_ref_vector m_todo;
         void register_terms(expr* e);
         void register_term(expr* e);
 
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 756df1110..296e2e860 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -1,6 +1,6 @@
 
-#include "ast/sls/bv_sls_eval.h"
-#include "ast/sls/bv_sls_terms.h"
+#include "ast/sls/sls_bv_eval.h"
+#include "ast/sls/sls_bv_terms.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/reg_decl_plugins.h"
 #include "ast/ast_pp.h"
@@ -57,8 +57,8 @@ namespace bv {
 
             my_sat_solver_context solver;
             sls::context ctx(m, solver);
-            sls_terms terms(ctx);
-            sls_eval ev(terms, ctx);
+            sls::bv_terms terms(ctx);
+            sls::bv_eval ev(terms, ctx);
             for (auto e : es)
                 ev.register_term(e);
             ev.init();
@@ -176,8 +176,8 @@ namespace bv {
 
             my_sat_solver_context solver;
             sls::context ctx(m, solver);
-            sls_terms terms(ctx);
-            sls_eval ev(terms, ctx);
+            sls::bv_terms terms(ctx);
+            sls::bv_eval ev(terms, ctx);
             for (auto e : es)
                 ev.register_term(e);
             ev.init();