diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index 83e920042..1e5c9822c 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -121,24 +121,22 @@ namespace sls {
         return false;
     }
 
-    bool bv_eval::bval1_bv(app* e, bool use_current) const {
+    bool bv_eval::bval1_bv(app* e) const {
         SASSERT(m.is_bool(e));
         SASSERT(e->get_family_id() == bv.get_fid());
 
-        bool use_current1 = use_current || (e->get_num_args() > 0 && !m_lookahead.on_restore(e->get_arg(0)));
-        bool use_current2 = use_current || (e->get_num_args() > 1 && !m_lookahead.on_restore(e->get_arg(1)));
         auto ucompare = [&](std::function<bool(int)> const& f) {
             auto& a = wval(e->get_arg(0)); 
             auto& b = wval(e->get_arg(1)); 
-            return f(mpn.compare(a.tmp_bits(use_current1).data(), a.nw, b.tmp_bits(use_current2).data(), b.nw));
+            return f(mpn.compare(a.bits().data(), a.nw, b.bits().data(), b.nw));
         };
 
         // x <s y <=> x + 2^{bw-1} <u y + 2^{bw-1}
         auto scompare = [&](std::function<bool(int)> const& f) {
             auto& a = wval(e->get_arg(0));
             auto& b = wval(e->get_arg(1));
-            add_p2_1(a, use_current1, m_tmp);
-            add_p2_1(b, use_current2, m_tmp2);
+            add_p2_1(a, m_tmp);
+            add_p2_1(b, m_tmp2);
             return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw));
         };
 
@@ -146,7 +144,7 @@ namespace sls {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval(e->get_arg(0));
             auto const& b = wval(e->get_arg(1));
-            return a.set_mul(m_tmp2, a.tmp_bits(use_current1), b.tmp_bits(use_current2));
+            return a.set_mul(m_tmp2, a.bits(), b.bits());
         };
 
         switch (e->get_decl_kind()) {
@@ -171,7 +169,7 @@ namespace sls {
             unsigned idx;
             VERIFY(bv.is_bit2bool(e, child, idx));
             auto& a = wval(child);
-            return a.tmp_bits(use_current1).get(idx);
+            return a.bits().get(idx);
         }
         case OP_BUMUL_NO_OVFL: 
             return !umul_overflow();
@@ -181,7 +179,7 @@ namespace sls {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval(e->get_arg(0));
             auto const& b = wval(e->get_arg(1));
-            return a.set_add(m_tmp, a.tmp_bits(use_current1), b.tmp_bits(use_current1));
+            return a.set_add(m_tmp, a.bits(), b.bits());
         }
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:         
@@ -198,27 +196,81 @@ namespace sls {
         return false;
     }
 
+    void bv_eval::set_bool_value(expr* e, bool val) {
+        m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef);
+        m_tmp_bool_value_indices.push_back(e->get_id());
+    }
+
+    bool bv_eval::get_bool_value(expr* e) const {
+        auto val = m_tmp_bool_values.get(e->get_id(), l_undef);
+        if (val != l_undef)
+            return val == l_true;
+        auto v = ctx.atom2bool_var(e);
+        if (v != sat::null_bool_var)
+            return ctx.is_true(v);
+        auto b = bval1_bool(to_app(e));
+        m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef);
+        m_tmp_bool_value_indices.push_back(e->get_id());
+        return b;
+    }
+
+    void bv_eval::clear_bool_values() { 
+        for (auto i : m_tmp_bool_value_indices)
+            m_tmp_bool_values[i] = l_undef;
+        m_tmp_bool_value_indices.reset(); 
+    }
+
+    bool bv_eval::bval1_bool(app* e) const {
+        SASSERT(e->get_family_id() == basic_family_id);
+        switch (e->get_decl_kind()) {
+        case OP_AND: {
+            return all_of(*e, [&](expr* arg) { return get_bool_value(arg); });
+        case OP_OR:
+            return any_of(*e, [&](expr* arg) { return get_bool_value(arg); });
+        case OP_NOT:
+            return !get_bool_value(e->get_arg(0));
+        case OP_EQ:
+            if (m.is_iff(e))
+                return get_bool_value(e->get_arg(0)) == get_bool_value(e->get_arg(1));
+            return ctx.get_value(e->get_arg(0)) == ctx.get_value(e->get_arg(1));
+        case OP_IMPLIES:
+            return !get_bool_value(e->get_arg(0)) || get_bool_value(e->get_arg(1));
+        case OP_ITE:
+            return get_bool_value(e->get_arg(0)) ? get_bool_value(e->get_arg(1)) : get_bool_value(e->get_arg(2));
+        case OP_XOR: {
+            bool r = false;
+            for (expr* arg : *e)
+                r ^= get_bool_value(arg);
+            return r;
+        }
+        case OP_TRUE:
+            return true;
+        case OP_FALSE:
+            return false;
+        case OP_DISTINCT:
+            for (unsigned i = 0; i < e->get_num_args(); ++i)
+                for (unsigned j = i + 1; j < e->get_num_args(); ++j)
+                    if (ctx.get_value(e->get_arg(i)) == ctx.get_value(e->get_arg(j)))
+                        return false;
+            return true;
+        default:
+            UNREACHABLE();
+            break;
+        }
+        }
+        return false;
+    }
+
     bool bv_eval::bval1(app* e) const {
         if (e->get_family_id() == bv.get_fid())
-            return bval1_bv(e, true);
+            return bval1_bv(e);
         expr* x, * y;
         if (m.is_eq(e, x, y) && bv.is_bv(x)) {
             return wval(x).bits() == wval(y).bits();
         }
-        verbose_stream() << mk_bounded_pp(e, m) << "\n";
-        UNREACHABLE();
-        return false;
-    }
-
-    bool bv_eval::bval1_tmp(app* e) const {
-        if (e->get_family_id() == bv.get_fid())
-            return bval1_bv(e, false);
-        expr* x, * y;
-        if (m.is_eq(e, x, y) && bv.is_bv(x)) {
-            bool use_current1 = !m_lookahead.on_restore(x);
-            bool use_current2 = !m_lookahead.on_restore(y);
-            return wval(x).tmp_bits(use_current1) == wval(y).tmp_bits(use_current2);
-        }
+        if (e->get_family_id() == basic_family_id)
+            return bval1_bool(e);
+                   
         verbose_stream() << mk_bounded_pp(e, m) << "\n";
         UNREACHABLE();
         return false;
@@ -1296,9 +1348,9 @@ namespace sls {
         return r;
     }
 
-    void bv_eval::add_p2_1(bvval const& a, bool use_current, 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.tmp_bits(use_current), m_zero);
+        a.set_add(t, a.bits(), m_zero);
         m_zero.set(a.bw - 1, false);
         a.clear_overflow_bits(t);
     }
diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h
index aaf847472..b8d977ca8 100644
--- a/src/ast/sls/sls_bv_eval.h
+++ b/src/ast/sls/sls_bv_eval.h
@@ -54,6 +54,8 @@ namespace sls {
         bool_vector         m_is_fixed;
         unsigned            m_lookahead_steps = 0;
         unsigned            m_lookahead_phase_size = 10;
+        mutable svector<lbool>      m_tmp_bool_values;
+        mutable unsigned_vector     m_tmp_bool_value_indices;
         
 
         scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
@@ -73,8 +75,9 @@ namespace sls {
         void add_bit_vector(app* e);
         sls::bv_valuation* alloc_valuation(app* e);
 
-        bool bval1_bv(app* e, bool use_current) const;  
-        bool bval1_tmp(app* e) const;
+        bool bval1_bv(app* e) const;  
+        bool bval1_bool(app* e) const;
+
 
 
         void fold_oper(bvect& out, app* e, unsigned i, std::function<void(bvect&, bvval const&)> const& f);
@@ -124,7 +127,7 @@ namespace sls {
         bool try_repair_eq(bool is_true, bvval& a, bvval const& b);
         bool try_repair_eq(app* e, unsigned i);
         bool try_repair_int2bv(bvect const& e, expr* arg);
-        void add_p2_1(bvval const& a, bool use_current, bvect& t) const;
+        void add_p2_1(bvval const& a, bvect& t) const;
 
         bool add_overflow_on_fixed(bvval const& a, bvect const& t);
         bool mul_overflow_on_fixed(bvval const& a, bvect const& t);
@@ -184,6 +187,10 @@ namespace sls {
 
         bool bval0(expr* e) const { return ctx.is_true(e); }
         bool bval1(app* e) const;
+
+        void set_bool_value(expr* e, bool val);
+        void clear_bool_values();
+        bool get_bool_value(expr* e)const;
       
         /*
          * Try to invert value of child to repair value assignment of parent.
diff --git a/src/ast/sls/sls_bv_evaluator.h b/src/ast/sls/sls_bv_evaluator.h
index 13aff4a97..37502452d 100644
--- a/src/ast/sls/sls_bv_evaluator.h
+++ b/src/ast/sls/sls_bv_evaluator.h
@@ -633,16 +633,14 @@ public:
     void update_all() {
         unsigned max_depth = 0;
 
-        sls_tracker::entry_point_type::iterator start = m_tracker.get_entry_points().begin();
-        sls_tracker::entry_point_type::iterator end = m_tracker.get_entry_points().end();
-        for (sls_tracker::entry_point_type::iterator it = start; it != end; it++) {
-            expr * ep = m_tracker.get_entry_point(it->m_key);
+        for (auto const& [key, value] : m_tracker.get_entry_points()) {
+            expr* ep = m_tracker.get_entry_point(key);
             unsigned cur_depth = m_tracker.get_distance(ep);
-            if (m_traversal_stack.size() <= cur_depth) 
-                m_traversal_stack.resize(cur_depth+1);
+            m_traversal_stack.reserve(cur_depth + 1);
             m_traversal_stack[cur_depth].push_back(ep);
-            if (cur_depth > max_depth) max_depth = cur_depth;
+            max_depth = std::max(max_depth, cur_depth);
         }
+
         run_serious_update(max_depth);
     }
 
@@ -650,10 +648,8 @@ public:
         m_tracker.set_value(fd, new_value);
         expr * ep = m_tracker.get_entry_point(fd);
         unsigned cur_depth = m_tracker.get_distance(ep);
-        if (m_traversal_stack.size() <= cur_depth) 
-            m_traversal_stack.resize(cur_depth+1);
+        m_traversal_stack.reserve(cur_depth + 1);
         m_traversal_stack[cur_depth].push_back(ep);
-
         run_update(cur_depth);
     }
 
@@ -662,10 +658,8 @@ public:
         m_tracker.set_value(fd, new_value);
         expr * ep = m_tracker.get_entry_point(fd);
         unsigned cur_depth = m_tracker.get_distance(ep);
-        if (m_traversal_stack.size() <= cur_depth) 
-            m_traversal_stack.resize(cur_depth+1);
+        m_traversal_stack.reserve(cur_depth+1);
         m_traversal_stack[cur_depth].push_back(ep);
-
         run_serious_update(cur_depth);
     }
 
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index d65446ef7..8327aa010 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -76,9 +76,6 @@ namespace sls {
             if (apply_guided_move(vars))
                 continue;
 
-            if (false && apply_flip())
-                return;
-
             // bail out if no progress, and try random update
             if (apply_random_update(get_candidate_uninterp()))
                 recalibrate_weights();
@@ -108,6 +105,11 @@ namespace sls {
         if (vars.empty())
             return false;
         expr* e = vars[ctx.rand(vars.size())];
+        if (m.is_bool(e)) {
+            ctx.flip(ctx.atom2bool_var(e));
+            return true;
+        }
+        SASSERT(bv.is_bv(e));
         auto& v = wval(e);
         m_v_updated.set_bw(v.bw);
         v.get_variant(m_v_updated, m_ev.m_rand);
@@ -118,7 +120,14 @@ namespace sls {
     * random move: select a variable at random and use one of the moves: flip, add1, sub1
     */
     bool bv_lookahead::apply_random_move(ptr_vector<expr> const& vars) {
+        if (vars.empty())
+            return false;
         expr* e = vars[ctx.rand(vars.size())];
+        if (m.is_bool(e)) {
+            ctx.flip(ctx.atom2bool_var(e));
+            return true;
+        }
+        SASSERT(bv.is_bv(e));
         auto& v = wval(e);
         m_v_updated.set_bw(v.bw);
         v.bits().copy_to(v.nw, m_v_updated);
@@ -139,17 +148,6 @@ namespace sls {
         return apply_update(e, m_v_updated, "random move");
     }
 
-    bool bv_lookahead::apply_flip() {
-        if (!m_last_atom)
-            return false;
-        auto const& cond = m_ev.terms.condition_occurs(m_last_atom);
-        if (cond.empty())
-            return false;         
-        expr* e = cond[ctx.rand(cond.size())];
-        ctx.flip(ctx.atom2bool_var(e));
-        return true;        
-    }
-
     /**
     * Retrieve a candidate top-level predicate that is false, give preference to
     * those with high score, but back off if they are frequently chosen.
@@ -187,8 +185,6 @@ namespace sls {
         if (!e)
             return m_empty_vars;
 
-
-
         auto const& vars = m_ev.terms.uninterp_occurs(e);
 
         TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
@@ -256,7 +252,7 @@ namespace sls {
         if (!is_bv_literal(lit))
             return false;
         app* a = to_app(ctx.atom(lit.var()));
-        return (m_ev.bval0(a) != m_ev.bval1(a));
+        return m_ev.bval0(a) != m_ev.bval1(a);
     }
 
    
@@ -285,7 +281,7 @@ namespace sls {
     * for inequalities.
     */
     double bv_lookahead::new_score(app* a) {
-        bool is_true = ctx.is_true(a);
+        bool is_true = m_ev.get_bool_value(a);
         bool is_true_new = m_ev.bval1(a);
         if (is_true == is_true_new)
             return 1;
@@ -366,6 +362,11 @@ namespace sls {
         return 0;
     }
 
+    double bv_lookahead::lookahead_flip(sat::bool_var v) {
+        auto a = ctx.atom(v);
+        return -1000;
+    }
+
     /**
     * Rehearse an update. The update is revered while a score is computed and returned.
     * Walk all parents, until hitting predicates where their scores are computed.
@@ -386,28 +387,26 @@ namespace sls {
         for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
             for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
                 auto a = m_update_stack[depth][i];
-                if (bv.is_bv(a)) {
-                    if (a != t) {
-                        m_ev.eval(a);
-                        insert_update(a);
-                    }
-                    for (auto p : ctx.parents(a)) {
-                        insert_update_stack(p);
-                        max_depth = std::max(max_depth, get_depth(p));
-                    }
+                TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " " << depth << " " << i << "\n";);
+                for (auto p : ctx.parents(a)) {
+                    insert_update_stack(p);
+                    max_depth = std::max(max_depth, get_depth(p));
                 }
-                else if (is_root(a)) 
+                if (is_root(a)) 
                     score += get_weight(a) * (new_score(a) - old_score(a));                
-                else if (m.is_bool(a))
+
+                if (a == t)
                     continue;
-                else {
-                    IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n");
-                }
+                else if (bv.is_bv(a)) 
+                    m_ev.eval(a);
+
+                insert_update(a);
             }
             m_update_stack[depth].reset();
         }
         m_in_update_stack.reset();
         restore_lookahead();
+        m_ev.clear_bool_values();
 
         TRACE("sls_verbose", tout << mk_bounded_pp(t, m) << " := " << new_value << " score: " << m_top_score << "\n");
 
@@ -418,7 +417,7 @@ namespace sls {
         if (!wval(u).can_set(new_value))
             return;
         auto score = lookahead_update(u, new_value);
-        ++m_stats.m_num_updates;
+        ++m_stats.m_num_lookaheads;
         //verbose_stream() << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << "\n";
         if (score > m_best_score) {
             m_best_score = score;
@@ -428,7 +427,24 @@ namespace sls {
         }
     }
 
+    void bv_lookahead::try_flip(expr* u) {
+        auto v = ctx.atom2bool_var(u);
+        if (v == sat::null_bool_var)
+            return;
+        auto score = lookahead_flip(v);
+        verbose_stream() << "lookahead flip " << mk_bounded_pp(u, m) << " score: " << score << "\n";
+        ++m_stats.m_num_lookaheads;
+        if (score > m_best_score) {
+            m_best_score = score;
+            m_best_expr = u;
+        }
+    }
+
     void bv_lookahead::add_updates(expr* u) {
+        if (m.is_bool(u)) {
+            try_flip(u);
+            return;
+        }
         SASSERT(bv.is_bv(u));
         auto& v = wval(u);
         while (m_v_saved.size() < v.bits().size()) {
@@ -483,41 +499,51 @@ namespace sls {
     bool bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) {
         if (!e || !wval(e).can_set(new_value))
             return false;
-        SASSERT(bv.is_bv(e));
+
         SASSERT(is_uninterp(e));
         SASSERT(m_restore.empty());
+        SASSERT(bv.is_bv(e));
 
         wval(e).eval = new_value;
         double old_top_score = m_top_score;
-
         VERIFY(wval(e).commit_eval_check_tabu());
+
         insert_update_stack(e);
         unsigned max_depth = get_depth(e);
         for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
             for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
                 auto e = m_update_stack[depth][i];
-                if (bv.is_bv(e)) {
-                    m_ev.eval(e); // updates wval(e).eval
-                    wval(e).commit_eval_ignore_tabu();
-                    for (auto p : ctx.parents(e)) {
-                        insert_update_stack(p);
-                        max_depth = std::max(max_depth, get_depth(p));
-                    }
-                }
-                else if (is_root(e)) {
+                TRACE("bv", tout << "update " << mk_bounded_pp(e, m) << "\n";);
+                if (is_root(e)) {
                     double score = new_score(e);
                     m_top_score += get_weight(e) * (score - old_score(e));
                     set_score(e, score);
                 }
-                else if (m.is_bool(e))
-                    continue;
-                else {
-                    UNREACHABLE();
+
+                if (bv.is_bv(e)) {
+                    m_ev.eval(e); // updates wval(e).eval
+                    wval(e).commit_eval_ignore_tabu();
                 }
+                else if (m.is_bool(e)) {
+                    auto v0 = m_ev.get_bool_value(to_app(e));
+                    auto v1 = m_ev.bval1(to_app(e));
+                    if (v0 == v1)
+                        continue;
+                    m_ev.set_bool_value(to_app(e), v1);
+                    auto v = ctx.atom2bool_var(e);
+                    if (v != sat::null_bool_var)
+                        ctx.flip(v);
+                }
+                for (auto p : ctx.parents(e)) {
+                    insert_update_stack(p);
+                    max_depth = std::max(max_depth, get_depth(p));
+                }                
+                VERIFY(m.is_bool(e) || bv.is_bv(e));
             }
             m_update_stack[depth].reset();
         }
         m_in_update_stack.reset();
+        m_ev.clear_bool_values();
         TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m)
             << " := " << new_value
             << " score " << m_top_score << "\n";);
@@ -525,12 +551,20 @@ namespace sls {
     }
 
     void bv_lookahead::insert_update(expr* e) {
-        auto& v = wval(e);
-        m_restore.push_back(e);
-        m_on_restore.mark(e);
-        TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << " " << v << "\n");
-        v.save_value();
-        v.commit_eval_ignore_tabu();
+
+        TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n");
+        if (bv.is_bv(e)) {
+            auto& v = wval(e);
+            v.save_value();
+            v.commit_eval_ignore_tabu();
+            SASSERT(!m_restore.contains(e));
+            m_restore.push_back(e);
+        }
+        else if (m.is_bool(e)) {
+            auto v1 = m_ev.bval1(to_app(e));
+            m_ev.set_bool_value(to_app(e), v1);
+        }
+
     }
 
     void bv_lookahead::insert_update_stack(expr* e) {
@@ -545,20 +579,15 @@ namespace sls {
     void bv_lookahead::restore_lookahead() {
         for (auto e : m_restore) {
             wval(e).restore_value();
-            TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
+            TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");            
         }
         m_restore.reset();
-        m_on_restore.reset();
     }
 
     sls::bv_valuation& bv_lookahead::wval(expr* e) const {
         return m_ev.wval(e);
     }
 
-    bool bv_lookahead::on_restore(expr* e) const {
-        return m_on_restore.is_marked(e);
-    }
-
     bv_lookahead::bool_info& bv_lookahead::get_bool_info(expr* e) {
         return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0, 1});
     }
@@ -630,8 +659,7 @@ namespace sls {
     }
 
     void bv_lookahead::collect_statistics(statistics& st) const {
-        st.update("sls-bv-lookahead", m_stats.m_num_lookahead);
-        st.update("sls-bv-updates", m_stats.m_num_updates);
+        st.update("sls-bv-lookaheads", m_stats.m_num_lookaheads);
         st.update("sls-bv-moves", m_stats.m_moves);
         st.update("sls-bv-restarts", m_stats.m_restarts);
     }
diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
index 05f5501a5..9edb1bcdf 100644
--- a/src/ast/sls/sls_bv_lookahead.h
+++ b/src/ast/sls/sls_bv_lookahead.h
@@ -48,8 +48,7 @@ namespace sls {
         };
 
         struct stats {
-            unsigned m_num_lookahead = 0;
-            unsigned m_num_updates = 0;
+            unsigned m_num_lookaheads = 0;
             unsigned m_moves = 0;
             unsigned m_restarts = 0;
             unsigned m_num_propagations = 0;
@@ -70,7 +69,7 @@ namespace sls {
         bvect m_v_saved, m_v_updated;
         ptr_vector<expr> m_restore;
         vector<ptr_vector<app>> m_update_stack;
-        expr_mark m_on_restore, m_in_update_stack;
+        expr_mark m_in_update_stack;
         double m_best_score = 0, m_top_score = 0;
         bvect m_best_value;
         expr* m_best_expr = nullptr;
@@ -94,6 +93,8 @@ namespace sls {
         void   set_score(app* c, double d) { get_bool_info(c).score = d; }
         double new_score(app* c);
 
+        double lookahead_flip(sat::bool_var v);
+
         void rescore();
 
         unsigned get_weight(expr* e) { return get_bool_info(e).weight; }
@@ -108,12 +109,12 @@ namespace sls {
         void inc_touched(app* e) { ++get_bool_info(e).touched; }
 
         void try_set(expr* u, bvect const& new_value);
+        void try_flip(expr* u);
         void add_updates(expr* u);
         bool apply_update(expr* e, bvect const& new_value, char const* reason);
         bool apply_random_move(ptr_vector<expr> const& vars);
         bool apply_guided_move(ptr_vector<expr> const& vars);
         bool apply_random_update(ptr_vector<expr> const& vars);
-        bool apply_flip();
         ptr_vector<expr> const& get_candidate_uninterp();
 
         void check_restart();
@@ -123,8 +124,6 @@ namespace sls {
 
         void search();
 
-
-
     public:
         bv_lookahead(bv_eval& ev);
 
@@ -132,8 +131,6 @@ namespace sls {
 
         void start_propagation();
 
-        bool on_restore(expr* e) const;
-
         void collect_statistics(statistics& st) const;
 
     };
diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp
index 08f1d3040..0621850c6 100644
--- a/src/ast/sls/sls_bv_terms.cpp
+++ b/src/ast/sls/sls_bv_terms.cpp
@@ -134,23 +134,12 @@ namespace sls {
         return m_uninterp_occurs[id];
     }
 
-    ptr_vector<expr> const& bv_terms::condition_occurs(expr* e) {
-        unsigned id = e->get_id();
-        m_condition_occurs.reserve(id + 1);
-        if (!m_condition_occurs[id].empty())
-            return m_condition_occurs[id];
-        register_uninterp(e);
-        return m_condition_occurs[id];
-    }
-
     void bv_terms::register_uninterp(expr* e) {
         if (!is_bv_predicate(e))
             return;
         m_uninterp_occurs.reserve(e->get_id() + 1);
-        m_condition_occurs.reserve(e->get_id() + 1);
         auto& occs = m_uninterp_occurs[e->get_id()];
-        auto& cond_occs = m_condition_occurs[e->get_id()];
-        ptr_vector<expr> todo, cond_todo;
+        ptr_vector<expr> todo;
         todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
         expr_mark marked;
         expr* c, * th, * el;
@@ -159,9 +148,7 @@ namespace sls {
             if (marked.is_marked(e))
                 continue;
             marked.mark(e);
-            if (is_bv_predicate(e))
-                cond_occs.push_back(e);
-            else if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid()) {
+            if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid()) {
                 for (expr* arg : *to_app(e))
                     todo.push_back(arg);
             }
@@ -170,14 +157,14 @@ namespace sls {
                     todo.push_back(arg);
             }
             else if (m.is_ite(e, c, th, el)) {
-                cond_occs.push_back(c);
+                todo.push_back(c);
                 if (ctx.is_true(c))
                     todo.push_back(th);
                 else
                     todo.push_back(el);
             }
-            else if (bv.is_bv(e))
-                occs.push_back(e);
+            else if (is_uninterp(e) && (m.is_bool(e) || bv.is_bv(e))) 
+                occs.push_back(e);            
         }
     }
 }
diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h
index a69020b61..5dbf8d72f 100644
--- a/src/ast/sls/sls_bv_terms.h
+++ b/src/ast/sls/sls_bv_terms.h
@@ -34,7 +34,6 @@ namespace sls {
         bv_util             bv;
         expr_ref_vector     m_axioms;
         vector<ptr_vector<expr>> m_uninterp_occurs;
-        vector<ptr_vector<expr>> m_condition_occurs;
 
         expr_ref ensure_binary(expr* e);
 
@@ -54,9 +53,5 @@ namespace sls {
         expr_ref_vector& axioms() { return m_axioms; }
 
         ptr_vector<expr> const& uninterp_occurs(expr* e);
-
-        ptr_vector<expr> const& condition_occurs(expr* e);
-
-
     };
 }
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 5cdb0934c..74b2eccb8 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -284,7 +284,12 @@ namespace sls {
         auto fid = s->get_family_id();
         auto p = m_plugins.get(fid, nullptr);
         if (p) 
-            return p->get_value(e);      
+            return p->get_value(e);  
+        if (m.is_bool(e)) {
+            sat::bool_var v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
+            if (v != sat::null_bool_var)
+                return expr_ref(m.mk_bool_val(is_true(v)), m);
+        }
         verbose_stream() << fid << " " << m.get_family_name(fid) << " " << mk_pp(e, m) << "\n";
         UNREACHABLE();
         return expr_ref(e, m);