diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 67ed1da87..1adee41e6 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);                      \
         if (BR_FAILED == OP(a, b, result))       \
             result = m_util.OP(a, b);            \
         return result;                           \
@@ -237,6 +237,7 @@ public:
 
     MK_BV_BINARY(mk_bv_urem);
     MK_BV_BINARY(mk_ule);
+    MK_BV_BINARY(mk_sle);
     MK_BV_BINARY(mk_bv_add);
     MK_BV_BINARY(mk_bv_mul);
     MK_BV_BINARY(mk_bv_sub);
@@ -249,6 +250,13 @@ public:
         return result;        
     }
 
+    expr_ref mk_bv_neg(expr* a) {
+        expr_ref result(a, m);
+        if (BR_FAILED == mk_uminus(a, result))
+            result = m_util.mk_bv_neg(a);
+        return result;
+    }
+
 
 
 };
diff --git a/src/ast/sls/CMakeLists.txt b/src/ast/sls/CMakeLists.txt
index 1703a39ac..e1f35e583 100644
--- a/src/ast/sls/CMakeLists.txt
+++ b/src/ast/sls/CMakeLists.txt
@@ -1,7 +1,6 @@
 z3_add_component(ast_sls
   SOURCES
     bvsls_opt_engine.cpp
-    bv_sls.cpp
     bv_sls_eval.cpp
     bv_sls_fixed.cpp
     bv_sls_terms.cpp  
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
index f1b2a9f4f..700436a8d 100644
--- a/src/ast/sls/bv_sls.cpp
+++ b/src/ast/sls/bv_sls.cpp
@@ -23,14 +23,13 @@ Author:
 #include "ast/ast_ll_pp.h"
 #include "params/sls_params.hpp"
 
-namespace bv {
+namespace bvu {
 
     sls::sls(ast_manager& m, params_ref const& p): 
         m(m), 
         bv(m),
         m_terms(m),
-        m_eval(m),
-        m_engine(m, p)
+        m_eval(m)
     {
         updt_params(p);
     }
@@ -100,55 +99,12 @@ namespace bv {
 
 
     void sls::reinit_eval() {
-        init_repair_candidates();
-
-        if (m_to_repair.empty())
-            return;
-
-        // refresh the best model so far to a callback
-        set_model();
-
-        // add fresh units, if any
-        bool new_assertion = false;
-        while (m_get_unit) {
-            auto e = m_get_unit();
-            if (!e)
-                break;
-            new_assertion = true;
-            assert_expr(e);
-        }
-        if (new_assertion) 
-            init();        
-           
-        std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
-            unsigned id = e->get_id();
-            bool keep = !m_to_repair.contains(id);
-            if (m.is_bool(e)) {
-                if (m_eval.is_fixed0(e) || keep)
-                    return m_eval.bval0(e);
-                if (m_engine_init) {
-                    auto const& z = m_engine.get_value(e);
-                    return rational(z).get_bit(0);
-                }
-            }
-            else if (bv.is_bv(e)) {
-                auto& w = m_eval.wval(e);
-                if (w.fixed.get(i) || keep)
-                    return w.get_bit(i);
-                if (m_engine_init) {
-                    auto const& z = m_engine.get_value(e);
-                    return rational(z).get_bit(i);
-                }
-            }
-            
-            return m_rand() % 2 == 0;
-        };
-        m_eval.init_eval(m_terms.assertions(), eval);
         init_repair();
-        // m_engine_init = false;
     }
 
+
     std::pair<bool, app*> sls::next_to_repair() {
+#if 0
         app* e = nullptr;
         if (m_repair_down != UINT_MAX) {
             e = m_terms.term(m_repair_down);
@@ -176,7 +132,7 @@ namespace bv {
             }
             m_repair_roots.remove(index);
         }
-
+#endif
         return { false, nullptr };
     }
 
@@ -199,35 +155,17 @@ namespace bv {
         return l_undef;
     }
 
-    lbool sls::search2() {
-        lbool res = l_undef;
-        if (m_stats.m_restarts == 0)
-            res = m_engine(),
-            m_engine_init = true;
-        else if (m_stats.m_restarts % 1000 == 0)
-            res = m_engine.search_loop(),
-            m_engine_init = true;
-        if (res != l_undef) 
-            m_engine_model = true;   
-        return res;
-    }
-
 
     lbool sls::operator()() {
         lbool res = l_undef;
         m_stats.reset();
         m_stats.m_restarts = 0;
-        m_engine_model = false;
-        m_engine_init = false;
 
         do {
             res = search1();
             if (res != l_undef)
                 break;
             trace();
-            //res = search2();
-            if (res != l_undef)
-                break;
             reinit_eval();
         } 
         while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
@@ -300,26 +238,8 @@ namespace bv {
         }
     }
 
-
-    model_ref sls::get_model() {
-        if (m_engine_model)
-            return m_engine.get_model();
-
-        model_ref mdl = alloc(model, m);         
-        auto& terms = m_eval.sort_assertions(m_terms.assertions());
-        for (expr* e : terms) {
-            if (!is_uninterp_const(e))
-                continue;
-            auto f = to_app(e)->get_decl();
-            auto v = m_eval.get_value(to_app(e));
-            if (v)
-                mdl->register_decl(f, v);
-        }
-        terms.reset();
-        return mdl;
-    }
-
     std::ostream& sls::display(std::ostream& out) { 
+#if 0
         auto& terms = m_eval.sort_assertions(m_terms.assertions());
         for (expr* e : terms) {
             out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " ";
@@ -333,6 +253,7 @@ namespace bv {
             out << "\n";
         }
         terms.reset();
+#endif
         return out; 
     }
 
@@ -344,7 +265,6 @@ namespace bv {
         m_terms.updt_params(_p);
         params_ref q = _p;
         q.set_uint("max_restarts", 10);
-        m_engine.updt_params(q);
     }
 
     std::ostream& sls::trace_repair(bool down, expr* e) {
diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h
index 987cebcdb..c72e1d172 100644
--- a/src/ast/sls/bv_sls.h
+++ b/src/ast/sls/bv_sls.h
@@ -26,11 +26,10 @@ Author:
 #include "ast/sls/sls_valuation.h"
 #include "ast/sls/bv_sls_terms.h"
 #include "ast/sls/bv_sls_eval.h"
-#include "ast/sls/sls_engine.h"
 #include "ast/bv_decl_plugin.h"
 #include "model/model.h"
 
-namespace bv {
+namespace bvu {
 
 
     class sls {
@@ -42,15 +41,14 @@ namespace bv {
 
         ast_manager&        m;
         bv_util             bv;
-        sls_terms           m_terms;
-        sls_eval            m_eval;
-        sls_stats           m_stats;
+        bv::sls_terms           m_terms;
+        bv::sls_eval            m_eval;
+        bv::sls_stats           m_stats;
         indexed_uint_set    m_repair_up, m_repair_roots;
         unsigned            m_repair_down = UINT_MAX;
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;
-        sls_engine          m_engine;
         bool                m_engine_model = false;
         bool                m_engine_init = false;
         std::function<expr_ref()> m_get_unit;
@@ -78,11 +76,6 @@ namespace bv {
     public:
         sls(ast_manager& m, params_ref const& p);
                 
-        /**
-        * Add constraints
-        */
-        void assert_expr(expr* e) { m_terms.assert_expr(e); m_engine.assert_expr(e); }
-
         /*
         * Invoke init after all expressions are asserted. 
         */
@@ -110,17 +103,17 @@ namespace bv {
         lbool operator()();
 
         void updt_params(params_ref const& p);
-        void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); m_engine.collect_statistics(st); }
-        void reset_statistics() { m_stats.reset(); m_engine.reset_statistics(); }
+        void collect_statistics(statistics& st) const { m_stats.collect_statistics(st);  }
+        void reset_statistics() { m_stats.reset(); }
 
-        unsigned get_num_moves() { return m_stats.m_moves + m_engine.get_stats().m_moves; }
+        unsigned get_num_moves() { return m_stats.m_moves; }
 
         std::ostream& display(std::ostream& out);
 
         /**
         * Retrieve valuation
         */
-        sls_valuation const& wval(expr* e) const { return m_eval.wval(e); }
+        bv::sls_valuation const& wval(expr* e) const { return m_eval.wval(e); }
 
         model_ref get_model();
 
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index f2dd165ab..27a4acf4e 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -17,65 +17,31 @@ Author:
 
 namespace bv {
 
-    sls_eval::sls_eval(ast_manager& m): 
-        m(m), 
+    sls_eval::sls_eval(sls_terms& terms, sls::context& ctx): 
+        m(ctx.get_manager()),
+        ctx(ctx),
+        terms(terms),
         bv(m),
-        m_fix(*this)
+        m_fix(*this, terms, ctx)
     {}   
 
-    void sls_eval::init_eval(expr_ref_vector const& es, std::function<bool(expr*, unsigned)> const& eval) {
-        auto& terms = sort_assertions(es);
-        for (expr* e : terms) {
+    void sls_eval::init_eval(std::function<bool(expr*, unsigned)> const& eval) {
+        for (expr* e : terms.subterms()) {
             if (!is_app(e))
                 continue;
             app* a = to_app(e);
-            if (bv.is_bv(e)) 
-                add_bit_vector(a);
-            if (a->get_family_id() == basic_family_id)
-                init_eval_basic(a);
-            else if (a->get_family_id() == bv.get_family_id())
+            if (!bv.is_bv(e))
+                continue;
+            add_bit_vector(a);
+            if (a->get_family_id() == bv.get_family_id())
                 init_eval_bv(a);
             else if (is_uninterp(e)) {
-                if (bv.is_bv(e)) {
-                    auto& v = wval(e);
-                    for (unsigned i = 0; i < v.bw; ++i)
-                        m_tmp.set(i, eval(e, i));
-                    v.set_repair(random_bool(), m_tmp);
-                }
-                else if (m.is_bool(e))
-                    m_eval.setx(e->get_id(), eval(e, 0), false);
-            }
-            else {
-                TRACE("sls", tout << "Unhandled expression " << mk_pp(e, m) << "\n");
+                auto& v = wval(e);
+                for (unsigned i = 0; i < v.bw; ++i)
+                    m_tmp.set(i, eval(e, i));
+                v.set_repair(random_bool(), m_tmp);                
             }
         }
-        terms.reset();
-    }
-
-    /**
-    * Sort all sub-expressions by depth, smallest first.
-    */
-    ptr_vector<expr>& sls_eval::sort_assertions(expr_ref_vector const& es) {
-        expr_fast_mark1 mark;
-        for (expr* e : es) {
-            if (!mark.is_marked(e)) {
-                mark.mark(e);
-                m_todo.push_back(e);
-            }
-        }
-        for (unsigned i = 0; i < m_todo.size(); ++i) {
-            auto e = m_todo[i];
-            if (!is_app(e))
-                continue;
-            for (expr* arg : *to_app(e)) {
-                if (!mark.is_marked(arg)) {
-                    mark.mark(arg);
-                    m_todo.push_back(arg);
-                }
-            }
-        }
-        std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
-        return m_todo;
     }
 
     bool sls_eval::add_bit_vector(app* e) {
@@ -115,83 +81,10 @@ namespace bv {
         return r;
     }
 
-    void sls_eval::init_eval_basic(app* e) {
-        auto id = e->get_id();
-        if (m.is_bool(e)) 
-            m_eval.setx(id, bval1(e), false);                    
-        else if (m.is_ite(e)) {
-            SASSERT(bv.is_bv(e->get_arg(1)));
-            auto& val = wval(e);
-            auto& val_th = wval(e->get_arg(1));
-            auto& val_el = wval(e->get_arg(2));
-            if (bval0(e->get_arg(0))) 
-                val.set(val_th.bits());            
-            else
-                val.set(val_el.bits()); 
-        }
-        else {
-            UNREACHABLE();
-        }             
-    }
 
     void sls_eval::init_eval_bv(app* e) {
         if (bv.is_bv(e)) 
-            eval(e).commit_eval();        
-        else if (m.is_bool(e)) 
-            m_eval.setx(e->get_id(), bval1_bv(e), false);        
-    }
-
-    bool sls_eval::bval1_basic(app* e) const {
-        SASSERT(m.is_bool(e));
-        SASSERT(e->get_family_id() == basic_family_id);
-
-        auto id = e->get_id();
-        switch (e->get_decl_kind()) {
-        case OP_TRUE:
-            return true;
-        case OP_FALSE:
-            return false;
-        case OP_AND:
-            return all_of(*to_app(e), [&](expr* arg) { return bval0(arg); });
-        case OP_OR:
-            return any_of(*to_app(e), [&](expr* arg) { return bval0(arg); });
-        case OP_NOT:
-            return !bval0(e->get_arg(0));
-        case OP_XOR: {
-            bool r = false;
-            for (auto* arg : *to_app(e))
-                r ^= bval0(arg);
-            return r;
-        }
-        case OP_IMPLIES: {
-            auto a = e->get_arg(0);
-            auto b = e->get_arg(1);
-            return !bval0(a) || bval0(b);
-        }
-        case OP_ITE: {
-            auto c = bval0(e->get_arg(0));
-            return bval0(c ? e->get_arg(1) : e->get_arg(2));
-        }
-        case OP_EQ: {
-            auto a = e->get_arg(0);
-            auto b = e->get_arg(1);
-            if (m.is_bool(a))
-                return bval0(a) == bval0(b);
-            else if (bv.is_bv(a)) {
-                auto const& va = wval(a);
-                auto const& vb = wval(b);
-                return va.eq(vb);
-            }
-            return m.are_equal(a, b);
-        }
-        case OP_DISTINCT:
-        default:
-            verbose_stream() << mk_bounded_pp(e, m) << "\n";
-            UNREACHABLE();
-            break;
-        }
-        UNREACHABLE();
-        return false;
+            eval(e).commit_eval();               
     }
     
     bool sls_eval::can_eval1(app* e) const {
@@ -296,12 +189,10 @@ namespace bv {
     }
 
     bool sls_eval::bval1(app* e) const {
-        if (e->get_family_id() == basic_family_id)
-            return bval1_basic(e);
         if (e->get_family_id() == bv.get_fid())
             return bval1_bv(e);
-        SASSERT(is_uninterp_const(e));
-        return bval0(e); 
+        UNREACHABLE();
+        return false;
     }
 
     sls_valuation& sls_eval::eval(app* e) const {
@@ -701,41 +592,11 @@ namespace bv {
     }
 
     bool sls_eval::try_repair(app* e, unsigned i) {      
-        if (is_fixed0(e->get_arg(i)))
-            return false;
-        else if (e->get_family_id() == basic_family_id)
-            return try_repair_basic(e, i);
         if (e->get_family_id() == bv.get_family_id())
             return try_repair_bv(e, i);
         return false;
     }
 
-    bool sls_eval::try_repair_basic(app* e, unsigned i) {
-        switch (e->get_decl_kind()) {
-        case OP_AND:
-            return try_repair_and_or(e, i);
-        case OP_OR:
-            return try_repair_and_or(e, i);
-        case OP_NOT:
-            return try_repair_not(e);
-        case OP_FALSE:             
-            return false;
-        case OP_TRUE:             
-            return false;
-        case OP_EQ:
-            return try_repair_eq(e, i);
-        case OP_IMPLIES: 
-            return try_repair_implies(e, i);
-        case OP_XOR:
-            return try_repair_xor(e, i);
-        case OP_ITE:
-            return try_repair_ite(e, i);
-        default:
-            UNREACHABLE();
-            return false;
-        }
-    }
-
     bool sls_eval::try_repair_bv(app* e, unsigned i) {
         switch (e->get_decl_kind()) {
         case OP_BAND:
@@ -880,21 +741,7 @@ namespace bv {
         }
     }
 
-    bool sls_eval::try_repair_and_or(app* e, unsigned i) {
-        auto b = bval0(e);
-        auto child = e->get_arg(i);
-        if (b == bval0(child))
-            return false;
-        m_eval[child->get_id()] = b;
-        return true;
-    }
-
-    bool sls_eval::try_repair_not(app* e) {
-        auto child = e->get_arg(0);
-        m_eval[child->get_id()] = !bval0(e);
-        return true;
-    }
-
+#if 0
     bool sls_eval::try_repair_eq(app* e, unsigned i) {
         auto child = e->get_arg(i);        
         auto is_true = bval0(e);
@@ -911,6 +758,7 @@ namespace bv {
         }
         return false;
     }
+#endif
 
     bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {
@@ -939,47 +787,6 @@ namespace bv {
         }
     }
 
-    bool sls_eval::try_repair_xor(app* e, unsigned i) {
-        bool ev = bval0(e);
-        bool bv = bval0(e->get_arg(1 - i));
-        auto child = e->get_arg(i);
-        m_eval[child->get_id()] = ev != bv;
-        return true;
-    }
-
-    bool sls_eval::try_repair_ite(app* e, unsigned i) {
-        auto child = e->get_arg(i);
-        bool c = bval0(e->get_arg(0));
-        if (i == 0) {
-            m_eval[child->get_id()] = !c;
-            return true;
-        }
-        if (c != (i == 1))
-            return false;
-        if (m.is_bool(e)) {
-            m_eval[child->get_id()] = bval0(e);
-            return true;
-        }
-        if (bv.is_bv(e)) 
-            return wval(child).try_set(wval(e).bits());        
-        return false;
-    }
-
-    bool sls_eval::try_repair_implies(app* e, unsigned i) {
-        auto child = e->get_arg(i);
-        bool ev = bval0(e);
-        bool av = bval0(child);
-        bool bv = bval0(e->get_arg(1 - i));
-        if (i == 0) {
-            if (ev == (!av || bv))
-                return false;
-        }
-        else if (ev != (!bv || av))
-            return false;
-        m_eval[child->get_id()] = ev;
-        return true;
-    }
-
     //
     // e = a & b
     // e[i] = 1 -> a[i] = 1
@@ -1892,28 +1699,18 @@ namespace bv {
     }
 
     bool sls_eval::repair_up(expr* e) {
-        if (!is_app(e))
+        if (!bv.is_bv(e) || !is_app(e))
             return false;
-        if (m.is_bool(e)) {
-            auto b = bval1(to_app(e));
-            if (is_fixed0(e))
-                return b == bval0(e);
-            m_eval[e->get_id()] = b;
+        auto& v = eval(to_app(e));
+        for (unsigned i = 0; i < v.nw; ++i) {
+            if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
+                v.bits().copy_to(v.nw, v.eval);
+                return false;
+            }
+        }
+        if (v.commit_eval())
             return true;
-        }
-        if (bv.is_bv(e)) {
-            auto& v = eval(to_app(e));
-            
-            for (unsigned i = 0; i < v.nw; ++i)
-                if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
-                    v.bits().copy_to(v.nw, v.eval);
-                    return false;
-                }
-            if (v.commit_eval())
-                return true;
-            v.bits().copy_to(v.nw, v.eval);
-            return false;
-        }
+        v.bits().copy_to(v.nw, v.eval);
         return false;
     }
 
@@ -1923,21 +1720,15 @@ namespace bv {
     }
 
     void sls_eval::init_eval(app* t) {
-        if (m.is_bool(t))
-            set(t, bval1(t));
-        else if (bv.is_bv(t)) {
+        if (bv.is_bv(t)) {
             auto& v = wval(t);
             v.bits().copy_to(v.nw, v.eval);
         }
     }
 
     void sls_eval::commit_eval(app* e) {
-        if (m.is_bool(e)) {
-            set(e, bval1(e));
-        }
-        else {
-            VERIFY(wval(e).commit_eval());
-        }
+        if (bv.is_bv(e)) 
+            VERIFY(wval(e).commit_eval());        
     }
 
     void sls_eval::set_random(app* e) {
@@ -1983,6 +1774,7 @@ namespace bv {
     }
 
     std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) {
+#if 0
         auto& terms = sort_assertions(es);
         for (expr* e : terms) {
             out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " ";
@@ -1991,14 +1783,13 @@ namespace bv {
             display_value(out, e) << "\n";
         }
         terms.reset();
+#endif
         return out;
     }
 
     std::ostream& sls_eval::display_value(std::ostream& out, expr* e) {
         if (bv.is_bv(e)) 
             return out << wval(e);
-        if (m.is_bool(e))
-            return out << (bval0(e)?"T":"F");
         return out << "?";
     }
 }
diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h
index 4384660e7..9f087c4f4 100644
--- a/src/ast/sls/bv_sls_eval.h
+++ b/src/ast/sls/bv_sls_eval.h
@@ -19,17 +19,12 @@ Author:
 #include "ast/ast.h"
 #include "ast/sls/sls_valuation.h"
 #include "ast/sls/bv_sls_fixed.h"
+#include "ast/sls/sls_smt.h"
 #include "ast/bv_decl_plugin.h"
 
 namespace bv {
 
-    class sls_fixed;
-
-    class sls_eval_plugin {
-    public:
-        virtual ~sls_eval_plugin() {}
-        
-    };
+    class sls_terms;
 
     class sls_eval {
         struct config {
@@ -39,28 +34,24 @@ namespace bv {
         friend class sls_fixed;
         friend class sls_test;
         ast_manager&        m;
+        sls::context&       ctx;
+        sls_terms&          terms;
         bv_util             bv;
         sls_fixed           m_fix;
         mutable mpn_manager mpn;
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;
-
-        scoped_ptr_vector<sls_eval_plugin> m_plugins;
-
-
+        bool_vector         m_fixed;
+        
 
         scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation
-        bool_vector                      m_eval;   // expr-id -> boolean valuation
-        bool_vector                      m_fixed;  // expr-id -> is Boolean fixed
 
         mutable bvect m_tmp, m_tmp2, m_tmp3, m_tmp4, m_zero, m_one, m_minus_one;
         bvect m_a, m_b, m_nextb, m_nexta, m_aux;
 
         using bvval = sls_valuation;
 
-
-        void init_eval_basic(app* e);
         void init_eval_bv(app* e);
        
         /**
@@ -70,20 +61,13 @@ namespace bv {
         bool add_bit_vector(app* e);
         sls_valuation* alloc_valuation(app* e);
 
-        bool bval1_basic(app* e) const;
+        //bool bval1_basic(app* e) const;
         bool bval1_bv(app* e) const;  
 
         /**
         * Repair operations
         */
-        bool try_repair_basic(app* e, unsigned i);
         bool try_repair_bv(app * e, unsigned i);
-        bool try_repair_and_or(app* e, unsigned i);
-        bool try_repair_not(app* e);
-        bool try_repair_eq(app* e, unsigned i);
-        bool try_repair_xor(app* e, unsigned i);
-        bool try_repair_ite(app* e, unsigned i);
-        bool try_repair_implies(app* e, unsigned i);
         bool try_repair_band(bvect const& e, bvval& a, bvval const& b);
         bool try_repair_bor(bvect const& e, bvval& a, bvval const& b);
         bool try_repair_add(bvect const& e, bvval& a, bvval const& b);
@@ -136,32 +120,30 @@ namespace bv {
 
         bvect const& eval_value(app* e) const { return wval(e).eval; }
 
+        bool bval0(expr* e) const { return ctx.is_true(e); }
+
+        /**
+         * Retrieve evaluation based on immediate children.
+         */
+        bool bval1(app* e) const;
+        bool can_eval1(app* e) const;
+
     public:
-        sls_eval(ast_manager& m);
+        sls_eval(sls_terms& terms, sls::context& ctx);
 
-        void init_eval(expr_ref_vector const& es, std::function<bool(expr*, unsigned)> const& eval);
+        void init_eval(std::function<bool(expr*, unsigned)> const& eval);
 
-        void tighten_range(expr_ref_vector const& es) { m_fix.init(es); }
-
-        ptr_vector<expr>& sort_assertions(expr_ref_vector const& es);
+        void tighten_range() { m_fix.init(); }
 
         /**
          * Retrieve evaluation based on cache.
          * bval - Boolean values
          * wval - Word (bit-vector) values
-         */
-        
-        bool bval0(expr* e) const { return m_eval[e->get_id()]; }
+         */        
 
         sls_valuation& wval(expr* e) const;
 
         bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
-
-        /**
-         * Retrieve evaluation based on immediate children.         
-         */
-        bool bval1(app* e) const;
-        bool can_eval1(app* e) const;
         
         sls_valuation& eval(app* e) const;
 
@@ -176,18 +158,10 @@ namespace bv {
         bool re_eval_is_correct(app* e);
 
         expr_ref get_value(app* e);
-
-        /**
-         * Override evaluaton.
-         */
-
-        void set(expr* e, bool b) {
-            m_eval[e->get_id()] = b;
-        }        
-
+      
         /*
-        * Try to invert value of child to repair value assignment of parent.
-        */
+         * Try to invert value of child to repair value assignment of parent.
+         */
 
         bool try_repair(app* e, unsigned i);
 
diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp
index 9f897a7bd..7613797dc 100644
--- a/src/ast/sls/bv_sls_fixed.cpp
+++ b/src/ast/sls/bv_sls_fixed.cpp
@@ -14,55 +14,48 @@ 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"
 
 namespace bv {
 
-    sls_fixed::sls_fixed(sls_eval& ev):
+    sls_fixed::sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx):
         ev(ev),
+        terms(terms),
         m(ev.m),
-        bv(ev.bv)
+        bv(ev.bv),
+        ctx(ctx)
     {}
 
-    void sls_fixed::init(expr_ref_vector const& es) {
-        ev.sort_assertions(es);
-        for (expr* e : ev.m_todo) {
-            if (!is_app(e))
-                continue;
-            app* a = to_app(e);
-            ev.m_fixed.setx(a->get_id(), is_fixed1(a), false);
-            if (a->get_family_id() == basic_family_id)
-                init_fixed_basic(a);
-            else if (a->get_family_id() == bv.get_family_id())
-                init_fixed_bv(a);
-            else
-                ;
-        }
-        init_ranges(es);
-        ev.m_todo.reset();        
-    }
+    void sls_fixed::init() {
+        for (auto e : terms.subterms())
+            set_fixed(e);
 
-
-    void sls_fixed::init_ranges(expr_ref_vector const& es) {
-        for (expr* e : es) {
-            bool sign = m.is_not(e, e);
-            if (is_app(e))
-                init_range(to_app(e), sign);
+        for (auto const& c : ctx.clauses()) {
+            if (c.m_clause.size() == 1) {
+                auto lit = c.m_clause[0];
+                auto a = ctx.atom(lit.var());
+                if (!a)
+                    continue;
+                a = terms.translated(a);
+                if (is_app(a))
+                    init_range(to_app(a), lit.sign());
+                ev.m_fixed.setx(a->get_id(), true, false);
+            }
         }
-        
-        for (expr* e : ev.m_todo)
-            propagate_range_up(e);
+        for (auto e : terms.subterms())
+            propagate_range_up(e);    
     }
 
     void sls_fixed::propagate_range_up(expr* e) {
         expr* t, * s;
         rational v;
         if (bv.is_concat(e, t, s)) {
-            auto& vals = wval(s);
+            auto& vals = ev.wval(s);
             if (vals.lo() != vals.hi() && (vals.lo() < vals.hi() || vals.hi() == 0))
                 // lo <= e
                 add_range(e, vals.lo(), rational::zero(), false);
-            auto valt = wval(t);
+            auto valt = ev.wval(t);
             if (valt.lo() != valt.hi() && (valt.lo() < valt.hi() || valt.hi() == 0)) {
                 // (2^|s|) * lo <= e < (2^|s|) * hi
                 auto p = rational::power_of_two(bv.get_bv_size(s));
@@ -70,12 +63,12 @@ namespace bv {
             }
         }        
         else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) {
-            auto& val = wval(t);
+            auto& val = ev.wval(t);
             if (val.lo() != val.hi()) 
                 add_range(e, v + val.lo(), v + val.hi(), false);  
         }
         else if (bv.is_bv_add(e, t, s) && bv.is_numeral(s, v)) {
-            auto& val = wval(t);
+            auto& val = ev.wval(t);
             if (val.lo() != val.hi()) 
                 add_range(e, v + val.lo(), v + val.hi(), false);          
         }
@@ -83,7 +76,7 @@ namespace bv {
         // x in [lo, hi[ => -x in [-hi + 1, -lo + 1[
         else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) && 
             v + 1 == rational::power_of_two(bv.get_bv_size(e))) {
-            auto& val = wval(t);
+            auto& val = ev.wval(t);
             if (val.lo() != val.hi())
                 add_range(e, -val.hi() + 1, - val.lo() + 1, false);
         }
@@ -149,7 +142,7 @@ namespace bv {
             return true;
         }
         else if (bv.is_bit2bool(e, s, idx)) {
-            auto& val = wval(s);
+            auto& val = ev.wval(s);
             val.try_set_bit(idx, !sign);
             val.fixed.set(idx, true);
             val.tighten_range();
@@ -188,13 +181,13 @@ namespace bv {
         if (bv.is_extract(t, lo, hi, s)) {
             if (hi == lo) {
                 sign = sign ? a == 1 : a == 0;
-                auto& val = wval(s);
+                auto& val = ev.wval(s);
                 if (val.try_set_bit(lo, !sign)) 
                     val.fixed.set(lo, true);                                    
                 val.tighten_range();
             }
             else if (!sign) {
-                auto& val = wval(s);
+                auto& val = ev.wval(s);
                 for (unsigned i = lo; i <= hi; ++i) 
                     if (val.try_set_bit(i, a.get_bit(i - lo)))
                         val.fixed.set(i, true);                
@@ -236,7 +229,7 @@ namespace bv {
     }
 
     bool sls_fixed::add_range(expr* e, rational lo, rational hi, bool sign) {
-        auto& v = wval(e);
+        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)));
         if (lo == hi)
@@ -285,50 +278,19 @@ namespace bv {
             x = nullptr;
     }
 
-    sls_valuation& sls_fixed::wval(expr* e) {
-        return ev.wval(e);
-    }
-
-    void sls_fixed::init_fixed_basic(app* e) {
-        if (bv.is_bv(e) && m.is_ite(e)) {
-            auto& val = wval(e);
-            auto& val_th = wval(e->get_arg(1));
-            auto& val_el = wval(e->get_arg(2));
-            for (unsigned i = 0; i < val.nw; ++i)
-                val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i));
-        }
-    }
-
-    void sls_fixed::init_fixed_bv(app* e) {
-        if (bv.is_bv(e))
-            set_fixed_bw(e);
-    }
-
     bool sls_fixed::is_fixed1(app* e) const {
         if (is_uninterp(e))
             return false;
-        if (e->get_family_id() == basic_family_id)
-            return is_fixed1_basic(e);
         return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); });
     }
-
-    bool sls_fixed::is_fixed1_basic(app* e) const {
-        switch (e->get_decl_kind()) {
-        case OP_TRUE:
-        case OP_FALSE:
-            return true;
-        case OP_AND:
-            return any_of(*e, [&](expr* arg) { return ev.is_fixed0(arg) && !ev.bval0(e); });
-        case OP_OR:
-            return any_of(*e, [&](expr* arg) { return ev.is_fixed0(arg) && ev.bval0(e); });
-        default:
-            return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); });
-        }
-    }
     
-    void sls_fixed::set_fixed_bw(app* e) {
-        SASSERT(bv.is_bv(e));
-        SASSERT(e->get_family_id() == bv.get_fid());
+    void sls_fixed::set_fixed(expr* _e) {
+        if (!is_app(_e))
+            return;
+        auto e = to_app(_e);
+        if (!bv.is_bv(e))
+            return;
+
         auto& v = ev.wval(e);
         if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) {
             for (unsigned i = 0; i < v.bw; ++i)
@@ -336,39 +298,54 @@ namespace bv {
             ev.m_fixed.setx(e->get_id(), true, false);
             return;
         }
+
+        if (m.is_ite(e)) {
+            auto& val_th = ev.wval(e->get_arg(1));
+            auto& val_el = ev.wval(e->get_arg(2));
+            for (unsigned i = 0; i < v.nw; ++i)
+                v.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i));
+            return;
+        }
+
+        if (e->get_family_id() != bv.get_fid())
+            return;
         switch (e->get_decl_kind()) {
         case OP_BAND: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits)
             for (unsigned i = 0; i < a.nw; ++i)
                 v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i));
             break;
         }
         case OP_BOR: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits)
             for (unsigned i = 0; i < a.nw; ++i)
                 v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i));
             break;
         }
         case OP_BXOR: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             for (unsigned i = 0; i < a.nw; ++i)
                 v.fixed[i] = a.fixed[i] & b.fixed[i];
             break;
         }
         case OP_BNOT: {
-            auto& a = wval(e->get_arg(0));
+            auto& a = ev.wval(e->get_arg(0));
             for (unsigned i = 0; i < a.nw; ++i)
                 v.fixed[i] = a.fixed[i];
             break;
         }
         case OP_BADD: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             bool pfixed = true;
             for (unsigned i = 0; i < v.bw; ++i) {
                 if (pfixed && a.fixed.get(i) && b.fixed.get(i)) 
@@ -386,8 +363,9 @@ namespace bv {
             break;
         }
         case OP_BMUL: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             unsigned j = 0, k = 0, zj = 0, zk = 0, hzj = 0, hzk = 0;
             // i'th bit depends on bits j + k = i
             // if the first j, resp k bits are 0, the bits j + k are 0  
@@ -437,8 +415,9 @@ namespace bv {
             break;
         }
         case OP_CONCAT: {
-            auto& a = wval(e->get_arg(0));
-            auto& b = wval(e->get_arg(1));
+            SASSERT(e->get_num_args() == 2);
+            auto& a = ev.wval(e->get_arg(0));
+            auto& b = ev.wval(e->get_arg(1));
             for (unsigned i = 0; i < b.bw; ++i)
                 v.fixed.set(i, b.fixed.get(i));
             for (unsigned i = 0; i < a.bw; ++i)
@@ -449,13 +428,13 @@ namespace bv {
             expr* child;
             unsigned lo, hi;
             VERIFY(bv.is_extract(e, lo, hi, child));
-            auto& a = wval(child);
+            auto& a = ev.wval(child);
             for (unsigned i = lo; i <= hi; ++i)
                 v.fixed.set(i - lo, a.fixed.get(i));
             break;
         }
         case OP_BNEG: {
-            auto& a = wval(e->get_arg(0));
+            auto& a = ev.wval(e->get_arg(0));
             bool pfixed = true;
             for (unsigned i = 0; i < v.bw; ++i) {
                 if (pfixed && a.fixed.get(i))
diff --git a/src/ast/sls/bv_sls_fixed.h b/src/ast/sls/bv_sls_fixed.h
index 2e88484c5..01fccecf9 100644
--- a/src/ast/sls/bv_sls_fixed.h
+++ b/src/ast/sls/bv_sls_fixed.h
@@ -18,18 +18,21 @@ Author:
 
 #include "ast/ast.h"
 #include "ast/sls/sls_valuation.h"
+#include "ast/sls/sls_smt.h"
 #include "ast/bv_decl_plugin.h"
 
 namespace bv {
 
     class sls_eval;
+    class sls_terms;
     
     class sls_fixed {
         sls_eval&           ev;
+        sls_terms&          terms;
         ast_manager&        m;
         bv_util&            bv;
+        sls::context&       ctx;
 
-        void init_ranges(expr_ref_vector const& es);
         bool init_range(app* e, bool sign);
         void propagate_range_up(expr* e);
         bool init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign);
@@ -37,19 +40,11 @@ namespace bv {
         bool init_eq(expr* e, rational const& v, bool sign);
         bool add_range(expr* e, rational lo, rational hi, bool sign);
 
-        void init_fixed_basic(app* e);
-        void init_fixed_bv(app* e);
-
         bool is_fixed1(app* e) const;
-        bool is_fixed1_basic(app* e) const;
-        void set_fixed_bw(app* e);
-
-        sls_valuation& wval(expr* e);
+        void set_fixed(expr* e);
 
     public:
-        sls_fixed(sls_eval& ev);
-
-        void init(expr_ref_vector const& es);
-
+        sls_fixed(sls_eval& ev, sls_terms& terms, sls::context& ctx);
+        void init();
     };
 }
diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp
index ed1bf2396..084fc11b8 100644
--- a/src/ast/sls/bv_sls_terms.cpp
+++ b/src/ast/sls/bv_sls_terms.cpp
@@ -20,57 +20,50 @@ Author:
 
 #include "ast/ast_ll_pp.h"
 #include "ast/sls/bv_sls.h"
-#include "ast/rewriter/th_rewriter.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/bv_rewriter.h"
 
 namespace bv {
 
-    sls_terms::sls_terms(ast_manager& m): 
-        m(m), 
+    sls_terms::sls_terms(sls::context& ctx):
+        ctx(ctx),
+        m(ctx.get_manager()), 
         bv(m),
-        m_rewriter(m),
-        m_assertions(m),
-        m_pinned(m),
-        m_translated(m), 
-        m_terms(m){}
+        m_translated(m) {}
 
+    void sls_terms::init() {
+        for (auto t : ctx.subterms())
+            ensure_binary(t);
 
-    void sls_terms::assert_expr(expr* e) {
-        m_assertions.push_back(ensure_binary(e));
-    }
-
-    expr* sls_terms::ensure_binary(expr* e) {
-        expr* top = e;
-        m_pinned.push_back(e);
-        m_todo.push_back(e);
-        {
-            expr_fast_mark1 mark;
-            for (unsigned i = 0; i < m_todo.size(); ++i) {
-                expr* e = m_todo[i];
-                if (!is_app(e))
+        m_subterms.reset();
+        expr_fast_mark1 visited;
+        for (auto t : ctx.subterms())
+            m_subterms.push_back(translated(t));
+        for (auto t : m_subterms)
+            visited.mark(t, true);
+        for (unsigned i = 0; i < m_subterms.size(); ++i) {
+            auto t = m_subterms[i];
+            if (!is_app(t))
+                continue;
+            app* a = to_app(t);
+            for (expr* arg : *a) {
+                if (visited.is_marked(arg))
                     continue;
-                if (m_translated.get(e->get_id(), nullptr))
-                    continue;
-                if (mark.is_marked(e))
-                    continue;
-                mark.mark(e);
-                for (auto arg : *to_app(e))
-                    m_todo.push_back(arg);
+                visited.mark(arg, true);
+                m_subterms.push_back(arg);
             }
         }
-        std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
-        for (expr* e : m_todo)
-            ensure_binary_core(e);
-        m_todo.reset();
-        return m_translated.get(top->get_id());
+        std::stable_sort(m_subterms.begin(), m_subterms.end(), 
+            [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
     }
 
-    void sls_terms::ensure_binary_core(expr* e) {
+    void sls_terms::ensure_binary(expr* e) {
         if (m_translated.get(e->get_id(), nullptr))
             return;
         
         app* a = to_app(e);
         auto arg = [&](unsigned i) {
-            return m_translated.get(a->get_arg(i)->get_id());
+            return a->get_arg(i);
         };
         unsigned num_args = a->get_num_args();
         expr_ref r(m);
@@ -79,16 +72,7 @@ namespace bv {
         for (unsigned i = 1; i < num_args; ++i)\
             r = oper(r, arg(i)); \
 
-        if (m.is_and(e)) {
-            FOLD_OP(m.mk_and);
-        }
-        else if (m.is_or(e)) {
-            FOLD_OP(m.mk_or);
-        }
-        else if (m.is_xor(e)) {
-            FOLD_OP(m.mk_xor);
-        }
-        else if (bv.is_bv_and(e)) {
+        if (bv.is_bv_and(e)) {
             FOLD_OP(bv.mk_bv_and);
         }
         else if (bv.is_bv_or(e)) {
@@ -106,13 +90,6 @@ namespace bv {
         else if (bv.is_concat(e)) {
             FOLD_OP(bv.mk_concat);
         }
-        else if (m.is_distinct(e)) {
-            expr_ref_vector es(m);
-            for (unsigned i = 0; i < num_args; ++i)
-                for (unsigned j = i + 1; j < num_args; ++j)
-                    es.push_back(m.mk_not(m.mk_eq(arg(i), arg(j))));
-            r = m.mk_and(es);
-        }
         else if (bv.is_bv_sdiv(e) || bv.is_bv_sdiv0(e) || bv.is_bv_sdivi(e)) {
             r = mk_sdiv(arg(0), arg(1));
         }
@@ -122,12 +99,8 @@ namespace bv {
         else if (bv.is_bv_srem(e) || bv.is_bv_srem0(e) || bv.is_bv_sremi(e)) {
             r = mk_srem(arg(0), arg(1));
         }
-        else {
-            for (unsigned i = 0; i < num_args; ++i)
-                m_args.push_back(arg(i));
-            r = m.mk_app(a->get_decl(), num_args, m_args.data());
-            m_args.reset();
-        }
+        else
+            r = e;                   
         m_translated.setx(e->get_id(), r);
     }
 
@@ -140,19 +113,20 @@ namespace bv {
         // x < 0, y > 0 -> -d
         // x > 0, y > 0 -> d
         // x < 0, y < 0 -> d
+        bool_rewriter br(m);
+        bv_rewriter bvr(m);
         unsigned sz = bv.get_bv_size(x);
         rational N = rational::power_of_two(sz);
         expr_ref z(bv.mk_zero(sz), m);
-        expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
-        expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
-        expr* absx = m.mk_ite(signx, bv.mk_bv_neg(x), x);
-        expr* absy = m.mk_ite(signy, bv.mk_bv_neg(y), y);
+        expr* signx = bvr.mk_ule(bv.mk_numeral(N / 2, sz), x);
+        expr* signy = bvr.mk_ule(bv.mk_numeral(N / 2, sz), y);
+        expr* absx = br.mk_ite(signx, bvr.mk_bv_neg(x), x);
+        expr* absy = br.mk_ite(signy, bvr.mk_bv_neg(y), y);
         expr* d = bv.mk_bv_udiv(absx, absy);
-        expr_ref r(m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d)), m);
-        r = m.mk_ite(m.mk_eq(z, y),
-                     m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)),
-                     m.mk_ite(m.mk_eq(x, z), z, r));
-        m_rewriter(r);
+        expr_ref r(br.mk_ite(br.mk_eq(signx, signy), d, bvr.mk_bv_neg(d)), m);
+        r = br.mk_ite(br.mk_eq(z, y),
+                     br.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)),
+                     br.mk_ite(br.mk_eq(x, z), z, r));
         return r;
     }
 
@@ -164,18 +138,19 @@ namespace bv {
         // x < 0, y >= 0 ->  y - u
         // x >= 0, y < 0 ->  y + u
         // x >= 0, y >= 0 ->  u
+        bool_rewriter br(m);
+        bv_rewriter bvr(m);
         unsigned sz = bv.get_bv_size(x);
         expr_ref z(bv.mk_zero(sz), m);
-        expr_ref abs_x(m.mk_ite(bv.mk_sle(z, x), x, bv.mk_bv_neg(x)), m);
-        expr_ref abs_y(m.mk_ite(bv.mk_sle(z, y), y, bv.mk_bv_neg(y)), m);
-        expr_ref u(bv.mk_bv_urem(abs_x, abs_y), m);
+        expr_ref abs_x(br.mk_ite(bvr.mk_sle(z, x), x, bvr.mk_bv_neg(x)), m);
+        expr_ref abs_y(br.mk_ite(bvr.mk_sle(z, y), y, bvr.mk_bv_neg(y)), m);
+        expr_ref u(bvr.mk_bv_urem(abs_x, abs_y), m);
         expr_ref r(m);
-        r = m.mk_ite(m.mk_eq(u, z), z,
-                m.mk_ite(m.mk_eq(y, z), x,
-                    m.mk_ite(m.mk_and(bv.mk_sle(z, x), bv.mk_sle(z, x)), u,
-                        m.mk_ite(bv.mk_sle(z, x), bv.mk_bv_add(y, u),
-                            m.mk_ite(bv.mk_sle(z, y), bv.mk_bv_sub(y, u), bv.mk_bv_neg(u))))));
-        m_rewriter(r);
+        r = br.mk_ite(br.mk_eq(u, z), z,
+                br.mk_ite(br.mk_eq(y, z), x,
+                    br.mk_ite(br.mk_and(bvr.mk_sle(z, x), bvr.mk_sle(z, x)), u,
+                        br.mk_ite(bvr.mk_sle(z, x), bvr.mk_bv_add(y, u),
+                            br.mk_ite(bv.mk_sle(z, y), bvr.mk_bv_sub(y, u), bvr.mk_bv_neg(u))))));
         return r;
     }
 
@@ -183,47 +158,11 @@ namespace bv {
         // y = 0 -> x
         // else x - sdiv(x, y) * y
         expr_ref r(m);
-        r = m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))),
-                     x, bv.mk_bv_sub(x, bv.mk_bv_mul(y, mk_sdiv(x, y))));
-        m_rewriter(r);
+        bool_rewriter br(m);
+        bv_rewriter bvr(m);
+        expr_ref z(bv.mk_zero(bv.get_bv_size(x)), m);
+        r = br.mk_ite(br.mk_eq(y, z), x, bvr.mk_bv_sub(x, bvr.mk_bv_mul(y, mk_sdiv(x, y))));
         return r;
     }
 
-
-    void sls_terms::init() {
-        // populate terms
-        expr_fast_mark1 mark;
-        for (expr* e : m_assertions)
-            m_todo.push_back(e);
-        while (!m_todo.empty()) {
-            expr* e = m_todo.back();
-            m_todo.pop_back();
-            if (mark.is_marked(e) || !is_app(e))
-                continue;
-            mark.mark(e);            
-            m_terms.setx(e->get_id(), to_app(e));
-            for (expr* arg : *to_app(e))
-                m_todo.push_back(arg);
-        }       
-        // populate parents
-        m_parents.reset();
-        m_parents.reserve(m_terms.size());
-        for (expr* e : m_terms) {
-            if (!e || !is_app(e))
-                continue;
-            for (expr* arg : *to_app(e))
-                m_parents[arg->get_id()].push_back(e);                
-        }
-        m_assertion_set.reset();
-        for (auto a : m_assertions)
-            m_assertion_set.insert(a->get_id());
-    }
-
-    void sls_terms::updt_params(params_ref const& p) {
-        params_ref q = p;
-        q.set_bool("flat", false);
-        m_rewriter.updt_params(q);
-    }
-
-
 }
diff --git a/src/ast/sls/bv_sls_terms.h b/src/ast/sls/bv_sls_terms.h
index a6294aa9c..a35ea5025 100644
--- a/src/ast/sls/bv_sls_terms.h
+++ b/src/ast/sls/bv_sls_terms.h
@@ -17,63 +17,41 @@ Author:
 #pragma once
 
 #include "util/lbool.h"
-#include "util/params.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/uint_set.h"
 #include "ast/ast.h"
-#include "ast/rewriter/th_rewriter.h"
+#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/bv_decl_plugin.h"
+#include "ast/sls/sls_smt.h"
 
 namespace bv {
 
     class sls_terms {
+        sls::context&       ctx;
         ast_manager&        m;
         bv_util             bv;
-        th_rewriter         m_rewriter;
-        ptr_vector<expr>    m_todo, m_args;
-        expr_ref_vector     m_assertions, m_pinned, m_translated;
-        app_ref_vector      m_terms;
-        vector<ptr_vector<expr>> m_parents;
-        tracked_uint_set    m_assertion_set;
+        expr_ref_vector     m_translated;
+        ptr_vector<expr>    m_subterms;
 
-        expr* ensure_binary(expr* e);
-        void ensure_binary_core(expr* e);
+        void ensure_binary(expr* e);
 
         expr_ref mk_sdiv(expr* x, expr* y);
         expr_ref mk_smod(expr* x, expr* y);
         expr_ref mk_srem(expr* x, expr* y);
 
     public:
-        sls_terms(ast_manager& m);
-
-        void updt_params(params_ref const& p);
-        
-        /**
-        * Add constraints
-        */
-        void assert_expr(expr* e);
+        sls_terms(sls::context& ctx);       
 
         /**
          * Initialize structures: assertions, parents, terms
          */        
         void init();
 
-        /**
-         * Accessors.
-         */
-        
-        ptr_vector<expr> const& parents(expr* e) const { return m_parents[e->get_id()]; }
+        expr* translated(expr* e) const { return m_translated.get(e->get_id(), nullptr); }
 
-        expr_ref_vector const& assertions() const { return m_assertions; }
-
-        app* term(unsigned id) const { return m_terms.get(id); }
-
-        app_ref_vector const& terms() const { return m_terms; }
-
-        bool is_assertion(expr* e) const { return m_assertion_set.contains(e->get_id()); }
+        ptr_vector<expr> const& subterms() const { return m_subterms; }
 
     };
 }
diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index 21820c8df..d72d337fa 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -11,8 +11,7 @@
 
   Author:        
 
-    Nikolaj Bjorner, Marijn Heule 2019-4-23
-     
+    Nikolaj Bjorner, Marijn Heule 2019-4-23     
 
   Notes:
   
diff --git a/src/ast/sls/sls_bv.cpp b/src/ast/sls/sls_bv.cpp
index 1a6cf04cd..b910ee1c5 100644
--- a/src/ast/sls/sls_bv.cpp
+++ b/src/ast/sls/sls_bv.cpp
@@ -6,8 +6,8 @@ namespace sls {
     bv_plugin::bv_plugin(context& ctx): 
         plugin(ctx),
         bv(m),
-        m_terms(m),
-        m_eval(m)
+        m_terms(ctx),
+        m_eval(m_terms, ctx)
     {}
 
     void bv_plugin::init_bool_var(sat::bool_var v) {
@@ -55,39 +55,9 @@ namespace sls {
     }
 
     std::pair<bool, app*> bv_plugin::next_to_repair() {
-        app* e = nullptr;
-        if (m_repair_down != UINT_MAX) {
-            e = m_terms.term(m_repair_down);
-            m_repair_down = UINT_MAX;
-            return { true, e };
-        }
 
-        if (!m_repair_up.empty()) {
-            unsigned index = m_repair_up.elem_at(ctx.rand(m_repair_up.size()));
-            m_repair_up.remove(index);
-            e = m_terms.term(index);
-            return { false, e };
-        }
-
-        while (!m_repair_roots.empty()) {
-            unsigned index = m_repair_roots.elem_at(ctx.rand(m_repair_roots.size()));
-            e = m_terms.term(index);
-            if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
-                SASSERT(m_eval.bval0(e));
-                return { true, e };
-            }
-            if (!m_eval.re_eval_is_correct(e)) {
-                init_repair_goal(e);
-                return { true, e };
-            }
-            m_repair_roots.remove(index);
-        }
 
         return { false, nullptr };
     }
 
-    void bv_plugin::init_repair_goal(app* e) {
-        m_eval.init_eval(e);
-    }
-
 }
diff --git a/src/ast/sls/sls_bv.h b/src/ast/sls/sls_bv.h
index c1ad0464a..c591c4a7d 100644
--- a/src/ast/sls/sls_bv.h
+++ b/src/ast/sls/sls_bv.h
@@ -33,7 +33,7 @@ namespace sls {
         unsigned            m_repair_down = UINT_MAX;
 
         std::pair<bool, app*> next_to_repair();
-        void init_repair_goal(app* e);
+
     public:
         bv_plugin(context& ctx);
         ~bv_plugin() override {}
diff --git a/src/ast/sls/sls_smt.cpp b/src/ast/sls/sls_smt.cpp
index 4bbd7c136..20138874a 100644
--- a/src/ast/sls/sls_smt.cpp
+++ b/src/ast/sls/sls_smt.cpp
@@ -29,7 +29,7 @@ namespace sls {
     }
 
     context::context(ast_manager& m, sat_solver_context& s) : 
-        m(m), s(s), m_atoms(m), m_subterms(m) {
+        m(m), s(s), m_atoms(m), m_allterms(m) {
         reset();
     }
 
@@ -40,7 +40,7 @@ namespace sls {
 
     void context::register_atom(sat::bool_var v, expr* e) { 
         m_atoms.setx(v, e); 
-        m_atom2bool_var.setx(e->get_id(), v, UINT_MAX);
+        m_atom2bool_var.setx(e->get_id(), v, sat::null_bool_var);
     }
     
     void context::reset() {
@@ -51,7 +51,7 @@ namespace sls {
         m_parents.reset();
         m_relevant.reset();
         m_visited.reset();
-        m_subterms.reset();
+        m_allterms.reset();
         register_plugin(alloc(cc_plugin, *this));
         register_plugin(alloc(arith_plugin, *this));
     }
@@ -86,6 +86,18 @@ namespace sls {
         return l_undef;
     }
 
+    bool context::is_true(expr* e) {
+        SASSERT(m.is_bool(e));
+        auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
+        SASSERT(v != sat::null_bool_var);
+        return is_true(sat::literal(v, false));
+    }
+
+    bool context::is_fixed(expr* e) {
+        // is this a Boolean literal that is a unit?
+        return false;
+    }
+
     expr_ref context::get_value(expr* e) {
         if (m.is_bool(e)) {
             auto v = m_atom2bool_var[e->get_id()];
@@ -144,7 +156,7 @@ namespace sls {
         auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
         if (v == sat::null_bool_var) {
             v = s.add_var();
-            register_subterms(e);
+            register_terms(e);
             register_atom(v, e);
             init_bool_var(v);
         }
@@ -170,18 +182,19 @@ namespace sls {
     void context::register_terms() {
         for (auto a : m_atoms)
             if (a)
-                register_subterms(a);
+                register_terms(a);
     }
 
-    void context::register_subterms(expr* e) {
+    void context::register_terms(expr* e) {
         auto is_visited = [&](expr* e) {
-            return nullptr != m_subterms.get(e->get_id(), nullptr);
+            return nullptr != m_allterms.get(e->get_id(), nullptr);
         };
         auto visit = [&](expr* e) {
-            m_subterms.setx(e->get_id(), e);
+            m_allterms.setx(e->get_id(), e);
         };
         if (is_visited(e))
             return;
+        m_subterms.reset();
         m_todo.push_back(e);
         while (!m_todo.empty()) {
             expr* e = m_todo.back();
@@ -216,6 +229,17 @@ namespace sls {
                 p->register_term(e);
     }
 
+    ptr_vector<expr> const& context::subterms() {
+        if (!m_subterms.empty())
+            return m_subterms;
+        for (auto e : m_allterms)
+            if (e)
+                m_subterms.push_back(e);
+        std::stable_sort(m_subterms.begin(), m_subterms.end(), 
+            [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
+        return m_subterms;
+    }
+
     void context::reinit_relevant() {
         m_relevant.reset();
         m_visited.reset();
diff --git a/src/ast/sls/sls_smt.h b/src/ast/sls/sls_smt.h
index 3f555300c..3b0e16c7a 100644
--- a/src/ast/sls/sls_smt.h
+++ b/src/ast/sls/sls_smt.h
@@ -80,7 +80,8 @@ namespace sls {
         random_gen m_rand;
         bool m_initialized = false;
         bool m_new_constraint = false;
-        expr_ref_vector m_subterms;
+        expr_ref_vector m_allterms;
+        ptr_vector<expr> m_subterms;
 
         void register_plugin(plugin* p);
 
@@ -88,7 +89,7 @@ namespace sls {
         void init_bool_var(sat::bool_var v);
         void register_terms();
         ptr_vector<expr> m_todo;
-        void register_subterms(expr* e);
+        void register_terms(expr* e);
         void register_term(expr* e);
         sat::bool_var mk_atom(expr* e);
         
@@ -119,9 +120,12 @@ namespace sls {
 
         // Between plugin solvers
         expr_ref get_value(expr* e);
+        bool is_true(expr* e);
+        bool is_fixed(expr* e);
         void set_value(expr* e, expr* v);
         bool is_relevant(expr* e);  
         void add_constraint(expr* e);
+        ptr_vector<expr> const& subterms();        
         ast_manager& get_manager() { return m; }
         std::ostream& display(std::ostream& out) const;
     };
diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h
index 92a64955c..e04b82055 100644
--- a/src/sat/smt/sls_solver.h
+++ b/src/sat/smt/sls_solver.h
@@ -19,8 +19,8 @@ Author:
 
 #include "util/rlimit.h"
 #include "ast/sls/bv_sls.h"
-#include "sat/smt/sat_th.h"
 #include "ast/sls/sat_ddfw.h"
+#include "sat/smt/sat_th.h"
 
 
 #ifdef SINGLE_THREAD
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index f484372c8..f438d33a0 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -124,116 +124,11 @@ public:
 
 };
 
-class bv_sls_tactic : public tactic {
-    ast_manager& m;
-    params_ref   m_params;
-    bv::sls*     m_sls;
-    statistics   m_st;
-
-public:
-    bv_sls_tactic(ast_manager& _m, params_ref const& p) :
-        m(_m),
-        m_params(p) {
-        m_sls = alloc(bv::sls, m, p);
-    }
-
-    tactic* translate(ast_manager& m) override {
-        return alloc(bv_sls_tactic, m, m_params);
-    }
-
-    ~bv_sls_tactic() override {
-        dealloc(m_sls);
-    }
-
-    char const* name() const override { return "bv-sls"; }
-
-    void updt_params(params_ref const& p) override {
-        m_params.append(p);
-        m_sls->updt_params(m_params);
-    }
-
-    void collect_param_descrs(param_descrs& r) override {
-        sls_params::collect_param_descrs(r);
-    }
-
-    void run(goal_ref const& g, model_converter_ref& mc) {
-        if (g->inconsistent()) {
-            mc = nullptr;
-            return;
-        }
-
-        for (unsigned i = 0; i < g->size(); i++)
-            m_sls->assert_expr(g->form(i));
-
-        m_sls->init();
-        std::function<bool(expr*, unsigned)> false_eval = [&](expr* e, unsigned idx) {
-            return false;
-        };
-        m_sls->init_eval(false_eval);
-
-        lbool res = m_sls->operator()();
-        m_st.reset();
-        m_sls->collect_statistics(m_st);
-        report_tactic_progress("Number of flips:", m_sls->get_num_moves());
-        IF_VERBOSE(10, verbose_stream() << res << "\n");
-        IF_VERBOSE(10, m_sls->display(verbose_stream()));
-
-        if (res == l_true) {            
-            if (g->models_enabled()) {
-                model_ref mdl = m_sls->get_model();
-                mc = model2model_converter(mdl.get());
-                TRACE("sls_model", mc->display(tout););
-            }
-            g->reset();
-        }
-        else
-            mc = nullptr;
-
-    }
-
-    void operator()(goal_ref const& g,
-        goal_ref_buffer& result) override {
-        result.reset();
-
-        TRACE("sls", g->display(tout););
-        tactic_report report("sls", *g);
-
-        model_converter_ref mc;
-        run(g, mc);
-        g->add(mc.get());
-        g->inc_depth();
-        result.push_back(g.get());
-    }
-
-    void cleanup() override {
-
-        auto* d = alloc(bv::sls, m, m_params);
-        std::swap(d, m_sls);
-        dealloc(d);
-    }
-
-    void collect_statistics(statistics& st) const override {
-        st.copy(m_st);
-    }
-
-    void reset_statistics() override {
-        m_sls->reset_statistics();
-        m_st.reset();
-    }
-
-};
-
 static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
     return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
                     clean(alloc(sls_tactic, m, p)));
 }
 
-tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p) {
-    return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
-        clean(alloc(bv_sls_tactic, m, p)));
-}
-
-
 static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
 
     params_ref simp2_p = p;
@@ -268,10 +163,3 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
     return t;
 }
 
-tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p) {
-    params_ref q = p;
-    q.set_bool("elim_sign_ext", false);
-    tactic* t = and_then(mk_preamble(m, q), mk_bv_sls_tactic(m, q));
-    t->updt_params(q);
-    return t;
-}
diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h
index d58d310e3..867474319 100644
--- a/src/tactic/sls/sls_tactic.h
+++ b/src/tactic/sls/sls_tactic.h
@@ -24,16 +24,8 @@ class tactic;
 
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref());
 
-tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p = params_ref());
-
-tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p = params_ref());
-
 /*
   ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)")
 
-  ADD_TACTIC("qfbv-new-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_new_sls_tactic(m, p)")
-
-  ADD_TACTIC("qfbv-new-sls-core", "(try to) solve using stochastic local search for QF_BV.", "mk_bv_sls_tactic(m, p)")
-
 */