diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index a2bb9d8138d..41c2ef75238 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -445,6 +445,11 @@ class bv_recognizers {
     MATCH_BINARY(is_bv_sdivi);
     MATCH_BINARY(is_bv_udivi);
     MATCH_BINARY(is_bv_smodi);
+    MATCH_BINARY(is_bv_urem0);
+    MATCH_BINARY(is_bv_srem0);
+    MATCH_BINARY(is_bv_sdiv0);
+    MATCH_BINARY(is_bv_udiv0);
+    MATCH_BINARY(is_bv_smod0);
     MATCH_UNARY(is_bit2bool);
     MATCH_UNARY(is_int2bv);
     bool is_bit2bool(expr* e, expr*& bv, unsigned& idx) const;
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index 630e5e423f8..576c0a89e84 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -195,13 +195,8 @@ namespace bv {
         auto scompare = [&](std::function<bool(int)> const& f) {
             auto& a = wval0(e->get_arg(0));
             auto& b = wval0(e->get_arg(1));
-            unsigned c;
-            a.set(m_zero, a.bw - 1, true);
-            mpn.add(a.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp.data(), a.nw + 1, &c);
-            mpn.add(b.bits.data(), a.nw, m_zero.data(), a.nw, m_tmp2.data(), a.nw + 1, &c);
-            a.set(m_zero, a.bw - 1, false); 
-            a.clear_overflow_bits(m_tmp);
-            a.clear_overflow_bits(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));
         };
 
@@ -209,11 +204,7 @@ namespace bv {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
-            mpn.mul(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp2.data());
-            for (unsigned i = a.nw; i < 2 * a.nw; ++i)
-                if (m_tmp2[i] != 0)
-                    return true;
-            return a.has_overflow(m_tmp2);
+            return a.set_mul(m_tmp2, a.bits, b.bits);
         };
 
         switch (e->get_decl_kind()) {
@@ -248,9 +239,7 @@ namespace bv {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
-            digit_t c = 0;
-            mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp.data(), a.nw + 1, &c);
-            return c != 0 || a.has_overflow(m_tmp);
+            return a.set_add(m_tmp, a.bits, b.bits);
         }
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:         
@@ -300,8 +289,8 @@ namespace bv {
         }
         auto set_sdiv = [&]() {
             // d = udiv(abs(x), abs(y))
-            // y = 0, x > 0 -> -1
-            // y = 0, x <= 0 -> -1
+            // y = 0, x >= 0 -> -1
+            // y = 0, x < 0 -> 1
             // x = 0, y != 0 -> 0
             // x > 0, y < 0 -> -d
             // x < 0, y > 0 -> -d
@@ -309,39 +298,34 @@ namespace bv {
             // x < 0, y < 0 -> d
             auto& a = wval0(e->get_arg(0));
             auto& b = wval0(e->get_arg(1));
-            if (a.is_zero() && b.is_zero())
-                val.set(m_minus_one);
+            bool sign_a = a.sign();
+            bool sign_b = b.sign();
+            if (b.is_zero()) {
+                if (sign_a)
+                    val.set(m_one);
+                else
+                    val.set(m_minus_one);
+            }
             else if (a.is_zero())
                 val.set(m_zero);
-            else if (b.is_zero())
-                val.set(m_minus_one);
-            else if (!a.sign() && b.is_zero())
-                val.set(m_one);
             else {
-                bool sign_a = a.sign();
-                bool sign_b = b.sign();
-                digit_t c;
-
                 if (sign_a)
-                    mpn.sub(m_zero.data(), a.nw, a.bits.data(), a.nw, m_tmp.data(), &c);
+                    a.set_sub(m_tmp, m_zero, a.bits);
                 else
                     a.get(m_tmp);
-                val.clear_overflow_bits(m_tmp);
 
                 if (sign_b)
-                    mpn.sub(m_zero.data(), a.nw, b.bits.data(), a.nw, m_tmp2.data(), &c);
+                    b.set_sub(m_tmp2, m_zero, b.bits);
                 else
                     b.get(m_tmp2);
-                val.clear_overflow_bits(m_tmp2);
 
                 mpn.div(m_tmp.data(), a.nw, m_tmp2.data(), a.nw, m_tmp3.data(), m_tmp4.data());
                 if (sign_a == sign_b)
                     val.set(m_tmp3);
                 else
-                    mpn.sub(m_zero.data(), a.nw, m_tmp3.data(), a.nw, m_tmp.data(), &c),
-                    val.set(m_tmp);
+                    val.set_sub(val.bits, m_zero, m_tmp3);
             }
-            };
+        };
 
         auto mk_rotate_left = [&](unsigned n) {            
             auto& a = wval0(e->get_arg(0));
@@ -392,23 +376,21 @@ namespace bv {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
-            digit_t c;
-            mpn.add(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), val.nw + 1, &c);
+            val.set_add(val.bits, a.bits, b.bits);
             break;
         }
         case OP_BSUB: {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
-            digit_t c;
-            mpn.sub(a.bits.data(), a.nw, b.bits.data(), b.nw, val.bits.data(), &c);
+            val.set_sub(val.bits, a.bits, b.bits);
             break;
         }
         case OP_BMUL: {
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
-            mpn.mul(a.bits.data(), a.nw, b.bits.data(), b.nw, m_tmp2.data());
+            val.set_mul(m_tmp2, a.bits, b.bits);
             val.set(m_tmp2);
             break;
         }
@@ -429,7 +411,7 @@ namespace bv {
             auto const& a = wval0(child);
             SASSERT(lo <= hi && hi + 1 <= a.bw && hi - lo + 1 == val.bw);
             for (unsigned i = lo; i <= hi; ++i)
-                val.set(val.bits, i - lo, a.get(a.bits, i));         
+                val.set(val.bits, i - lo, a.get(a.bits, i));
             break;
         }
         case OP_BNOT: {
@@ -440,8 +422,7 @@ namespace bv {
         }
         case OP_BNEG: {
             auto& a = wval0(e->get_arg(0));
-            digit_t c;
-            mpn.sub(m_zero.data(), a.nw, a.bits.data(), a.nw, val.bits.data(), &c);
+            val.set_sub(val.bits, m_zero, a.bits);
             break;
         }
         case OP_BIT0:
@@ -530,7 +511,7 @@ namespace bv {
         case OP_BSMOD:
         case OP_BSMOD_I:
         case OP_BSMOD0: {
-            // u = mod(x,y)
+            // u = mod(abs(x),abs(y))
             // u = 0 ->  0
             // y = 0 ->  x
             // x < 0, y < 0 ->  -u
@@ -542,22 +523,26 @@ namespace bv {
             if (b.is_zero())
                 val.set(a.bits);
             else {
-                digit_t c;
-                mpn.div(a.bits.data(), a.nw,
-                    b.bits.data(), b.nw,
+                if (a.sign())
+                    a.set_sub(m_tmp3, m_zero, a.bits);
+                else
+                    a.set(m_tmp3, a.bits);
+                if (b.sign())
+                    b.set_sub(m_tmp4, m_zero, b.bits);
+                else
+                    a.set(m_tmp4, b.bits);                
+                mpn.div(m_tmp3.data(), a.nw,
+                    m_tmp4.data(), b.nw,
                     m_tmp.data(), // quotient
                     m_tmp2.data()); // remainder
                 if (val.is_zero(m_tmp2))
                     val.set(m_tmp2);
                 else if (a.sign() && b.sign())
-                    mpn.sub(m_zero.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), &c),
-                    val.set(m_tmp);
+                    val.set_sub(val.bits, m_zero, m_tmp2);
                 else if (a.sign())
-                    mpn.sub(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), &c),
-                    val.set(m_tmp);
+                    val.set_sub(val.bits, b.bits, m_tmp2);
                 else if (b.sign())
-                    mpn.add(b.bits.data(), a.nw, m_tmp2.data(), a.nw, m_tmp.data(), a.nw + 1, &c),
-                    val.set(m_tmp);
+                    val.set_add(val.bits, b.bits, m_tmp2);
                 else
                     val.set(m_tmp2);
             }
@@ -590,19 +575,17 @@ namespace bv {
         case OP_BSREM:
         case OP_BSREM0:
         case OP_BSREM_I: {
-            // y = 0 -> x
-            // else x - sdiv(x, y) * y
+            // b = 0 -> a
+            // else a - sdiv(a, b) * b
             // 
             auto& a = wval0(e->get_arg(0));
             auto& b = wval0(e->get_arg(1));
             if (b.is_zero()) 
                 val.set(a.bits);
             else {
-                digit_t c;
                 set_sdiv();
-                mpn.mul(val.bits.data(), a.nw, b.bits.data(), a.nw, m_tmp.data());
-                mpn.sub(a.bits.data(), a.nw, m_tmp.data(), a.nw, m_tmp2.data(), &c);
-                val.set(m_tmp2);
+                val.set_mul(m_tmp, val.bits, b.bits);
+                val.set_sub(val.bits, a.bits, m_tmp);
             }
             break;
         }
@@ -669,6 +652,13 @@ namespace bv {
         val.clear_overflow_bits(val.bits);
     }
 
+    digit_t sls_eval::random_bits() {
+        digit_t r = 0;
+        for (digit_t i = 0; i < sizeof(digit_t); ++i)
+            r ^= m_rand() << (8 * i);
+        return r;
+    }
+
     bool sls_eval::try_repair(app* e, unsigned i) {
         if (is_fixed0(e->get_arg(i)))
             return false;
@@ -781,10 +771,7 @@ namespace bv {
             VERIFY(bv.is_bit2bool(e, arg, idx));
             return try_repair_bit2bool(wval0(e, 0), idx);
         }
-        case OP_BSDIV:
-        case OP_BSDIV_I:
-        case OP_BSDIV0:
-            return try_repair_sdiv(wval0(e), wval0(e, 0), wval0(e, 1), i);
+
         case OP_BUDIV:
         case OP_BUDIV_I:
         case OP_BUDIV0:
@@ -793,14 +780,6 @@ namespace bv {
         case OP_BUREM_I:
         case OP_BUREM0:
             return try_repair_urem(wval0(e), wval0(e, 0), wval0(e, 1), i);
-        case OP_BSREM:
-        case OP_BSREM_I:
-        case OP_BSREM0:
-            return try_repair_srem(wval0(e), wval0(e, 0), wval0(e, 1), i);
-        case OP_BSMOD:
-        case OP_BSMOD_I:
-        case OP_BSMOD0:
-            return try_repair_smod(wval0(e), wval0(e, 0), wval0(e, 1), i);
         case OP_ROTATE_LEFT:
             return try_repair_rotate_left(wval0(e), wval0(e, 0), e->get_parameter(0).get_int());
         case OP_ROTATE_RIGHT:
@@ -822,6 +801,19 @@ namespace bv {
         case OP_BSMUL_OVFL:
         case OP_BUMUL_NO_OVFL:
         case OP_BUMUL_OVFL:
+            return false;
+        case OP_BSREM:
+        case OP_BSREM_I:
+        case OP_BSREM0:
+        case OP_BSMOD:
+        case OP_BSMOD_I:
+        case OP_BSMOD0:
+        case OP_BSDIV:
+        case OP_BSDIV_I:
+        case OP_BSDIV0:
+            // these are currently compiled to udiv and urem.
+            UNREACHABLE();
+            return false;
         default:
             return false;
         }
@@ -922,13 +914,14 @@ namespace bv {
     // e = a & b
     // e[i] = 1 -> a[i] = 1
     // e[i] = 0 & b[i] = 1 -> a[i] = 0
-    //
+    // e[i] = 0 & b[i] = 0 -> a[i] = random
     // a := e[i] | (~b[i] & a[i])
 
     bool sls_eval::try_repair_band(bvval const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < e.nw; ++i)
-            m_tmp[i] = e.bits[i] | (~b.bits[i] & a.bits[i]);
-        return a.try_set(m_tmp);
+            m_tmp[i] = (e.bits[i] & ~a.fixed[i]) | (~b.bits[i] & ~a.fixed[i] & random_bits());
+        a.set_repair(random_bool(), m_tmp);
+        return true;       
     }
 
     //
@@ -938,20 +931,23 @@ namespace bv {
     //     
     bool sls_eval::try_repair_bor(bvval const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < e.nw; ++i)
-            m_tmp[i] = e.bits[i] & (a.bits[i] | ~b.bits[i]);
-        return a.try_set(m_tmp);       
+            m_tmp[i] = e.bits[i] & (~b.bits[i] | random_bits());
+        a.set_repair(random_bool(), m_tmp);
+        return true;     
     }
 
     bool sls_eval::try_repair_bxor(bvval const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < e.nw; ++i)
             m_tmp[i] = e.bits[i] ^ b.bits[i];
-        return a.try_set(m_tmp);
+        a.set_repair(random_bool(), m_tmp);
+        return true;        
     }
 
+
     bool sls_eval::try_repair_add(bvval const& e, bvval& a, bvval const& b) {
-        digit_t c;
-        mpn.sub(e.bits.data(), e.nw, b.bits.data(), e.nw, m_tmp.data(), &c);
-        return a.try_set(m_tmp);
+        a.set_sub(m_tmp, e.bits, b.bits);
+        a.set_repair(random_bool(), m_tmp);
+        return true;
     }
 
     /**
@@ -976,52 +972,84 @@ namespace bv {
         auto inv_b = nb.pseudo_inverse(b.bw);
         rational na = mod(inv_b * ne, rational::power_of_two(a.bw));
         a.set_value(m_tmp, na);
-        return a.try_set(m_tmp);      
+        a.set_repair(random_bool(), m_tmp);
+        return true;        
     }
 
     bool sls_eval::try_repair_bnot(bvval const& e, bvval& a) {
         for (unsigned i = 0; i < e.nw; ++i)
             m_tmp[i] = ~e.bits[i];
-        return a.try_set(m_tmp);       
+        a.clear_overflow_bits(m_tmp);
+        a.set_repair(random_bool(), m_tmp);
+        return true;
     }
 
     bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) {
-        digit_t c;
-        mpn.sub(m_zero.data(), e.nw, e.bits.data(), e.nw, m_tmp.data(), &c);        
-        return a.try_set(m_tmp);
+        a.set_sub(m_tmp, m_zero, e.bits); 
+        a.set_repair(random_bool(), m_tmp);
+        return true;
     }
 
     bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
-        if (e) 
-            return a.try_set(b.bits);
-        else {
-            digit_t c;           
-            mpn.add(b.bits.data(), a.nw, m_one.data(), a.nw, &c, a.nw + 1, m_tmp.data());       
-            return a.try_set(m_tmp);
-        }        
+        return try_repair_ule(e, a, b.bits);       
     }
 
     bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
-        if (e)
-            return a.try_set(b.bits);
-        else {
-            digit_t c;
-            mpn.sub(b.bits.data(), a.nw, m_one.data(), a.nw, m_tmp.data(), &c);          
-            return a.try_set(m_tmp);
-        }        
+        return try_repair_uge(e, a, b.bits);
     }
 
     bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
-        return try_repair_ule(e, a, b);
+        add_p2_1(b, m_tmp4);
+        return try_repair_ule(e, a, m_tmp4);
     }
 
     bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
-        return try_repair_uge(e, a, b);
+        add_p2_1(b, m_tmp4);
+        return try_repair_uge(e, a, m_tmp4);
+    }
+
+    void sls_eval::add_p2_1(bvval const& a, svector<digit_t>& t) const {
+        a.set(m_zero, a.bw - 1, true);
+        a.set_add(t, a.bits, m_zero);
+        a.set(m_zero, a.bw - 1, false);
+        a.clear_overflow_bits(t);
+    }
+
+    bool sls_eval::try_repair_ule(bool e, bvval& a, svector<digit_t> const& t) {
+        if (e) {
+            if (!a.get_at_most(t, m_tmp))
+                return false;
+        }
+        else {
+            // a > b
+            a.set_add(m_tmp2, t, m_one);
+            if (a.is_zero(m_tmp2))
+                return false;
+            if (!a.get_at_least(m_tmp2, m_tmp))
+                return false;           
+        }
+        a.set_repair(random_bool(), m_tmp2);
+        return true;
+    }
+
+    bool sls_eval::try_repair_uge(bool e, bvval& a, svector<digit_t> const& t) {
+        if (e) {
+            if (!a.get_at_least(t, m_tmp))
+                return false;         
+        }
+        else {
+            if (a.is_zero(t))
+                return false;
+            a.set_sub(m_tmp2, t, m_one);
+            if (!a.get_at_most(m_tmp2, m_tmp))
+                return false;
+        }
+        a.set_repair(random_bool(), m_tmp);
+        return true;
     }
 
     bool sls_eval::try_repair_bit2bool(bvval& a, unsigned idx) {
-        for (unsigned i = 0; i < a.nw; ++i)
-            m_tmp[i] = a.bits[i];
+        a.set(m_tmp, a.bits);
         a.set(m_tmp, idx, !a.get(a.bits, idx));
         return a.try_set(m_tmp);
     }
@@ -1090,24 +1118,139 @@ namespace bv {
         return try_repair_ashr(e, a, b, i);
     }
 
-    bool sls_eval::try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i) {
-        return false;
-    }
+    // e = a udiv b
+    // e = 0 => a != ones
+    // b = 0 => e = -1        // nothing to repair on a
+    // e != -1 => max(a) >=u e
 
     bool sls_eval::try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i) {
-        return false;
+        if (i == 0) {
+            if (e.is_zero() && a.is_ones(a.fixed) && a.is_ones())
+                return false;            
+            if (b.is_zero())
+                return true;
+            if (!e.is_ones()) {
+                for (unsigned i = 0; i < a.nw; ++i)
+                    m_tmp[i] = ~a.fixed[i] | a.bits[i];
+                a.clear_overflow_bits(m_tmp);
+                if (a.lt(m_tmp, e.bits))
+                    return false;
+            }
+            // e = 1 => a := b
+            if (e.is_one()) {
+                a.set(m_tmp, b.bits);
+                a.set_repair(false, m_tmp);
+                return true;
+            }
+            // y * e + r = a
+            for (unsigned i = 0; i < a.nw; ++i)
+                m_tmp[i] = random_bits();
+            while (mul_overflow_on_fixed(e, m_tmp)) {
+                auto i = b.msb(m_tmp);
+                b.set(m_tmp, i, false);
+            }
+            for (unsigned i = 0; i < a.nw; ++i)
+                m_tmp2[i] = random_bits();
+            while (b.gt(m_tmp2, b.bits)) 
+                b.set(m_tmp2, b.msb(m_tmp2), false);
+            while (a.set_add(m_tmp3, m_tmp, m_tmp2)) 
+                b.set(m_tmp2, b.msb(m_tmp2), false);            
+            a.set_repair(true, m_tmp3);
+        }
+        else {
+            if (e.is_one()) {
+                b.set(m_tmp, a.bits);
+                b.set_repair(true, m_tmp);
+                return true;
+            }
+            // e * b + r = a
+            // b = (a - r) udiv e 
+            // random version of r:
+            for (unsigned i = 0; i < a.nw; ++i)
+                m_tmp[i] = random_bits();
+            a.clear_overflow_bits(m_tmp);
+            // ensure r <= a
+            while (a.lt(a.bits, m_tmp))
+                a.set(m_tmp, a.msb(m_tmp), false);
+            a.set_sub(m_tmp2, a.bits, m_tmp);
+            mpn.div(m_tmp2.data(), a.nw, e.bits.data(), a.nw, m_tmp3.data(), m_tmp4.data());
+            b.set_repair(random_bool(), m_tmp4);
+        }
+        return true;
     }
 
-    bool sls_eval::try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i) {
-        return false;
-    }
+    // table III in Niemetz et al
+    // x urem s = t <=>
+    //     ~(-s) >=u t 
+    //     ((s = 0 or t = ones) => mcb(x, t))
+    //     ((s != 0 and t != ones) => exists y . (mcb(x, s*y + t) and ~mulo(s, y) and ~addo(s*y, t))
+    // s urem x = t <=> 
+    //      (s = t => x can be >u t)
+    //      (s != t => exists y . (mcb(x, y) and y >u t and (s - t) mod y = 0)
+
 
     bool sls_eval::try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i) {
-        return false;
+
+        if (i == 0) {
+            if (b.is_zero()) {
+                a.set(m_tmp, e.bits);
+                a.set_repair(random_bool(), m_tmp);
+                return true;
+            }
+            // a urem b = e: b*y + e = a
+            // ~Ovfl*(b, y)
+            // ~Ovfl+(b*y, e) 
+            // choose y at random
+            // lower y as long as y*b overflows with fixed bits in b
+
+            for (unsigned i = 0; i < a.nw; ++i)
+                m_tmp[i] = random_bits();
+            while (mul_overflow_on_fixed(b, m_tmp)) {
+                auto i = b.msb(m_tmp);
+                b.set(m_tmp, i, false);
+            }
+            while (true) {
+                a.set_mul(m_tmp2, m_tmp, b.bits);
+                a.clear_overflow_bits(m_tmp2);
+                if (!add_overflow_on_fixed(e, m_tmp2))
+                    break;
+                auto i = b.msb(m_tmp);
+                b.set(m_tmp, i, false);
+            }
+            a.set_add(m_tmp3, m_tmp2, e.bits);
+            a.set_repair(random_bool(), m_tmp3);
+            return true;
+        }
+        else {
+            // a urem b = e: b*y + e = a
+            // b*y = a - e
+            // b = (a - e) div y
+            // ~Ovfl*(b, y)
+            // ~Ovfl+(b*y, e)
+            // choose y at random
+            // lower y as long as y*b overflows with fixed bits in b
+            for (unsigned i = 0; i < a.nw; ++i)
+                m_tmp[i] = random_bits();
+            a.set_sub(m_tmp2, a.bits, e.bits);
+            mpn.div(m_tmp2.data(), a.nw, m_tmp.data(), a.nw, m_tmp3.data(), m_tmp4.data());
+            a.clear_overflow_bits(m_tmp3);
+            b.set_repair(random_bool(), m_tmp3);
+            return true;
+        }
     }
 
-    bool sls_eval::try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i) {
-        return false;
+    bool sls_eval::add_overflow_on_fixed(bvval const& a, svector<digit_t> const& t) {
+        a.set(m_tmp3, m_zero);
+        for (unsigned i = 0; i < a.nw; ++i)
+            m_tmp3[i] = a.fixed[i] & a.bits[i];
+        return a.set_add(m_tmp4, t, m_tmp3);
+    }
+
+    bool sls_eval::mul_overflow_on_fixed(bvval const& a, svector<digit_t> const& t) {
+        a.set(m_tmp3, m_zero);
+        for (unsigned i = 0; i < a.nw; ++i)
+            m_tmp3[i] = a.fixed[i] & a.bits[i];
+        return a.set_mul(m_tmp4, m_tmp3, t);
     }
 
     bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const {
@@ -1116,8 +1259,9 @@ namespace bv {
         for (unsigned i = a.bw - n; i < a.bw; ++i)
             a.set(m_tmp, i + n - a.bw, e.get(e.bits, i));
         for (unsigned i = 0; i < a.bw - n; ++i)
-            a.set(m_tmp, i + a.bw - n, e.get(e.bits, i));
-        return a.try_set(m_tmp);
+            a.set(m_tmp, i + n, e.get(e.bits, i));
+        a.set_repair(true, m_tmp);
+        return true;
     }
 
     bool sls_eval::try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i) {
@@ -1131,7 +1275,8 @@ namespace bv {
             SASSERT(i == 1);
             unsigned sh = m_rand(b.bw);
             b.set(m_tmp, sh);
-            return b.try_set(m_tmp);
+            b.set_repair(random_bool(), m_tmp);
+            return true;
         }       
     }
 
diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h
index 5fa51ed178a..70a08283fdf 100644
--- a/src/ast/sls/bv_sls_eval.h
+++ b/src/ast/sls/bv_sls_eval.h
@@ -83,13 +83,19 @@ namespace bv {
         bool try_repair_ashr(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_bit2bool(bvval& a, unsigned idx);
-        bool try_repair_sdiv(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_udiv(bvval const& e, bvval& a, bvval& b, unsigned i);
-        bool try_repair_smod(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_urem(bvval const& e, bvval& a, bvval& b, unsigned i);
-        bool try_repair_srem(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_rotate_left(bvval const& e, bvval& a, unsigned n) const;
         bool try_repair_rotate_left(bvval const& e, bvval& a, bvval& b, unsigned i);
+        bool try_repair_ule(bool e, bvval& a, svector<digit_t> const& t);
+        bool try_repair_uge(bool e, bvval& a, svector<digit_t> const& t);
+        void add_p2_1(bvval const& a, svector<digit_t>& t) const;
+
+        bool add_overflow_on_fixed(bvval const& a, svector<digit_t> const& t);
+        bool mul_overflow_on_fixed(bvval const& a, svector<digit_t> const& t);
+
+        digit_t random_bits();
+        bool random_bool() { return m_rand() % 2 == 0; }
 
         sls_valuation& wval0(app* e, unsigned i) { return wval0(e->get_arg(i)); }
 
diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp
index 4dafb6034c2..490557a56a7 100644
--- a/src/ast/sls/bv_sls_fixed.cpp
+++ b/src/ast/sls/bv_sls_fixed.cpp
@@ -54,6 +54,7 @@ namespace bv {
     void sls_fixed::init_range(app* e, bool sign) {
         expr* s, * t, * x, * y;
         rational a, b;
+        unsigned idx;
         auto N = [&](expr* s) {
             auto b = bv.get_bv_size(s);
             return b > 0 ? rational::power_of_two(b - 1) : rational(0);
@@ -98,6 +99,19 @@ namespace bv {
             get_offset(t, y, b);
             init_range(x, a + N(s), y, b + N(s), !sign);
         }
+        else if (!sign && m.is_eq(e, s, t)) {
+            if (bv.is_numeral(s, a))
+                // t - a <= 0
+                init_range(t, -a, nullptr, rational(0), !sign);
+            else if (bv.is_numeral(t, a))
+                init_range(s, -a, nullptr, rational(0), !sign);
+        }
+        else if (bv.is_bit2bool(e, s, idx)) {
+            auto& val = wval0(s);
+            val.set(val.bits, idx, !sign);
+            val.set(val.fixed, idx, true);
+            val.init_fixed();
+        }
     }
 
     // 
@@ -167,6 +181,7 @@ namespace bv {
             auto& val_el = wval0(e->get_arg(2));
             for (unsigned i = 0; i < val.nw; ++i)
                 val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits[i] ^ val_th.bits[i]);
+            val.init_fixed();
         }
     }
 
@@ -224,6 +239,13 @@ namespace bv {
                 v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits[i]) | (b.fixed[i] & b.bits[i]);
             break;
         }
+        case OP_BXOR: {
+            auto& a = wval0(e->get_arg(0));
+            auto& b = wval0(e->get_arg(1));
+            for (unsigned i = 0; i < a.nw; ++i)
+                v.fixed[i] = a.fixed[i] & b.fixed[i];
+            break;
+        }
         case OP_BNOT: {
             auto& a = wval0(e->get_arg(0));
             for (unsigned i = 0; i < a.nw; ++i)
@@ -331,9 +353,9 @@ namespace bv {
             // if 0 < b < v.bw is known, then inherit shift of fixed values of a
             // if 0 < b < v.bw but not known, then inherit run lengths of equal bits of a
             // that are fixed.
-            NOT_IMPLEMENTED_YET();
             break;
         }
+
         case OP_BASHR:
         case OP_BLSHR:
         case OP_INT2BV:
@@ -352,10 +374,9 @@ namespace bv {
         case OP_BUREM0:
         case OP_BSMOD:
         case OP_BSMOD_I:
-        case OP_BSMOD0:
-        case OP_BXOR:
+        case OP_BSMOD0:       
         case OP_BXNOR:
-            NOT_IMPLEMENTED_YET();
+            // NOT_IMPLEMENTED_YET();
             break;
         case OP_BV_NUM:
         case OP_BIT0:
@@ -381,6 +402,7 @@ namespace bv {
         case OP_SLT:
             UNREACHABLE();
             break;
-        }        
+        }      
+        v.init_fixed();
     }
 }
diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp
index 422b2017eb6..0a110a7d813 100644
--- a/src/ast/sls/bv_sls_terms.cpp
+++ b/src/ast/sls/bv_sls_terms.cpp
@@ -66,6 +66,7 @@ namespace bv {
         };
         unsigned num_args = a->get_num_args();
         expr_ref r(m);
+        expr* x, * y;
 #define FOLD_OP(oper)           \
         r = arg(0);             \
         for (unsigned i = 1; i < num_args; ++i)\
@@ -98,6 +99,15 @@ namespace bv {
         else if (bv.is_concat(e)) {
             FOLD_OP(bv.mk_concat);
         }
+        else 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 {
             for (unsigned i = 0; i < num_args; ++i)
                 m_todo.push_back(arg(i));
@@ -107,6 +117,60 @@ namespace bv {
         m_translated.setx(e->get_id(), r);
     }
 
+    expr* sls_terms::mk_sdiv(expr* x, expr* y) {
+        // d = udiv(abs(x), abs(y))
+        // y = 0, x > 0 -> 1
+        // y = 0, x <= 0 -> -1
+        // x = 0, y != 0 -> 0
+        // x > 0, y < 0 -> -d
+        // x < 0, y > 0 -> -d
+        // x > 0, y > 0 -> d
+        // x < 0, y < 0 -> d
+        unsigned sz = bv.get_bv_size(x);
+        rational N = rational::power_of_two(sz);
+        expr_ref z(bv.mk_zero(sz), m);
+        expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
+        expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
+        expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
+        expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
+        expr* d = bv.mk_bv_udiv(absx, absy);
+        expr* r = m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d));
+        r = m.mk_ite(m.mk_eq(z, y),
+                m.mk_ite(signx, bv.mk_numeral(N - 1, sz), bv.mk_one(sz)),
+                m.mk_ite(m.mk_eq(x, z), z, r));
+        return r;
+    }
+
+    expr* sls_terms::mk_smod(expr* x, expr* y) {
+        // u := umod(abs(x), abs(y))
+        // u = 0 ->  0
+        // y = 0 ->  x
+        // x < 0, y < 0 ->  -u
+        // x < 0, y >= 0 ->  y - u
+        // x >= 0, y < 0 ->  y + u
+        // x >= 0, y >= 0 ->  u
+        unsigned sz = bv.get_bv_size(x);
+        expr_ref z(bv.mk_zero(sz), m);
+        expr_ref abs_x(m.mk_ite(bv.mk_sle(z, x), x, bv.mk_bv_neg(x)), m);
+        expr_ref abs_y(m.mk_ite(bv.mk_sle(z, y), y, bv.mk_bv_neg(y)), m);
+        expr_ref u(bv.mk_bv_urem(abs_x, abs_y), m);
+        return
+            m.mk_ite(m.mk_eq(u, z), z,
+                m.mk_ite(m.mk_eq(y, z), x,
+                    m.mk_ite(m.mk_and(bv.mk_sle(z, x), bv.mk_sle(z, x)), u,
+                        m.mk_ite(bv.mk_sle(z, x), bv.mk_bv_add(y, u),
+                            m.mk_ite(bv.mk_sle(z, y), bv.mk_bv_sub(y, u), bv.mk_bv_neg(u))))));
+                      
+    }
+
+    expr* sls_terms::mk_srem(expr* x, expr* y) {
+        // y = 0 -> x
+        // else x - sdiv(x, y) * y
+        return 
+            m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))),
+                     x, bv.mk_bv_sub(x, bv.mk_bv_mul(y, mk_sdiv(x, y))));
+    }
+
 
     void sls_terms::init() {
         // populate terms
diff --git a/src/ast/sls/bv_sls_terms.h b/src/ast/sls/bv_sls_terms.h
index 68804784676..95d9a508eba 100644
--- a/src/ast/sls/bv_sls_terms.h
+++ b/src/ast/sls/bv_sls_terms.h
@@ -40,6 +40,10 @@ namespace bv {
         expr* ensure_binary(expr* e);
         void ensure_binary_core(expr* e);
 
+        expr* mk_sdiv(expr* x, expr* y);
+        expr* mk_smod(expr* x, expr* y);
+        expr* mk_srem(expr* x, expr* y);
+
     public:
         sls_terms(ast_manager& m);
         
@@ -65,6 +69,5 @@ namespace bv {
 
         bool is_assertion(expr* e) const { return m_assertion_set.contains(e->get_id()); }
 
-
     };
 }
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index fb2c8f129ad..75307c6677b 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -33,15 +33,13 @@ namespace bv {
         for (unsigned i = 0; i < nw; ++i)
             lo[i] = 0, hi[i] = 0, bits[i] = 0, fixed[i] = 0;
         for (unsigned i = bw; i < 8 * sizeof(digit_t) * nw; ++i)
-            set(fixed, i, false);
-    }
-
-    sls_valuation::~sls_valuation() {
+            set(fixed, i, true);
     }
 
     bool sls_valuation::in_range(svector<digit_t> const& bits) const {
         mpn_manager m;    
         auto c = m.compare(lo.data(), nw, hi.data(), nw);
+        SASSERT(!has_overflow(bits));
         // full range
         if (c == 0)
             return true;
@@ -56,44 +54,187 @@ namespace bv {
             m.compare(bits.data(), nw, hi.data(), nw) < 0;
     }
 
-    bool sls_valuation::eq(svector<digit_t> const& other) const {
-        auto c = 0 == memcmp(bits.data(), other.data(), bw / 8);
-        if (bw % 8 == 0 || !c)
-            return c;
-        for (unsigned i = 8 * (bw / 8); i < bw; ++i)
-            if (get(bits, i) != get(other, i))
-                return false;
-        return true;
+    bool sls_valuation::eq(svector<digit_t> const& a, svector<digit_t> const& b) const {
+        SASSERT(!has_overflow(a));
+        SASSERT(!has_overflow(b));
+        return 0 == memcmp(a.data(), b.data(), num_bytes());
     }
 
     bool sls_valuation::gt(svector<digit_t> const& a, svector<digit_t> const& b) const {
+        SASSERT(!has_overflow(a));
+        SASSERT(!has_overflow(b));
         mpn_manager m;
         return m.compare(a.data(), nw, b.data(), nw) > 0;
     }
 
+    bool sls_valuation::lt(svector<digit_t> const& a, svector<digit_t> const& b) const {
+        SASSERT(!has_overflow(a));
+        SASSERT(!has_overflow(b));
+        mpn_manager m;
+        return m.compare(a.data(), nw, b.data(), nw) < 0;
+    }
+
+    bool sls_valuation::le(svector<digit_t> const& a, svector<digit_t> const& b) const {
+        SASSERT(!has_overflow(a));
+        SASSERT(!has_overflow(b));
+        mpn_manager m;
+        return m.compare(a.data(), nw, b.data(), nw) <= 0;
+    }
+
     void sls_valuation::clear_overflow_bits(svector<digit_t>& bits) const { 
         for (unsigned i = bw; i < nw * sizeof(digit_t) * 8; ++i)
             set(bits, i, false);
+        SASSERT(!has_overflow(bits));
     }
 
-    bool sls_valuation::get_below(svector<digit_t> const& src, svector<digit_t>& dst) {
+    //
+    // largest dst <= src and dst is feasible
+    // set dst := src & (~fixed | bits)
+    // 
+    // increment dst if dst < src by setting bits below msb(src & ~dst) to 1
+    // 
+    // if dst < lo < hi:
+    //    return false
+    // if lo < hi <= dst:
+    //    set dst := hi - 1
+    // if hi <= dst < lo
+    //    set dst := hi - 1
+    // 
+
+    bool sls_valuation::get_at_most(svector<digit_t> const& src, svector<digit_t>& dst) const {
+        SASSERT(!has_overflow(src));
         for (unsigned i = 0; i < nw; ++i)
-            dst[i] = (src[i] & ~fixed[i]) | (fixed[i] & bits[i]);
+            dst[i] = src[i] & (~fixed[i] | bits[i]);
+
+        //
+        // If dst < src, then find the most significant 
+        // bit where src[idx] = 1, dst[idx] = 0
+        // set dst[j] = bits_j | ~fixed_j for j < idx
+        //
+        for (unsigned i = nw; i-- > 0; ) {
+            if (0 != (~dst[i] & src[i])) {
+                auto idx = log2(~dst[i] & src[i]);
+                auto mask = (1 << idx) - 1;
+                dst[i] = (~fixed[i] & mask) | dst[i];
+                for (unsigned j = i; j-- > 0; )
+                    dst[j] = (~fixed[j] | bits[j]);
+                break;
+            }
+        }
+        SASSERT(!has_overflow(dst));
+        return round_down(dst);
+    }
+
+    //
+    // smallest dst >= src and dst is feasible with respect to this.
+    // set dst := (src & ~fixed) | (fixed & bits)
+    // 
+    // decrement dst if dst > src by setting bits below msb to 0 unless fixed
+    // 
+    // if lo < hi <= dst
+    //    return false
+    // if dst < lo < hi:
+    //    set dst := lo
+    // if hi <= dst < lo
+    //    set dst := lo
+    // 
+    bool sls_valuation::get_at_least(svector<digit_t> const& src, svector<digit_t>& dst) const {
+        SASSERT(!has_overflow(src));
         for (unsigned i = 0; i < nw; ++i)
-            dst[i] = fixed[i] & bits[i];
-        if (gt(dst, src))
-            return false;
-        if (!in_range(dst)) {
-            // lo < hi:
-            // set dst to lo, except for fixed bits
-            // 
-            if (gt(hi, lo)) {
+            dst[i] = (~fixed[i] & src[i]) | (fixed[i] & bits[i]);
+
+        //
+        // If dst > src, then find the most significant 
+        // bit where src[idx] = 0, dst[idx] = 1
+        // set dst[j] = dst[j] & fixed_j for j < idx
+        //
+        for (unsigned i = nw; i-- > 0; ) {
+            if (0 != (dst[i] & ~src[i])) {
+                auto idx = log2(dst[i] & ~src[i]);
+                auto mask = (1 << idx);
+                dst[i] = dst[i] & (fixed[i] | mask);
+                for (unsigned j = i; j-- > 0; )
+                    dst[j] = dst[j] & fixed[j];
+                break;
+            }
+        }
+        SASSERT(!has_overflow(dst));
+        return round_up(dst);
+    }
+
+    bool sls_valuation::round_up(svector<digit_t>& dst) const {
+        if (lt(lo, hi)) {
+            if (le(hi, dst))
+                return false;
+            if (lt(dst, lo))
+                set(dst, lo);
+        }
+        else if (le(hi, dst) && lt(dst, lo))
+            set(dst, lo);
+        SASSERT(!has_overflow(dst));
+        return true;
+    }
 
+    bool sls_valuation::round_down(svector<digit_t>& dst) const {
+        if (lt(lo, hi)) {
+            if (lt(lo, hi))
+                return false;
+            if (le(hi, dst)) {
+                set(dst, hi);
+                sub1(dst);
             }
-        }         
+        }
+        else if (le(hi, dst) && lt(dst, lo)) {
+            set(dst, hi);
+            sub1(dst);
+        }
+        SASSERT(!has_overflow(dst));
         return true;
     }
 
+    void sls_valuation::set_repair(bool try_down, svector<digit_t>& dst) {
+        for (unsigned i = 0; i < nw; ++i)
+            dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & bits[i]);
+        bool ok = try_down ? round_down(dst) : round_up(dst);
+        if (!ok)
+            VERIFY(try_down ? round_up(dst) : round_down(dst));
+        set(bits, dst);
+        SASSERT(!has_overflow(dst));
+    }
+
+    void sls_valuation::min_feasible(svector<digit_t>& out) const {
+        if (gt(hi, lo)) {
+            for (unsigned i = 0; i < nw; ++i)
+                out[i] = lo[i];
+        }
+        else {
+            for (unsigned i = 0; i < nw; ++i)
+                out[i] = fixed[i] & bits[i];
+        }
+        SASSERT(!has_overflow(out));
+    }
+
+    void sls_valuation::max_feasible(svector<digit_t>& out) const {
+        if (gt(hi, lo)) {        
+            for (unsigned i = 0; i < nw; ++i)
+                out[i] = hi[i];
+            sub1(out);
+        }
+        else {
+            for (unsigned i = 0; i < nw; ++i)
+                out[i] = ~fixed[i] | bits[i];
+        }
+        SASSERT(!has_overflow(out));
+    }
+
+    unsigned sls_valuation::msb(svector<digit_t> const& src) const {
+        SASSERT(!has_overflow(src));
+        for (unsigned i = nw; i-- > 0; ) 
+            if (src[i] != 0)
+                return i * 8 * sizeof(digit_t) + log2(src[i]);        
+        return bw;
+    }
+
     void sls_valuation::set_value(svector<digit_t>& bits, rational const& n) {       
         for (unsigned i = 0; i < bw; ++i) 
             set(bits, i, n.get_bit(i)); 
@@ -123,7 +264,8 @@ namespace bv {
     // 0 = (new_bits ^ bits) & fixed
     // also check that new_bits are in range
     //
-    bool sls_valuation::can_set(svector<digit_t> const& new_bits) const {        
+    bool sls_valuation::can_set(svector<digit_t> const& new_bits) const { 
+        SASSERT(!has_overflow(new_bits));
         for (unsigned i = 0; i < nw; ++i)
             if (0 != ((new_bits[i] ^ bits[i]) & fixed[i]))
                 return false;        
@@ -131,6 +273,7 @@ namespace bv {
     }
 
     unsigned sls_valuation::to_nat(svector<digit_t> const& d, unsigned max_n) {
+        SASSERT(!has_overflow(d));
         SASSERT(max_n < UINT_MAX / 2);
         unsigned p = 1;
         unsigned value = 0;
@@ -156,12 +299,129 @@ namespace bv {
         if (eq(lo, hi)) {
             set_value(lo, l);
             set_value(hi, h);
+        }
+        else {
+            rational old_lo, old_hi;
+            get_value(lo, old_lo);
+            get_value(hi, old_hi);
+            if (old_lo < old_hi) {
+                if (old_lo < l && l < old_hi)
+                    set_value(lo, l),
+                    old_lo = l;
+                if (old_hi < h && h < old_hi)
+                    set_value(hi, h);
+            }
+            else {
+                SASSERT(old_hi < old_lo);
+                if (old_lo < l || l < old_hi)
+                    set_value(lo, l),
+                    old_lo = l;
+                if (old_lo < h && h < old_hi)
+                    set_value(hi, h);
+                else if (old_hi < old_lo && (h < old_hi || old_lo < h))
+                    set_value(hi, h);
+            }
+        }    
+        SASSERT(!has_overflow(lo));
+        SASSERT(!has_overflow(hi));
+    }
+
+    void sls_valuation::init_fixed() {
+        if (eq(lo, hi))
             return;
+        bool lo_ok = true;
+        for (unsigned i = 0; i < nw; ++i)
+            lo_ok &= (0 == (fixed[i] & (bits[i] ^ lo[i])));
+        if (!lo_ok) {
+            svector<digit_t> tmp(nw + 1);
+            if (get_at_least(lo, tmp)) {
+                if (lt(lo, hi) && lt(tmp, hi))
+                    set(lo, tmp);                
+                else if (gt(lo, hi))
+                    set(lo, tmp);
+            }
+            else if (gt(lo, hi)) {
+                svector<digit_t> zero(nw + 1, (unsigned) 0);
+                if (get_at_least(zero, tmp) && lt(tmp, hi))
+                    set(lo, tmp);
+            }
+        }
+        bool hi_ok = true;
+        svector<digit_t> hi1(nw + 1, (unsigned)0);
+        svector<digit_t> one(nw + 1, (unsigned)0);
+        one[0] = 1;
+        digit_t c;
+        mpn_manager().sub(hi.data(), nw, one.data(), nw, hi1.data(), &c);
+        for (unsigned i = 0; i < nw; ++i)
+            hi_ok &= (0 == (fixed[i] & (bits[i] ^ hi1[i])));
+        if (!hi_ok) {
+            svector<digit_t> tmp(nw + 1);
+            if (get_at_most(hi1, tmp)) {
+                if (lt(tmp, hi) && (le(lo, tmp) || lt(hi, lo))) {
+                    mpn_manager().add(tmp.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c);
+                    clear_overflow_bits(hi1);
+                    set(hi, hi1);
+                }
+            }
+            // TODO other cases
+        }
+
+        // set most significant bits
+        if (lt(lo, hi)) {
+            unsigned i = bw;
+            for (; i-- > 0; ) {
+                if (get(hi, i))
+                    break;
+                if (!get(fixed, i)) {
+                    set(fixed, i, true);
+                    set(bits, i, false);
+                }
+            }
+            bool is_power_of2 = true;
+            for (unsigned j = 0; is_power_of2 && j < i; ++j)
+                is_power_of2 = !get(hi, j);            
+            if (is_power_of2) {
+                if (!get(fixed, i)) {
+                    set(fixed, i, true);
+                    set(bits, i, false);
+                }
+            }
         }
-        
-        // TODO: intersect with previous range, if any
-        set_value(lo, l);
-        set_value(hi, h);       
+        svector<digit_t> tmp(nw + 1, (unsigned)0);
+        mpn_manager().add(lo.data(), nw, one.data(), nw, tmp.data(), nw + 1, &c);
+        clear_overflow_bits(tmp);
+        if (eq(tmp, hi)) {
+            for (unsigned i = 0; i < bw; ++i) {
+                if (!get(fixed, i)) {
+                    set(fixed, i, true);
+                    set(bits, i, get(lo, i));
+                }
+            }
+        }
+        SASSERT(!has_overflow(bits));
+    }
+
+    void sls_valuation::set_sub(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const {
+        digit_t c;
+        mpn_manager().sub(a.data(), nw, b.data(), nw, out.data(), &c);
+        clear_overflow_bits(out);
+    }
+
+    bool sls_valuation::set_add(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const {
+        digit_t c;
+        mpn_manager().add(a.data(), nw, b.data(), nw, out.data(), nw + 1, &c);
+        bool ovfl = out[nw] != 0 || has_overflow(out);
+        clear_overflow_bits(out);
+        return ovfl;
+    }
+
+    bool sls_valuation::set_mul(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const {
+        mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
+        bool ovfl = has_overflow(out);
+        for (unsigned i = nw; i < 2 * nw; ++i)
+            ovfl |= out[i] != 0;
+        clear_overflow_bits(out);
+        return ovfl;
     }
 
 }
diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h
index 34ab55f611f..6a5b241b34b 100644
--- a/src/ast/sls/sls_valuation.h
+++ b/src/ast/sls/sls_valuation.h
@@ -33,7 +33,6 @@ namespace bv {
         svector<digit_t> lo,  hi;        // range assignment to bit-vector, as wrap-around interval
         svector<digit_t> bits, fixed;    // bit assignment and don't care bit
         sls_valuation(unsigned bw);
-        ~sls_valuation();
         
         unsigned num_bytes() const { return (bw + 7) / 8; }
 
@@ -41,6 +40,7 @@ namespace bv {
         void get_value(svector<digit_t> const& bits, rational& r) const;
         void get(svector<digit_t>& dst) const;
         void add_range(rational lo, rational hi);
+        void init_fixed();
         void set1(svector<digit_t>& bits);
         
         void clear_overflow_bits(svector<digit_t>& bits) const;
@@ -52,6 +52,8 @@ namespace bv {
         bool eq(svector<digit_t> const& other) const { return eq(other, bits); }
         bool eq(svector<digit_t> const& a, svector<digit_t> const& b) const;
         bool gt(svector<digit_t> const& a, svector<digit_t> const& b) const;
+        bool lt(svector<digit_t> const& a, svector<digit_t> const& b) const;
+        bool le(svector<digit_t> const& a, svector<digit_t> const& b) const;
 
         bool is_zero() const { return is_zero(bits); }
         bool is_zero(svector<digit_t> const& a) const { 
@@ -60,6 +62,29 @@ namespace bv {
                     return false; 
             return true; 
         }
+        bool is_ones() const { return is_ones(bits); }
+        bool is_ones(svector<digit_t> const& a) const {
+            auto bound = bw % (sizeof(digit_t) * 8) == 0 ? nw : nw - 1;
+            for (unsigned i = 0; i < bound; ++i)
+                if (a[i] != ~0)
+                    return false;
+            if (bound < nw) {
+                for (unsigned i = bound * sizeof(digit_t) * 8; i < bw; ++i)
+                    if (!get(a, i))
+                        return false;
+            }
+            return true;
+        }
+
+        bool is_one() const { return is_one(bits); }
+        bool is_one(svector<digit_t> const& bits) const {
+            if (1 != bits[0])
+                return false;
+            for (unsigned i = 1; i < nw; ++i)
+                if (0 != bits[i])
+                    return false;
+            return true;
+        }
 
         bool sign() const { return get(bits, bw - 1); }
 
@@ -71,14 +96,25 @@ namespace bv {
         }
 
         unsigned parity(svector<digit_t> const& bits) const {
-            unsigned i = 0;
-            for (; i < bw && !get(bits, i); ++i);
-            return i;               
+            for (unsigned i = 0; i < nw; ++i) 
+                if (bits[i] != 0)
+                    return (8 * sizeof(digit_t) * i) + trailing_zeros(bits[i]);
+            return bw;              
         }
 
-        // retrieve number at or below src which is feasible
+        void min_feasible(svector<digit_t>& out) const;
+        void max_feasible(svector<digit_t>& out) const;
+
+        // most significant bit or bw if src = 0
+        unsigned msb(svector<digit_t> const& src) const;
+
+        // retrieve largest number at or below (above) src which is feasible
         // with respect to fixed, lo, hi.
-        bool get_below(svector<digit_t> const& src, svector<digit_t>& dst);
+        bool get_at_most(svector<digit_t> const& src, svector<digit_t>& dst) const;
+        bool get_at_least(svector<digit_t> const& src, svector<digit_t>& dst) const;
+        bool round_up(svector<digit_t>& dst) const;
+        bool round_down(svector<digit_t>& dst) const;
+        void set_repair(bool try_down, svector<digit_t>& dst);
 
         bool try_set(svector<digit_t> const& src) {
             if (!can_set(src))
@@ -98,12 +134,21 @@ namespace bv {
                 bits[i] = 0;
         }
 
-
-        void set_fixed(svector<digit_t> const& src) {
-            for (unsigned i = nw; i-- > 0; )
-                fixed[i] = src[i];
+        void sub1(svector<digit_t>& out) const {
+            for (unsigned i = 0; i < bw; ++i) {
+                if (get(out, i)) {
+                    set(out, i, false);
+                    return;
+                }
+                else
+                    set(out, i, true);
+            }
         }
 
+        void set_sub(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const;
+        bool set_add(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const;
+        bool set_mul(svector<digit_t>& out, svector<digit_t> const& a, svector<digit_t> const& b) const;
+
         void set_range(svector<digit_t>& dst, unsigned lo, unsigned hi, bool b) {
             for (unsigned i = lo; i < hi; ++i)
                 set(dst, i, b);
@@ -120,6 +165,11 @@ namespace bv {
                 dst[i] = 0;
         }
 
+        void set(svector<digit_t>& dst, svector<digit_t> const& src) const {
+            for (unsigned i = 0; i < nw; ++i)
+                dst[i] = src[i];
+        }
+
         bool get(svector<digit_t> const& d, unsigned bit_idx) const {
             return (get_bit_word(d, bit_idx) & get_pos_mask(bit_idx)) != 0;
         }
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 8e9cc10ad6a..3b0fd580a77 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -84,7 +84,7 @@ namespace bv {
                 .push_back(bv.mk_ule(a, b))
                 .push_back(bv.mk_sle(a, b))
                 .push_back(bv.mk_concat(a, b))
-                .push_back(bv.mk_extract(6, 3, a))
+                .push_back(bv.mk_extract(4, 2, a))
                 .push_back(bv.mk_bvuadd_ovfl(a, b))
                 .push_back(bv.mk_bv_rotate_left(a, j))
                 .push_back(bv.mk_bv_rotate_right(a, j))
@@ -97,6 +97,7 @@ namespace bv {
     //            .push_back(bv.mk_bvsmul_ovfl(a, b))
     //            .push_back(bv.mk_bvsdiv_ovfl(a, b))
                 ;
+            return result;
         }