diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index c3a65218e..2c1796294 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -14,6 +14,7 @@ Author:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/sls/sls_bv_eval.h"
+#include "ast/sls/sls_bv_terms.h"
 #include "ast/rewriter/th_rewriter.h"
 
 namespace sls {
@@ -116,22 +117,24 @@ namespace sls {
         return false;
     }
 
-    bool bv_eval::bval1_bv(app* e) const {
+    bool bv_eval::bval1_bv(app* e, bool use_current) 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_on_restore.is_marked(e->get_arg(0)));
+        bool use_current2 = use_current || (e->get_num_args() > 1 && !m_on_restore.is_marked(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.bits().data(), a.nw, b.bits().data(), b.nw));
+            return f(mpn.compare(a.tmp_bits(use_current1).data(), a.nw, b.tmp_bits(use_current2).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, m_tmp);
-            add_p2_1(b, m_tmp2);
+            add_p2_1(a, use_current1, m_tmp);
+            add_p2_1(b, use_current2, m_tmp2);
             return f(mpn.compare(m_tmp.data(), a.nw, m_tmp2.data(), b.nw));
         };
 
@@ -139,7 +142,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.bits(), b.bits());
+            return a.set_mul(m_tmp2, a.tmp_bits(use_current1), b.tmp_bits(use_current2));
         };
 
         switch (e->get_decl_kind()) {
@@ -164,7 +167,7 @@ namespace sls {
             unsigned idx;
             VERIFY(bv.is_bit2bool(e, child, idx));
             auto& a = wval(child);
-            return a.get_bit(idx);
+            return a.tmp_bits(use_current1).get(idx);
         }
         case OP_BUMUL_NO_OVFL: 
             return !umul_overflow();
@@ -174,7 +177,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.bits(), b.bits());
+            return a.set_add(m_tmp, a.tmp_bits(use_current1), b.tmp_bits(use_current1));
         }
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:         
@@ -193,7 +196,7 @@ namespace sls {
 
     bool bv_eval::bval1(app* e) const {
         if (e->get_family_id() == bv.get_fid())
-            return bval1_bv(e);
+            return bval1_bv(e, true);
         expr* x, * y;
         if (m.is_eq(e, x, y) && bv.is_bv(x)) {
             return wval(x).bits() == wval(y).bits();
@@ -203,6 +206,22 @@ namespace sls {
         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_on_restore.is_marked(x);
+            bool use_current2 = !m_on_restore.is_marked(y);
+            return wval(x).tmp_bits(use_current1) == wval(y).tmp_bits(use_current2);
+        }
+        verbose_stream() << mk_bounded_pp(e, m) << "\n";
+        UNREACHABLE();
+        return false;
+    }
+
+    // unsigned ddt_orig(expr* e);
+
     sls::bv_valuation& bv_eval::eval(app* e) const {
         auto& val = *m_values[e->get_id()];        
         eval(e, val);
@@ -661,15 +680,18 @@ namespace sls {
         if (m.is_value(arg))
             return false;
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
-            commit_eval(to_app(arg));
+            commit_eval(e, to_app(arg));
             ctx.new_value_eh(arg);
             return true;
         }
         if (m.is_eq(e) && bv.is_bv(arg) && try_repair_eq(e, i)) {
-            commit_eval(to_app(arg));
+            commit_eval(e, to_app(arg));
             ctx.new_value_eh(arg);
             return true;
         }
+        if (m.is_eq(e) && bv.is_bv(arg)) {
+            return try_repair_eq_lookahead(e);
+        }
         return false;
     }
 
@@ -856,13 +878,46 @@ namespace sls {
         return false;
     }
 
+    bool bv_eval::try_repair_eq_lookahead(app* e) {
+        auto is_true = bval0(e);
+        if (!is_true)
+            return false;
+        auto const& uninterp = terms.uninterp_occurs(e);
+        if (uninterp.empty())
+            return false;
+        for (auto e : uninterp)
+            verbose_stream() << mk_bounded_pp(e, m) << " ";
+        verbose_stream() << "\n";
+
+        expr* t = uninterp[m_rand() % uninterp.size()];
+
+        auto& v = wval(t);
+        if (v.set_random(m_rand)) {
+            verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
+            ctx.new_value_eh(t);
+            return true;
+        }
+        return false;
+
+
+        for (auto e : uninterp) {
+            auto& v = wval(e);
+            v.get_variant(m_tmp, m_rand);
+            auto d = lookahead(e, m_tmp);
+            verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
+        }
+        return false;
+    }
+
     bool bv_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {
             if (m_rand(20) != 0) 
                 if (a.try_set(b.bits()))
                     return true;
-            
-            return a.set_random(m_rand);
+
+            if (m_rand(20) == 0)
+                return a.set_random(m_rand);
+            return false; 
         }
         else {
             bool try_above = m_rand(2) == 0;
@@ -980,7 +1035,9 @@ namespace sls {
     // 
     bool bv_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
         if (m_rand(20) != 0) {
+            m_tmp.set_bw(a.bw);
             a.set_sub(m_tmp, e, b.bits());
+            // verbose_stream() << "set-sub " << e << " - " << b.bits() << " = " << m_tmp << "\n";
             if (a.try_set(m_tmp))
                 return true;
         }
@@ -1258,9 +1315,9 @@ namespace sls {
         return r;
     }
 
-    void bv_eval::add_p2_1(bvval const& a, bvect& t) const {
+    void bv_eval::add_p2_1(bvval const& a, bool use_current, bvect& t) const {
         m_zero.set(a.bw - 1, true);
-        a.set_add(t, a.bits(), m_zero);
+        a.set_add(t, a.tmp_bits(use_current), m_zero);
         m_zero.set(a.bw - 1, false);
         a.clear_overflow_bits(t);
     }
@@ -1851,6 +1908,7 @@ namespace sls {
     // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
     // 
     bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
+        //verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n";
         if (m_rand(m_config.m_prob_randomize_extract)  <= 100) {
             a.get_variant(m_tmp, m_rand);
             if (0 == (m_rand(2))) {
@@ -1868,9 +1926,13 @@ namespace sls {
             a.get(m_tmp);
         for (unsigned i = 0; i < e.bw; ++i)
             m_tmp.set(i + lo, e.get(i));
-        if (a.try_set(m_tmp))
+        m_tmp.set_bw(a.bw);
+        //verbose_stream() << a << " := " << m_tmp << "\n";
+        if (m_rand(5) != 0 && a.try_set(m_tmp))
             return true;
-        return a.set_random(m_rand);
+        bool ok = a.set_random(m_rand);
+        //verbose_stream() << "set random " << ok << " " << a << "\n";
+        return ok;
     }
 
     bool bv_eval::try_repair_int2bv(bvect const& e, expr* arg) {
@@ -1917,14 +1979,21 @@ namespace sls {
         if (!bv.is_bv(e))
             return false;
         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]))) {
+                verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n";
                 v.bits().copy_to(v.nw, v.eval);
+
                 return false;
             }
         }
+        //verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
         if (v.commit_eval())
             return true;
+        verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
+        for (expr* arg : *to_app(e))
+            verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";
         v.bits().copy_to(v.nw, v.eval);
         return false;
     }
@@ -1935,17 +2004,25 @@ namespace sls {
     }
 
 
-    void bv_eval::commit_eval(app* e) {
+    void bv_eval::commit_eval(expr* p, app* e) {
         if (!bv.is_bv(e))
             return;
+
+        if (e->get_id() == 5) {
+            //verbose_stream() << e->get_id() << " " << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
+            //verbose_stream() << "parent " << mk_bounded_pp(p, m) << " := " << wval(p) << "\n";
+        }
         //
         SASSERT(wval(e).commit_eval());
         VERIFY(wval(e).commit_eval());
     }
 
     void bv_eval::set_random(app* e) {
-        if (bv.is_bv(e))
-            eval(e).set_random(m_rand);
+        if (bv.is_bv(e)) {
+            auto& v = wval(e);
+            if (v.set_random(m_rand))
+                VERIFY(v.commit_eval());
+        }
     }
 
     bool bv_eval::eval_is_correct(app* e) {
@@ -1992,4 +2069,74 @@ namespace sls {
             return out << wval(e);
         return out << "?";
     }
+
+    double bv_eval::lookahead(expr* e, bvect const& new_value) {
+        SASSERT(bv.is_bv(e));
+        SASSERT(is_uninterp(e));
+        SASSERT(m_restore.empty());
+
+        bool has_tabu = false;
+        double break_count = 0, make_count = 0;
+
+        wval(e).eval = new_value;
+        if (!insert_update(e)) {
+            restore_lookahead();
+            return -1000000;
+        }
+        insert_update_stack(e);
+        unsigned max_depth = get_depth(e);
+        for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
+            for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
+                e = m_update_stack[depth][i];
+                if (bv.is_bv(e)) {
+                    auto& v = eval(to_app(e));
+                    if (insert_update(e)) {
+                        for (auto p : ctx.parents(e)) {
+                            insert_update_stack(p);
+                            max_depth = std::max(max_depth, get_depth(p));
+                        }
+                    }
+                    else
+                        has_tabu = true;                
+                }
+                else if (m.is_bool(e) && can_eval1(to_app(e))) {
+                    bool is_true = ctx.is_true(e);
+                    bool is_true_new = bval1(to_app(e));
+                    bool is_true_old = bval1_tmp(to_app(e));
+                    verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
+                    if (is_true == is_true_new && is_true_new != is_true_old)
+                        ++make_count;
+                    if (is_true == is_true_old && is_true_new != is_true_old)
+                        ++break_count;
+                }
+            }
+            m_update_stack[depth].reset();
+        }
+        restore_lookahead();
+        if (has_tabu)
+            return -10000;
+        return make_count - break_count;
+    }
+
+    bool bv_eval::insert_update(expr* e) {
+        m_restore.push_back(e);
+        m_on_restore.mark(e);
+        auto& v = wval(e);
+        v.save_value();
+        return v.commit_eval();
+    }
+
+    void bv_eval::insert_update_stack(expr* e) {
+        unsigned depth = get_depth(e);
+        m_update_stack.reserve(depth + 1);
+        if (!m_update_stack[depth].contains(e))
+            m_update_stack[depth].push_back(e);
+    }
+
+    void bv_eval::restore_lookahead() {
+        for (auto e : m_restore) 
+            wval(e).restore_value();
+        m_restore.reset();
+        m_on_restore.reset();
+    }
 }
diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h
index bdbf00a49..a4587b987 100644
--- a/src/ast/sls/sls_bv_eval.h
+++ b/src/ast/sls/sls_bv_eval.h
@@ -57,6 +57,14 @@ namespace sls {
         using bvval = sls::bv_valuation;
 
         void init_eval_bv(app* e);
+
+        ptr_vector<expr> m_restore;
+        vector<ptr_vector<expr>> m_update_stack;
+        expr_mark m_on_restore;
+        void insert_update_stack(expr* e);
+        bool insert_update(expr* e);
+        double lookahead(expr* e, bvect const& new_value);
+        void restore_lookahead();
        
         /**
         * Register e as a bit-vector. 
@@ -65,7 +73,9 @@ namespace sls {
         void add_bit_vector(app* e);
         sls::bv_valuation* alloc_valuation(app* e);
 
-        bool bval1_bv(app* e) const;  
+        bool bval1_bv(app* e, bool use_current) const;  
+        bool bval1_tmp(app* e) const;
+
 
         void fold_oper(bvect& out, app* e, unsigned i, std::function<void(bvect&, bvval const&)> const& f);
         /**
@@ -113,8 +123,9 @@ namespace sls {
         bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_eq(bool is_true, bvval& a, bvval const& b);
         bool try_repair_eq(app* e, unsigned i);
+        bool try_repair_eq_lookahead(app* e);
         bool try_repair_int2bv(bvect const& e, expr* arg);
-        void add_p2_1(bvval const& a, bvect& t) const;
+        void add_p2_1(bvval const& a, bool use_current, 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);
@@ -137,7 +148,7 @@ namespace sls {
 
         bool can_eval1(app* e) const;
 
-        void commit_eval(app* e);
+        void commit_eval(expr* p, app* e);
 
     public:
         bv_eval(sls::bv_terms& terms, sls::context& ctx);
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index f72186b67..55688a34a 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -28,6 +28,7 @@ namespace sls {
     {}
 
     void bv_fixed::init() {
+
         for (auto e : ctx.subterms())
             set_fixed(e);
 
@@ -40,6 +41,8 @@ namespace sls {
             ev.m_fixed.setx(a->get_id(), true, false);
         }
 
+
+
         for (auto e : ctx.subterms())
             propagate_range_up(e);    
     }
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index fe4972ec2..2b35bd154 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -165,8 +165,11 @@ namespace sls {
         }
         else if (bv.is_bv(e)) {
             log(e, true, false);
-            IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e));             
+            IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e)); 
+            verbose_stream() << "set random " << m_eval.wval(e) << " --> ";
+            auto& v = m_eval.wval(e);
             m_eval.set_random(e);
+            verbose_stream() << m_eval.wval(e) << "\n";
             ctx.new_value_eh(e);
         }
         else
@@ -197,11 +200,8 @@ namespace sls {
     }
 
     void bv_plugin::log(expr* e, bool up_down, bool success) {
-        //        unsigned value = 0;
-        // if (bv.is_bv(e))
-        //    value = svector_hash<unsigned_hash>()(m_eval.wval(e).bits());
         IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F");
-                   // if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e).bits();
+                   if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e);
                    verbose_stream() << "\n");
     }
 
diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp
index f309ff077..5b9d064bb 100644
--- a/src/ast/sls/sls_bv_terms.cpp
+++ b/src/ast/sls/sls_bv_terms.cpp
@@ -32,30 +32,18 @@ namespace sls {
         auto r = ensure_binary(e);
         if (r != e)
             m_axioms.push_back(m.mk_eq(e, r));
+        register_uninterp(e);
     }
 
     expr_ref bv_terms::ensure_binary(expr* e) {
-
-        app* a = to_app(e);
-        auto arg = [&](unsigned i) {
-            return a->get_arg(i);
-        };
-        unsigned num_args = a->get_num_args();
+        expr* x, * y;
         expr_ref r(m);
-#define FOLD_OP(oper)           \
-        r = arg(0);             \
-        for (unsigned i = 1; i < num_args; ++i)\
-            r = oper(r, arg(i)); \
-
-        if (bv.is_bv_sdiv(e) || bv.is_bv_sdiv0(e) || bv.is_bv_sdivi(e)) {
-            r = mk_sdiv(arg(0), arg(1));
-        }
-        else if (bv.is_bv_smod(e) || bv.is_bv_smod0(e) || bv.is_bv_smodi(e)) {
-            r = mk_smod(arg(0), arg(1));
-        }
-        else if (bv.is_bv_srem(e) || bv.is_bv_srem0(e) || bv.is_bv_sremi(e)) {
-            r = mk_srem(arg(0), arg(1));
-        }
+        if (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y))
+            r = mk_sdiv(x, y);
+        else if (bv.is_bv_smod(e, x, y) || bv.is_bv_smod0(e, x, y) || bv.is_bv_smodi(e, x, y))
+            r = mk_smod(x, y);
+        else if (bv.is_bv_srem(e, x, y) || bv.is_bv_srem0(e, x, y) || bv.is_bv_sremi(e, x, y)) 
+            r = mk_srem(x, y);        
         else
             r = e;                   
         return r;
@@ -124,4 +112,33 @@ namespace sls {
         return r;
     }
 
+    void bv_terms::register_uninterp(expr* e) {
+        if (!m.is_bool(e))
+            return;
+        expr* x, *y;
+
+        if (m.is_eq(e, x, y) && bv.is_bv(x))
+            ;
+        else if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid())
+            ;
+        else
+            return;
+        m_uninterp_occurs.reserve(e->get_id() + 1);
+        auto& occs = m_uninterp_occurs[e->get_id()];
+        ptr_vector<expr> todo;
+        todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        expr_mark marked;
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            e = todo[i];
+            if (marked.is_marked(e))
+                continue;
+            marked.mark(e);
+            if (is_app(e) && to_app(e)->get_family_id() == bv.get_fid()) {
+                for (expr* arg : *to_app(e))
+                    todo.push_back(arg);
+            }
+            else if (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 9fc71ba0e..98d57dead 100644
--- a/src/ast/sls/sls_bv_terms.h
+++ b/src/ast/sls/sls_bv_terms.h
@@ -33,6 +33,7 @@ namespace sls {
         ast_manager&        m;
         bv_util             bv;
         expr_ref_vector     m_axioms;
+        vector<ptr_vector<expr>> m_uninterp_occurs;
 
         expr_ref ensure_binary(expr* e);
 
@@ -40,11 +41,15 @@ namespace sls {
         expr_ref mk_smod(expr* x, expr* y);
         expr_ref mk_srem(expr* x, expr* y);
 
+        void register_uninterp(expr* e);
+
     public:
         bv_terms(sls::context& ctx);       
 
         void register_term(expr* e);
 
         expr_ref_vector& axioms() { return m_axioms; }
+
+        ptr_vector<expr> const& uninterp_occurs(expr* e) { m_uninterp_occurs.reserve(e->get_id() + 1); return m_uninterp_occurs[e->get_id()]; }
     };
 }
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
index 65a6ac4a9..210b542ec 100644
--- a/src/ast/sls/sls_bv_valuation.cpp
+++ b/src/ast/sls/sls_bv_valuation.cpp
@@ -247,14 +247,17 @@ namespace sls {
 
     bool bv_valuation::set_random_at_most(bvect const& src, random_gen& r) {
         m_tmp.set_bw(bw);
+        //verbose_stream() << "set_random_at_most " << src << "\n";
         if (!get_at_most(src, m_tmp))
             return false;
 
-        if (is_zero(m_tmp) && (0 != r(10)))
+        if (is_zero(m_tmp) && (0 != r(2)))
             return try_set(m_tmp) && m_tmp <= src;
 
         // random value below tmp
         set_random_below(m_tmp, r);
+
+        //verbose_stream() << "can set " << m_tmp << " " << can_set(m_tmp) << "\n";
         
         return (can_set(m_tmp) || get_at_most(src, m_tmp)) && m_tmp <= src && try_set(m_tmp);
     }
@@ -354,7 +357,7 @@ namespace sls {
                     dst.set(i, false);
             for (unsigned i = 0; i < bw && dst < m_lo && !in_range(dst); ++i)
                 if (!fixed.get(i) && !dst.get(i))
-                    dst.set(i, true);        
+                    dst.set(i, true);
         }
         else {
             for (unsigned i = 0; !in_range(dst) && i < bw; ++i)
@@ -441,7 +444,35 @@ namespace sls {
 
     bool bv_valuation::set_random(random_gen& r) {
         get_variant(m_tmp, r);
-        return set_repair(r(2) == 0, m_tmp);
+        repair_sign_bits(m_tmp);
+        if (in_range(m_tmp)) {
+            set(eval, m_tmp);
+            return true;
+        }
+        for (unsigned i = 0; i < nw; ++i)
+            m_tmp[i] = random_bits(r);
+        clear_overflow_bits(m_tmp);
+        // find a random offset within [lo, hi[
+        SASSERT(m_lo != m_hi);
+        set_sub(eval, m_hi, m_lo);        
+        for (unsigned i = bw; i-- > 0 && m_tmp >= eval; ) 
+            m_tmp.set(i, false);
+        
+        // set eval back to m_bits. It was garbage.
+        set(eval, m_bits);
+
+        // tmp := lo + tmp is within [lo, hi[
+        set_add(m_tmp, m_tmp, m_lo);
+        // respect fixed bits
+        for (unsigned i = 0; i < bw; ++i)
+            if (fixed.get(i))
+                m_tmp.set(i, m_bits.get(i));                
+        // decrease tmp until it is in range again
+        for (unsigned i = bw; i-- > 0 && !in_range(m_tmp); )
+            if (!fixed.get(i))
+                m_tmp.set(i, false);
+        repair_sign_bits(m_tmp);
+        return try_set(m_tmp);      
     }
 
     void bv_valuation::repair_sign_bits(bvect& dst) const {
diff --git a/src/ast/sls/sls_bv_valuation.h b/src/ast/sls/sls_bv_valuation.h
index 393880698..f2d2ae92f 100644
--- a/src/ast/sls/sls_bv_valuation.h
+++ b/src/ast/sls/sls_bv_valuation.h
@@ -132,6 +132,7 @@ namespace sls {
 
         digit_t bits(unsigned i) const { return m_bits[i]; }
         bvect const& bits() const { return m_bits; }
+        bvect const& tmp_bits(bool use_current) const { return use_current ? m_bits : m_tmp; }
         bool commit_eval();
         bool is_fixed() const { for (unsigned i = bw; i-- > 0; ) if (!fixed.get(i)) return false; return true; }
 
@@ -165,6 +166,9 @@ namespace sls {
         bool has_range() const { return m_lo != m_hi; }
         void tighten_range();
 
+        void save_value() { m_tmp = m_bits; }
+        void restore_value() { m_bits = m_tmp; }
+
         void clear_overflow_bits(bvect& bits) const {
             SASSERT(nw > 0);
             bits[nw - 1] &= mask;