diff --git a/src/ast/sls/sls_bv_engine.cpp b/src/ast/sls/sls_bv_engine.cpp
index f9d1da552..8d009b500 100644
--- a/src/ast/sls/sls_bv_engine.cpp
+++ b/src/ast/sls/sls_bv_engine.cpp
@@ -96,7 +96,6 @@ double sls_engine::top_score() {
     for (expr* e : m_assertions) {
         top_sum += m_tracker.get_score(e);
     }
-
     TRACE("sls_top", tout << "Score distribution:";
           for (expr* e : m_assertions) 
               tout << " " << m_tracker.get_score(e);
@@ -466,7 +465,6 @@ lbool sls_engine::search() {
 
         // randomize if no increasing move was found
         if (new_const == static_cast<unsigned>(-1)) {
-            score = old_score;
             if (m_walksat_repick)
                 m_evaluator.randomize_local(m_assertions);
             else
@@ -481,16 +479,16 @@ lbool sls_engine::search() {
                     // smooth weights with probability sp / 1024
                     if (m_tracker.get_random_uint(10) < m_paws_sp)
                     {
-                        if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
+                        if (m_mpz_manager.eq(m_tracker.get_value(q), m_one))
                             m_tracker.decrease_weight(q);
                     }
                     // increase weights otherwise
                     else
                     {
-                        if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
+                        if (m_mpz_manager.eq(m_tracker.get_value(q), m_zero))
                             m_tracker.increase_weight(q);
                     }
-                }
+                }                  
             }
         }
         // otherwise, apply most increasing move
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index 3439c7637..96e9e1579 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -27,9 +27,7 @@ namespace sls {
         ctx(ctx)
     {}
 
-    void bv_fixed::init() {
-
-        return;
+    void bv_fixed::init() {  
 
         for (auto e : ctx.subterms())
             set_fixed(e);
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 46f52ec33..13e0146e6 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -33,11 +33,12 @@ namespace sls {
         m(ev.m) {
     }
 
-    void bv_lookahead::init_updates() {
-        m_best_expr = nullptr;
+    void bv_lookahead::start_propagation() {
+        if (m_stats.m_num_propagations++ % m_config.propagation_base == 0) 
+            search();        
     }
 
-    lbool bv_lookahead::search() {
+    void bv_lookahead::search() {
         updt_params(ctx.get_params());
         rescore();
         m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
@@ -50,92 +51,181 @@ namespace sls {
             auto& vars = get_candidate_uninterp();
 
             if (vars.empty())
-                return l_true;
+                return;
 
-            // random walk with probability 1000/wp 
-            if (ctx.rand(10) < m_config.wp && apply_random_update(vars))
+            // random walk with probability 1024/wp 
+            if (ctx.rand(2047) < m_config.wp && apply_random_move(vars))
                 continue;
 
-            if (apply_guided_update(vars))
+            if (apply_guided_move(vars))
                 continue;
 
-            apply_random_update(vars);
-            recalibrate_weights();
+            if (apply_random_update(get_candidate_uninterp()))
+                recalibrate_weights();
         }
         m_config.max_moves_base += 100;
-        return l_undef;
     }
 
-    bool bv_lookahead::apply_guided_update(ptr_vector<expr> const& vars) {
-        init_updates();
-        double old_top_score = m_top_score;
-        for (auto u : vars)
-            add_updates(u);
-        m_top_score = old_top_score;
-        return apply_update();
+    bool bv_lookahead::apply_guided_move(ptr_vector<expr> const& vars) {
+        m_best_expr = nullptr;
+        m_best_score = m_top_score;
+        unsigned sz = vars.size();
+        unsigned start = ctx.rand(sz);
+        for (unsigned i = 0; i < sz; ++i)
+            add_updates(vars[(start + i) % sz]);
+        TRACE("bv", tout << "guided update " << m_best_score << " " << (m_best_expr?"no update":"") << "\n";);
+        if (!m_best_expr)
+            return false;
+
+        apply_update(m_best_expr, m_best_value);
+        //verbose_stream() << "increasing move " << mk_bounded_pp(m_best_expr, m) 
+        //    << " := " << m_best_value << " score: " << m_top_score << "\n";
+        return true;
     }
 
     ptr_vector<expr> const& bv_lookahead::get_candidate_uninterp() {
         auto const& lits = ctx.root_literals();
-        unsigned start = ctx.rand(lits.size());
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            auto lit = lits[(i + start) % lits.size()];
-            auto e = ctx.atom(lit.var());
-            if (!e || !is_app(e))
-                continue;
-            app* a = to_app(e);
-            if (!m_ev.can_eval1(a))
-                continue;
-            if (m_ev.bval0(a) == m_ev.bval1(a))
-                continue;
-            auto const& vars = m_ev.terms.uninterp_occurs(a);
-            VERIFY(!vars.empty());
-            TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
-                        for (auto e : vars) tout << mk_bounded_pp(e, m) << " ";
-                        tout << "\n";);
-            return vars;
+        app* e = nullptr;
+        if (m_config.ucb) {
+            double max = -1.0;
+            for (auto lit : ctx.root_literals()) {
+                if (!is_false_bv_literal(lit))
+                    continue;
+                auto a = to_app(ctx.atom(lit.var()));
+                auto score = old_score(a);
+                auto q = score 
+                    + m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a)) 
+                    + m_config.ucb_noise * ctx.rand(512);
+                if (q > max)
+                    max = q, e = a;
+            }
+            if (e) {
+                m_touched++;
+                inc_touched(e);
+            }
         }
-        return m_empty_vars;
+        else {
+            unsigned n = 0;
+            for (auto lit : ctx.root_literals())
+                if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0)
+                    e = to_app(ctx.atom(lit.var()));
+        }
+        if (!e)
+            return m_empty_vars;
+
+        auto const& vars = m_ev.terms.uninterp_occurs(e);
+        VERIFY(!vars.empty());
+        TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
+        for (auto e : vars) tout << mk_bounded_pp(e, m) << " ";
+        tout << "\n";);
+        return vars;
     }
 
+    bool bv_lookahead::apply_random_update(ptr_vector<expr> const& vars) {  
+        expr* e = vars[ctx.rand(vars.size())];
+        auto& v = wval(e);
+        m_v_updated.set_bw(v.bw);
+        v.get_variant(m_v_updated, m_ev.m_rand);
+        if (!v.can_set(m_v_updated))
+            return false;
+        apply_update(e, m_v_updated);
 
-    bool bv_lookahead::apply_random_update(ptr_vector<expr> const& vars) {
-        while (true) {
-            expr* e = vars[ctx.rand(vars.size())];
-            auto& v = wval(e);
-            m_v_updated.set_bw(v.bw);
-            v.get_variant(m_v_updated, m_ev.m_rand);
-            v.eval = m_v_updated;
-            if (!v.commit_eval())
-                continue;
-            apply_update(e, m_v_updated);
+        //verbose_stream() << "random update " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n";
+        return true;
+    }
+
+    bool bv_lookahead::apply_random_move(ptr_vector<expr> const& vars) {
+        expr* e = vars[ctx.rand(vars.size())];
+        auto& v = wval(e);
+        m_v_updated.set_bw(v.bw);
+        v.bits().copy_to(v.nw, m_v_updated);
+        switch (ctx.rand(3)) {
+        case 0: {
+            // flip a random bit
+            auto bit = ctx.rand(v.bw);
+            m_v_updated.set(bit, !m_v_updated.get(bit));
             break;
         }
+        case 1:
+            v.add1(m_v_updated);
+            break;
+        default:
+            v.sub1(m_v_updated);
+            break;
+        }
+
+        if (!v.can_set(m_v_updated))
+            return false;
+        apply_update(e, m_v_updated);
+        TRACE("bv", tout << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << "\n";);
+        // verbose_stream() << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n";
         return true;
     }
 
     void bv_lookahead::check_restart() {
-
-        if (m_stats.m_moves % m_config.restart_base == 0)
-            // ucb_forget();
+        
+        if (m_stats.m_moves % m_config.restart_base == 0) {
+            ucb_forget();
             rescore();
+        }
 
         if (m_stats.m_moves < m_config.restart_next)
             return;
 
-        if (m_stats.m_restarts & 1)
+        ++m_stats.m_restarts;
+
+        if (0x1 == (m_stats.m_restarts & 0x1))
             m_config.restart_next += m_config.restart_base;
         else
             m_config.restart_next += (2 << (m_stats.m_restarts >> 1)) * m_config.restart_base;
 
-        m_stats.m_restarts++;
-
-        // TODO: reset values of uninterpreted to 0        
+        reset_uninterp_in_false_literals(); 
+        rescore();
     }
 
+    void bv_lookahead::reset_uninterp_in_false_literals() {
+        auto const& lits = ctx.root_literals();
+        expr_mark marked;
+        for (auto lit : ctx.root_literals()) {
+            if (!is_false_bv_literal(lit))
+                continue;
+            app* a = to_app(ctx.atom(lit.var()));
+            auto const& occs = m_ev.terms.uninterp_occurs(a);
+            for (auto e : occs) {
+                if (marked.is_marked(e))
+                    continue;
+                marked.mark(e);
+                auto& v = wval(e);
+                m_v_updated.set_bw(v.bw);
+                m_v_updated.set_zero();
+                if (v.can_set(m_v_updated)) {
+                    apply_update(e, m_v_updated);
+                }
+            }
+        }
+    }
+
+    bool bv_lookahead::is_bv_literal(sat::literal lit) {
+        if (!ctx.is_true(lit))
+            return false;
+        auto e = ctx.atom(lit.var());
+        if (!e || !is_app(e))
+            return false;
+        app* a = to_app(e);
+        return m_ev.can_eval1(a);
+    }
+
+    bool bv_lookahead::is_false_bv_literal(sat::literal lit) {
+        if (!is_bv_literal(lit))
+            return false;
+        app* a = to_app(ctx.atom(lit.var()));
+        return (m_ev.bval0(a) != m_ev.bval1(a));
+    }
+
+   
     void bv_lookahead::updt_params(params_ref const& _p) {
         sls_params p(_p);
-        //m_config.max_restarts = p.max_restarts();
+
         m_config.walksat = p.walksat();
         m_config.walksat_repick = p.walksat_repick();
         m_config.paws_sp = p.paws_sp();
@@ -145,6 +235,12 @@ namespace sls {
         m_config.restart_next = m_config.restart_base;
         m_config.restart_init = p.restart_init();
         m_config.early_prune = p.early_prune();
+        m_config.ucb = p.walksat_ucb();
+
+        m_config.ucb_constant = p.walksat_ucb_constant();
+        m_config.ucb_forget = p.walksat_ucb_forget();
+        m_config.ucb_init = p.walksat_ucb_init();
+        m_config.ucb_noise = p.walksat_ucb_noise();
     }
 
     double bv_lookahead::new_score(app* a) {
@@ -163,7 +259,9 @@ namespace sls {
             for (unsigned i = 0; i < vx.bw; ++i)
                 if (vx.bits().get(i) != vy.bits().get(i))
                     ++delta;
-            return 1 - (delta / vx.bw);
+            auto d = 1.0 - (delta / (double)vx.bw);
+            //verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n";
+            return d;
         }
         else if (bv.is_ule(a, x, y)) {
             auto const& vx = wval(x);
@@ -229,12 +327,13 @@ namespace sls {
         return 0;
     }
 
-    double bv_lookahead::lookahead(expr* e, bvect const& new_value) {
+    double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) {
         SASSERT(bv.is_bv(e));
         SASSERT(is_uninterp(e));
         SASSERT(m_restore.empty());
 
         bool has_tabu = false;
+        double score = m_top_score;
 
         wval(e).eval = new_value;
         if (!insert_update(e)) {
@@ -254,11 +353,14 @@ namespace sls {
                             max_depth = std::max(max_depth, get_depth(p));
                         }
                     }
-                    else
+                    else {
+                        IF_VERBOSE(1, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << "\n");
                         has_tabu = true;
+                    }
+                }
+                else if (is_root(a)) {
+                     score += get_weight(a) * (new_score(a) - old_score(a));
                 }
-                else if (is_root(a))
-                    rescore(a);
                 else if (m.is_bool(a))
                     continue;
                 else {
@@ -275,17 +377,15 @@ namespace sls {
 
         if (has_tabu)
             return -10000;
-        if (m_top_score <= 0.000001)
-            return -10000;
-        return m_top_score;
+        return score;
     }
 
     void bv_lookahead::try_set(expr* u, bvect const& new_value) {
         if (!wval(u).can_set(new_value))
             return;
-        auto score = lookahead(u, new_value);
+        auto score = lookahead_update(u, new_value);
         ++m_stats.m_num_updates;
-        verbose_stream() << mk_bounded_pp(u, m) << " " << new_value << " score: " << score << "\n";
+        //verbose_stream() << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << "\n";
         if (score > m_best_score) {
             m_best_score = score;
             m_best_expr = u;
@@ -323,12 +423,6 @@ namespace sls {
         if (v.bw <= 1)
             return;
 
-        // invert
-        for (unsigned i = 0; i < v.nw; ++i)
-            m_v_updated[i] = ~m_v_updated[i];
-        v.clear_overflow_bits(m_v_updated);
-        try_set(u, m_v_updated);
-
         // increment
         m_v_saved.copy_to(v.nw, m_v_updated);
         v.add1(m_v_updated);
@@ -339,16 +433,12 @@ namespace sls {
         v.sub1(m_v_updated);
         try_set(u, m_v_updated);
 
-        // reset to original value
-        try_set(u, m_v_saved);
-    }
-
-    bool bv_lookahead::apply_update() {
-        CTRACE("bv", !m_best_expr, tout << "no update\n");
-        if (!m_best_expr)
-            return false;
-        apply_update(m_best_expr, m_best_value);
-        return true;       
+        // invert
+        m_v_saved.copy_to(v.nw, m_v_updated);
+        for (unsigned i = 0; i < v.nw; ++i)
+            m_v_updated[i] = ~m_v_updated[i];
+        v.clear_overflow_bits(m_v_updated);
+        try_set(u, m_v_updated);
     }
 
     void bv_lookahead::apply_update(expr* e, bvect const& new_value) {
@@ -357,6 +447,7 @@ namespace sls {
         SASSERT(is_uninterp(e));
         SASSERT(m_restore.empty());
         wval(e).eval = new_value;
+        double old_top_score = m_top_score;
 
         //verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n";
 
@@ -370,6 +461,7 @@ namespace sls {
                     m_ev.eval(e); // updates wval(e).eval
                     if (!wval(e).commit_eval()) {
                         TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
+                        IF_VERBOSE(0, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
                         // bv_plugin::is_sat picks up discrepancies
                         continue;
                     }
@@ -379,7 +471,9 @@ namespace sls {
                     }
                 }
                 else if (is_root(e)) {
-                    rescore(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;
@@ -390,6 +484,8 @@ namespace sls {
             m_update_stack[depth].reset();
         }
         m_in_update_stack.reset();
+        TRACE("bv", tout << mk_bounded_pp(e, m) << " := " 
+            << new_value << " " << m_top_score << " (" << old_top_score << ")\n");
     }
 
     bool bv_lookahead::insert_update(expr* e) {
@@ -427,77 +523,79 @@ namespace sls {
         return m_on_restore.is_marked(e);
     }
 
-    unsigned bv_lookahead::get_weight(expr* e) {
-        return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight;
-    }
-
-    void bv_lookahead::inc_weight(expr* e) {
-        m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight += 1;
+    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});
     }
 
     void bv_lookahead::dec_weight(expr* e) {
-        auto& w = m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0 }).weight;
+        auto& w = get_bool_info(e).weight;
         w = w > m_config.paws_init ? w - 1 : m_config.paws_init;
     }
 
-    void bv_lookahead::set_score(app* a, double d) {
-        m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score = d;
-    }
-
-    double bv_lookahead::old_score(app* a) {
-        return m_bool_info.insert_if_not_there(a, { m_config.paws_init, 0 }).score;
-    }
-
     void bv_lookahead::rescore() {
         m_top_score = 0;
-        m_rescore = false;
         m_is_root.reset();
         for (auto lit : ctx.root_literals()) {
-            auto e = ctx.atom(lit.var());
-            if (!e || !is_app(e))
+            if (!is_bv_literal(lit))
                 continue;
-            app* a = to_app(e);
-            if (!m_ev.can_eval1(a))
-                continue;
-
+            auto a = to_app(ctx.atom(lit.var()));
             double score = new_score(a);
             set_score(a, score);
             m_top_score += score;
             m_is_root.mark(a);
         }
-        verbose_stream() << "top score " << m_top_score << "\n";
-
-    }
-
-    void bv_lookahead::rescore(app* e) {
-        double score = new_score(e);
-        m_top_score += get_weight(e) * (score - old_score(e));
-        set_score(e, score);
     }
 
     void bv_lookahead::recalibrate_weights() {
         for (auto lit : ctx.root_literals()) {
-            auto e = ctx.atom(lit.var());
-            if (!e || !is_app(e))
+            if (!is_bv_literal(lit))
                 continue;
-            app* a = to_app(e);
-            if (!m_ev.can_eval1(a))
-                continue;
-            bool is_true = ctx.is_true(lit);
-            bool is_true_a = m_ev.bval1(a);
-            if (ctx.rand(10) < m_config.paws_sp) {
-                if (is_true == is_true_a)
+            auto a = to_app(ctx.atom(lit.var()));
+            bool is_true0 = m_ev.bval0(a);
+            bool is_true1 = m_ev.bval1(a);
+            if (ctx.rand(2047) < m_config.paws_sp) {
+                if (is_true0 == is_true1)
                     dec_weight(a);
             }
-            else if (is_true != is_true_a)
+            else if (is_true0 != is_true1)
                 inc_weight(a);
         }
-        m_best_score = 0;
+
+        IF_VERBOSE(20, display_weights(verbose_stream()));       
+    }
+
+    std::ostream& bv_lookahead::display_weights(std::ostream& out) {
+
+        for (auto lit : ctx.root_literals()) {
+            if (!is_bv_literal(lit))
+                continue;
+            auto a = to_app(ctx.atom(lit.var()));
+            out
+                << get_weight(a) << " "
+                << mk_bounded_pp(a, m) << " "
+                << old_score(a) << "\n";
+        }
+        return out;
+    }
+
+    void bv_lookahead::ucb_forget() {
+        if (m_config.ucb_forget >= 1.0)
+            return;
+        for (auto lit : ctx.root_literals()) {
+            if (!is_bv_literal(lit))
+                continue;
+            auto a = to_app(ctx.atom(lit.var()));
+            auto touched_old = get_touched(a);
+            auto touched_new = static_cast<unsigned>((touched_old - 1) * m_config.ucb_forget + 1);
+            set_touched(a, touched_new);
+            m_touched += touched_new - touched_old;
+        }
     }
 
     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-moves", m_stats.m_moves);
+        st.update("sls-bv-restarts", m_stats.m_restarts);
     }
 }
\ No newline at end of file
diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
index 2b3aed8d4..bc34800e4 100644
--- a/src/ast/sls/sls_bv_lookahead.h
+++ b/src/ast/sls/sls_bv_lookahead.h
@@ -38,7 +38,13 @@ namespace sls {
             unsigned restart_init = 1000;
             bool early_prune = true;
             unsigned max_moves = 0;
-            unsigned max_moves_base = 200;
+            unsigned max_moves_base = 800;
+            unsigned propagation_base = 10000;
+            bool ucb = true;
+            double ucb_constant = 1.0;
+            double ucb_forget = 0.1;
+            bool ucb_init = false;
+            double ucb_noise = 0.1;
         };
 
         struct stats {
@@ -46,11 +52,13 @@ namespace sls {
             unsigned m_num_updates = 0;
             unsigned m_moves = 0;
             unsigned m_restarts = 0;
+            unsigned m_num_propagations = 0;
         };
 
         struct bool_info {
-            unsigned weight = 0;
+            unsigned weight = 40;
             double score = 0;
+            unsigned touched = 1;
         };
 
         bv_util bv;
@@ -66,51 +74,61 @@ namespace sls {
         double m_best_score = 0, m_top_score = 0;
         bvect m_best_value;
         expr* m_best_expr = nullptr;
-        bool  m_rescore = true;
         ptr_vector<expr> m_empty_vars;
         obj_map<expr, bool_info> m_bool_info;
         expr_mark m_is_root;
+        unsigned m_touched = 1;
 
-        void init_updates();
+        std::ostream& display_weights(std::ostream& out);
 
         bv_valuation& wval(expr* e) const;
 
         void insert_update_stack(expr* e);
         bool insert_update(expr* e);        
         void restore_lookahead();
-        double lookahead(expr* u, bvect const& new_value);
-        double old_score(app* c);
+
+        bool_info& get_bool_info(expr* e);
+        double lookahead_update(expr* u, bvect const& new_value);
+        double old_score(app* c) { return get_bool_info(c).score; }
+        void   set_score(app* c, double d) { get_bool_info(c).score = d; }
         double new_score(app* c);
-        void   set_score(app* c, double d);
-        void   rescore(app* c);
 
         void rescore();
 
-
-        unsigned get_weight(expr* e);
-        void     inc_weight(expr* e);
+        unsigned get_weight(expr* e) { return get_bool_info(e).weight; }
+        void     inc_weight(expr* e) { ++get_bool_info(e).weight; }
         void     dec_weight(expr* e);
         void     recalibrate_weights();
         bool     is_root(expr* e) { return m_is_root.is_marked(e); }
 
+        void ucb_forget();
+        unsigned get_touched(app* e) { return get_bool_info(e).touched; }
+        void set_touched(app* e, unsigned t) { get_bool_info(e).touched = t; }
+        void inc_touched(app* e) { ++get_bool_info(e).touched; }
+
         void try_set(expr* u, bvect const& new_value);
         void add_updates(expr* u);
         void apply_update(expr* e, bvect const& new_value);
-        bool apply_update();
+        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_guided_update(ptr_vector<expr> const& vars);
         ptr_vector<expr> const& get_candidate_uninterp();
 
         void check_restart();
+        void reset_uninterp_in_false_literals();
+        bool is_bv_literal(sat::literal lit);
+        bool is_false_bv_literal(sat::literal lit);
+
+        void search();
+
+
 
     public:
         bv_lookahead(bv_eval& ev);
 
         void updt_params(params_ref const& p);
 
-        lbool search();
-
-        void start_propagation() { m_rescore = true; }
+        void start_propagation();
 
         bool on_restore(expr* e) const;