diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index e1350b6a0..3c55ec03d 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -196,6 +196,11 @@ namespace bv {
     bool sls_eval::bval1(app* e) const {
         if (e->get_family_id() == bv.get_fid())
             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;
     }
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index b5f04a3a7..3b34e0bec 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -503,7 +503,7 @@ namespace bv {
         if (h == l)
             return;
 
-//        verbose_stream() << *this << " " << l << " " << h << " --> ";
+        //verbose_stream() << *this << " lo " << l << " hi " << h << " --> ";
 
         if (m_lo == m_hi) {
             set_value(m_lo, l);
@@ -615,6 +615,12 @@ namespace bv {
         if (m_lo == m_hi)
             return;
 
+        if (!in_range(m_bits))
+            m_bits = m_lo;
+
+        if (is_zero(m_hi)) 
+            return;        
+
         inf_feasible(m_lo);
 
         bvect& hi1 = m_tmp;