diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index 9e319ab77..c137cf166 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -681,11 +681,13 @@ namespace sls {
             return false;
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
             commit_eval(e, to_app(arg));
+            IF_VERBOSE(11, verbose_stream() << "repair " << mk_bounded_pp(e, m) << " : " << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
             ctx.new_value_eh(arg);
             return true;
         }
         if (m.is_eq(e) && bv.is_bv(arg) && try_repair_eq(e, i)) {
             commit_eval(e, to_app(arg));
+            IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
             ctx.new_value_eh(arg);
             return true;
         }
@@ -1339,7 +1341,6 @@ namespace sls {
     }
 
     bool bv_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
-        //verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
         if (e) {
             // a >= t
             return a.set_random_at_least(b.bits(), m_rand);
@@ -1988,9 +1989,14 @@ namespace sls {
                 return false;
             }
         }
-        //verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
-        if (v.commit_eval())
+
+        if (v.eval == v.bits())
             return true;
+        //verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
+        if (v.commit_eval()) {
+            ctx.new_value_eh(e);
+            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";
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 57ff28b8a..14a2d1758 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -160,8 +160,6 @@ namespace sls {
                 if (ctx.is_true(e) != m_eval.bval1(e))
                     ctx.flip(ctx.atom2bool_var(e));
             }
-            else
-                ctx.new_value_eh(e);
         }
         else if (bv.is_bv(e)) {
             log(e, true, false);
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
index ef6bb57bb..cc4b13a31 100644
--- a/src/ast/sls/sls_bv_valuation.cpp
+++ b/src/ast/sls/sls_bv_valuation.cpp
@@ -181,6 +181,7 @@ namespace sls {
         
         for (unsigned i = 0; i < nw; ++i) 
             m_bits[i] = eval[i]; 
+
         SASSERT(well_formed()); 
         return true;
     }
@@ -662,8 +663,10 @@ namespace sls {
         }
 
         // a[hi_index:0] was incremented, but a[:hi_index+1] cannot be decremented.
-
-
+        // maximize a[:hi_index+1] to model wrap around behavior.
+        for (unsigned i = hi_index + 1; i < bw; ++i) 
+            if (!fixed.get(i)) 
+                a.set(i, true);       
     }
 
     void bv_valuation::tighten_range() {