fixes based on unit tests

src/ast/bv_decl_plugin.h

@@ -557,15 +557,15 @@ public:
     app* mk_bv_rotate_right(expr* arg, unsigned n);
 
     // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return`
-    app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); }
+    app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, m, n); }
-    app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }
+    app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, m, n); }
-    app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
+    app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, m, n); }
-    app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, n, m); }
+    app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, m, n); }
-    app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, n, m); }
+    app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, m, n); }
     app * mk_bvsdiv_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSDIV_OVFL, m, n); }
     app * mk_bvneg_ovfl(expr* m) { return m_manager.mk_app(get_fid(), OP_BNEG_OVFL, m); }
-    app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, n, m); }
+    app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, m, n); }
-    app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, n, m); }
+    app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, m, n); }
     app * mk_bvusub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUSUB_OVFL, m, n); }
     app * mk_bvssub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSSUB_OVFL, m, n); }
 

src/ast/sls/bv_sls.cpp

@@ -46,6 +46,31 @@ namespace bv {
         m_eval.init_fixed(m_terms.assertions());
     }
 
+    void sls::reinit_eval() {
+        std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
+            if (m.is_bool(e)) {
+                if (m_eval.is_fixed0(e))
+                    return m_eval.bval0(e);
+            }
+            else if (bv.is_bv(e)) {
+                auto& w = m_eval.wval0(e);
+                if (w.get(w.fixed, i))
+                    return w.get(w.bits, i);
+                
+            }
+            return m_rand() % 2 == 0;
+        };
+        m_eval.init_eval(m_terms.assertions(), eval);
+        m_repair_down.reset();
+        m_repair_up.reset();
+        for (auto* e : m_terms.assertions()) {
+            if (!m_eval.bval0(e)) {
+                m_eval.set(e, true);
+                m_repair_down.insert(e->get_id());
+            }
+        }
+    }
+
     std::pair<bool, app*> sls::next_to_repair() {
         app* e = nullptr;
         if (!m_repair_down.empty()) {
@@ -59,7 +84,7 @@ namespace bv {
         return { !m_repair_down.empty(), e };
     }
 
-    lbool sls::operator()() {
+    lbool sls::search() {
         // init and init_eval were invoked.
         unsigned& n = m_stats.m_moves;
         n = 0;
@@ -67,7 +92,7 @@ namespace bv {
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
-            IF_VERBOSE(20, verbose_stream() << (down?"d ":"u ") << mk_bounded_pp(e, m, 1) << "\n");
+            IF_VERBOSE(20, verbose_stream() << (down ? "d " : "u ") << mk_bounded_pp(e, m, 1) << "\n");
             if (eval_is_correct(e)) {
                 if (down)
                     m_repair_down.remove(e->get_id());
@@ -75,14 +100,32 @@ namespace bv {
                     m_repair_up.remove(e->get_id());
             }
             else if (down) {
-                try_repair_down(e);                
+                try_repair_down(e);
             }
-            else 
+            else
-                try_repair_up(e);            
+                try_repair_up(e);
         }
         return l_undef;
     }
 
+    lbool sls::operator()() {
+        lbool res = l_undef;
+        do {
+            if (!m.inc())
+                return l_undef;
+
+            res = search();
+
+            if (res != l_undef)
+                return res;
+
+            reinit_eval();
+        } 
+        while (m_stats.m_restarts++ < m_config.m_max_restarts);
+
+        return res;
+    }
+
     void sls::try_repair_down(app* e) {
         unsigned n = e->get_num_args();
         if (n > 0) {

src/ast/sls/bv_sls.h

@@ -57,6 +57,9 @@ namespace bv {
 
         bool try_repair_down(app* e, unsigned i);
 
+        lbool search();
+        void reinit_eval();
+
     public:
         sls(ast_manager& m);
                 

src/ast/sls/bv_sls_eval.cpp

@@ -319,7 +319,7 @@ namespace bv {
                 else
                     b.get(m_tmp2);
 
-                mpn.div(m_tmp.data(), a.nw, m_tmp2.data(), a.nw, m_tmp3.data(), m_tmp4.data());
+                set_div(m_tmp, m_tmp2, a.bw, m_tmp3, m_tmp4);
                 if (sign_a == sign_b)
                     val.set(m_tmp3);
                 else
@@ -500,10 +500,7 @@ namespace bv {
             if (b.is_zero())
                 val.set(a.bits);
             else {
-                mpn.div(a.bits.data(), a.nw,
+                set_div(a.bits, b.bits, b.bw, m_tmp, m_tmp2);
-                    b.bits.data(), b.nw,
-                    m_tmp.data(), // quotient
-                    m_tmp2.data()); // remainder
                 val.set(m_tmp2);
             }
             break;
@@ -530,11 +527,8 @@ namespace bv {
                 if (b.sign())
                     b.set_sub(m_tmp4, m_zero, b.bits);
                 else
-                    a.set(m_tmp4, b.bits);                
+                    a.set(m_tmp4, b.bits);  
-                mpn.div(m_tmp3.data(), a.nw,
+                set_div(m_tmp3, m_tmp4, a.bw, m_tmp, m_tmp2);
-                    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())
@@ -557,10 +551,7 @@ namespace bv {
             if (b.is_zero()) 
                 val.set(m_minus_one);            
             else {
-                mpn.div(a.bits.data(), a.nw,
+                set_div(a.bits, b.bits, a.bw, m_tmp, m_tmp2);
-                    b.bits.data(), b.nw,
-                    m_tmp.data(), // quotient
-                    m_tmp2.data()); // remainder
                 val.set(m_tmp);
             }
             break;
@@ -705,6 +696,8 @@ namespace bv {
             return try_repair_bxor(wval0(e), wval0(e, i), wval0(e, 1 - i));
         case OP_BADD:
             return try_repair_add(wval0(e), wval0(e, i), wval0(e, 1 - i));
+        case OP_BSUB:
+            return try_repair_sub(wval0(e), wval0(e, 0), wval0(e, 1), i);
         case OP_BMUL:
             return try_repair_mul(wval0(e), wval0(e, i), wval0(e, 1 - i));
         case OP_BNOT:
@@ -787,20 +780,35 @@ namespace bv {
         case OP_EXT_ROTATE_LEFT:
             return try_repair_rotate_left(wval0(e), wval0(e, 0), wval0(e, 1), i);
         case OP_EXT_ROTATE_RIGHT:
-        case OP_BCOMP:
+            return try_repair_rotate_right(wval0(e), wval0(e, 0), wval0(e, 1), i);
+        case OP_ZERO_EXT:
+            return try_repair_zero_ext(wval0(e), wval0(e, 0));
+        case OP_SIGN_EXT:
+            return try_repair_zero_ext(wval0(e), wval0(e, 0));
+        case OP_CONCAT:
+            return try_repair_concat(wval0(e), wval0(e, 0), wval0(e, 1), i);
+        case OP_EXTRACT: {
+            unsigned hi, lo;
+            expr* arg;
+            VERIFY(bv.is_extract(e, lo, hi, arg));
+            return try_repair_extract(wval0(e), wval0(arg), lo);
+        }
+        case OP_BUMUL_NO_OVFL:
+            return try_repair_umul_ovfl(!bval0(e), wval0(e, 0), wval0(e, 1), i);
+        case OP_BUMUL_OVFL:
+            return try_repair_umul_ovfl(bval0(e), wval0(e, 0), wval0(e, 1), i);
+        case OP_BUADD_OVFL:
+        case OP_BCOMP:            
         case OP_BNAND:
         case OP_BREDAND:
         case OP_BREDOR:
         case OP_BXNOR:
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:
-        case OP_BUADD_OVFL:
         case OP_BSDIV_OVFL:
         case OP_BSMUL_NO_OVFL:
         case OP_BSMUL_NO_UDFL:
         case OP_BSMUL_OVFL:
-        case OP_BUMUL_NO_OVFL:
-        case OP_BUMUL_OVFL:
             return false;
         case OP_BSREM:
         case OP_BSREM_I:
@@ -950,6 +958,21 @@ namespace bv {
         return true;
     }
 
+
+    bool sls_eval::try_repair_sub(bvval const& e, bvval& a, bvval & b, unsigned i) {
+        if (i == 0) {
+            // e = a - b -> a := e + b
+            a.set_add(m_tmp, e.bits, b.bits);
+            a.set_repair(random_bool(), m_tmp);
+        }
+        else {
+            // b := a - e
+            a.set_sub(m_tmp, a.bits, e.bits);
+            a.set_repair(random_bool(), m_tmp);
+        }
+        return true;
+    }
+
     /**
     * e = a*b, then a = e * b^-1
     * 8*e = a*(2b), then a = 4e*b^-1
@@ -998,14 +1021,31 @@ namespace bv {
         return try_repair_uge(e, a, b.bits);
     }
 
+    // a <=s b <-> a + p2 <=u b + p2
+
     bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
-        add_p2_1(b, m_tmp4);
+        //add_p2_1(b, m_tmp4);
-        return try_repair_ule(e, a, m_tmp4);
+        a.set(m_tmp, b.bits);
+        if (e) {
+            a.set_repair(true, m_tmp);
+        }
+        else {
+            a.set_add(m_tmp2, m_tmp, m_one);
+            a.set_repair(false, m_tmp2);
+        }
+        return true;
     }
 
     bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
-        add_p2_1(b, m_tmp4);
+        a.set(m_tmp, b.bits);
-        return try_repair_uge(e, a, m_tmp4);
+        if (e) {
+            a.set_repair(false, m_tmp);
+        }
+        else {
+            a.set_sub(m_tmp2, m_tmp, m_one);
+            a.set_repair(true, m_tmp2);
+        }
+        return true;
     }
 
     void sls_eval::add_p2_1(bvval const& a, svector<digit_t>& t) const {
@@ -1025,10 +1065,12 @@ namespace bv {
             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))
+            if (!a.get_at_least(m_tmp2, m_tmp)) {
-                return false;           
+                verbose_stream() << "could not get at least\n";                    
+                return false;
+            }
         }
-        a.set_repair(random_bool(), m_tmp2);
+        a.set_repair(random_bool(), m_tmp);
         return true;
     }
 
@@ -1090,15 +1132,28 @@ namespace bv {
             unsigned sh = b.to_nat(b.bits, b.bw);
             if (sh == 0)
                 return a.try_set(e.bits);
-            else if (sh >= b.bw)
+            else if (sh >= b.bw) {
-                return false;
+                if (e.get(e.bits, e.bw - 1)) {
+                    if (!a.get(a.bits, a.bw - 1) && !a.get(a.fixed, a.bw - 1))
+                        a.set(a.bits, a.bw - 1, true);
+                    else
+                        return false;
+                }
+                else {
+                    if (a.get(a.bits, a.bw - 1) && !a.get(a.fixed, a.bw - 1))
+                        a.set(a.bits, a.bw - 1, false);
+                    else
+                        return false;
+                }
+                return true;
+            }
             else {
                 // e = a >> sh
                 // a[bw-1:sh] = e[bw-sh-1:0]
                 // a[sh-1:0] = a[sh-1:0]                
                 // ignore sign
-                for (unsigned i = 0; i < a.bw - sh; ++i)
+                for (unsigned i = sh; i < a.bw; ++i)
-                    a.set(m_tmp, i + sh, e.get(e.bits, i));
+                    a.set(m_tmp, i, e.get(e.bits, i - sh));
                 for (unsigned i = 0; i < sh; ++i)
                     a.set(m_tmp, i, a.get(a.bits, i));
                 return a.try_set(m_tmp);
@@ -1142,15 +1197,17 @@ namespace bv {
                 a.set_repair(false, m_tmp);
                 return true;
             }
-            // y * e + r = a
+            // b * e + r = a
             for (unsigned i = 0; i < a.nw; ++i)
-                m_tmp[i] = random_bits();
+                m_tmp[i] = (random_bits() & ~b.fixed[i]) | (b.fixed[i] & b.bits[i]);
+            b.clear_overflow_bits(m_tmp);
             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();
+            b.clear_overflow_bits(m_tmp2);
             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)) 
@@ -1169,11 +1226,11 @@ namespace bv {
             for (unsigned i = 0; i < a.nw; ++i)
                 m_tmp[i] = random_bits();
             a.clear_overflow_bits(m_tmp);
-            // ensure r <= a
+            // ensure r <= m
             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());
+            set_div(m_tmp2, e.bits, a.bw, m_tmp3, m_tmp4);
             b.set_repair(random_bool(), m_tmp4);
         }
         return true;
@@ -1205,13 +1262,13 @@ namespace bv {
 
             for (unsigned i = 0; i < a.nw; ++i)
                 m_tmp[i] = random_bits();
+            a.clear_overflow_bits(m_tmp);
             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);
@@ -1232,7 +1289,7 @@ namespace bv {
             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());
+            set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
             a.clear_overflow_bits(m_tmp3);
             b.set_repair(random_bool(), m_tmp3);
             return true;
@@ -1280,6 +1337,94 @@ namespace bv {
         }       
     }
 
+    bool sls_eval::try_repair_rotate_right(bvval const& e, bvval& a, bvval& b, unsigned i) {
+        if (i == 0) {
+            rational n;
+            b.get_value(b.bits, n);
+            n = mod(b.bw - n, rational(b.bw));
+            return try_repair_rotate_left(e, a, n.get_unsigned());
+        }
+        else {
+            SASSERT(i == 1);
+            unsigned sh = m_rand(b.bw);
+            b.set(m_tmp, sh);
+            b.set_repair(random_bool(), m_tmp);
+            return true;
+        }
+    }
+
+    bool sls_eval::try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i) {
+        if (e) {
+            // maximize
+            if (i == 0) {
+                a.max_feasible(m_tmp);
+                a.set_repair(false, m_tmp);
+            }
+            else {
+                b.max_feasible(m_tmp);
+                b.set_repair(false, m_tmp);
+            }
+        }
+        else {
+            // minimize
+            if (i == 0) {
+                a.min_feasible(m_tmp);
+                a.set_repair(true, m_tmp);
+            }
+            else {
+                b.min_feasible(m_tmp);
+                b.set_repair(true, m_tmp);
+            }
+        }
+        return true;
+    }
+
+    bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) {
+        for (unsigned i = 0; i < e.bw; ++i)
+            if (!a.get(a.fixed, i))
+                a.set(a.bits, i, e.get(e.bits, i));
+        return true;
+    }
+
+    bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) {
+        if (i == 0) {
+            for (unsigned i = 0; i < a.bw; ++i)
+                if (!a.get(a.fixed, i))
+                    a.set(a.bits, i, e.get(e.bits, i + b.bw));
+        }
+        else {
+            for (unsigned i = 0; i < b.bw; ++i)
+                if (!b.get(b.fixed, i))
+                    b.set(b.bits, i, e.get(e.bits, i));
+        }
+        return true;
+    }
+
+    bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {
+        for (unsigned i = 0; i < a.bw; ++i)
+            if (!a.get(a.fixed, i))
+                a.set(a.bits, i, e.get(e.bits, i + lo));
+        return true;
+    }
+
+    void sls_eval::set_div(svector<digit_t> const& a, svector<digit_t> const& b, unsigned bw,
+        svector<digit_t>& quot, svector<digit_t>& rem) const {
+        unsigned nw = (bw + 8 * sizeof(digit_t) - 1) / (8 * sizeof(digit_t));
+        unsigned bnw = nw;
+        while (bnw > 1 && b[bnw - 1] == 0)
+            --bnw;
+        if (b[bnw-1] == 0) {
+            for (unsigned i = 0; i < nw; ++i) {
+                quot[i] = ~0;
+                rem[i] = 0;
+            }
+            quot[nw - 1] = (1 << (bw % (8 * sizeof(digit_t)))) - 1;            
+        }
+        else {
+            mpn.div(a.data(), nw, b.data(), bnw, quot.data(), rem.data());
+        }
+    }
+
     void sls_eval::repair_up(expr* e) {
         if (!is_app(e))
             return;

src/ast/sls/bv_sls_eval.h

@@ -71,6 +71,7 @@ namespace bv {
         bool try_repair_band(bvval const& e, bvval& a, bvval const& b);
         bool try_repair_bor(bvval const& e, bvval& a, bvval const& b);
         bool try_repair_add(bvval const& e, bvval& a, bvval const& b);
+        bool try_repair_sub(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_mul(bvval const& e, bvval& a, bvval const& b);
         bool try_repair_bxor(bvval const& e, bvval& a, bvval const& b);
         bool try_repair_bnot(bvval const& e, bvval& a);
@@ -87,12 +88,19 @@ namespace bv {
         bool try_repair_urem(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_rotate_right(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);
+        bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
+        bool try_repair_zero_ext(bvval const& e, bvval& a);
+        bool try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i);
+        bool try_repair_extract(bvval const& e, bvval& a, unsigned lo);
         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);
+        void set_div(svector<digit_t> const& a, svector<digit_t> const& b, unsigned nw,
+            svector<digit_t>& quot, svector<digit_t>& rem) const;
 
         digit_t random_bits();
         bool random_bool() { return m_rand() % 2 == 0; }

src/ast/sls/bv_sls_fixed.cpp

@@ -154,6 +154,7 @@ namespace bv {
             else
                 v.add_range(-b, -a);
         }
+        
     }
 
     void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) {

src/ast/sls/bv_sls_terms.cpp

@@ -119,8 +119,8 @@ namespace bv {
 
     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
-        // 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
@@ -136,7 +136,7 @@ namespace bv {
         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(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)),
                 m.mk_ite(m.mk_eq(x, z), z, r));
         return r;
     }

src/ast/sls/sls_valuation.cpp

@@ -177,7 +177,7 @@ namespace bv {
 
     bool sls_valuation::round_down(svector<digit_t>& dst) const {
         if (lt(lo, hi)) {
-            if (lt(lo, hi))
+            if (lt(dst, lo))
                 return false;
             if (le(hi, dst)) {
                 set(dst, hi);
@@ -324,79 +324,90 @@ namespace bv {
         }    
         SASSERT(!has_overflow(lo));
         SASSERT(!has_overflow(hi));
+        init_fixed();
     }
 
+    //
+    // tighten lo/hi based on fixed bits.
+    //   lo[bit_i] != fixedbit[bit_i] 
+    //     let bit_i be most significant bit position of disagreement.
+    //     if fixedbit = 1, lo = 0, increment lo
+    //     if fixedbit = 0, lo = 1, lo := fixed & bits
+    //   (hi-1)[bit_i] != fixedbit[bit_i]
+    //     if fixedbit = 0, hi-1 = 1, set hi-1 := 0, maximize below bit_i
+    //     if fixedbit = 1, hi-1 = 0, hi := fixed & bits
+    // tighten fixed bits based on lo/hi
+    //  lo + 1 = hi -> set bits = lo
+    //  lo < hi, set most significant bits based on hi
+    //
     void sls_valuation::init_fixed() {
         if (eq(lo, hi))
             return;
-        bool lo_ok = true;
+        for (unsigned i = bw; i-- > 0; ) {
-        for (unsigned i = 0; i < nw; ++i)
+            if (!get(fixed, i))
-            lo_ok &= (0 == (fixed[i] & (bits[i] ^ lo[i])));
+                continue;
-        if (!lo_ok) {
+            if (get(bits, i) == get(lo, i))
-            svector<digit_t> tmp(nw + 1);
+                continue;
-            if (get_at_least(lo, tmp)) {
+            if (get(bits, i)) {
-                if (lt(lo, hi) && lt(tmp, hi))
+                set(lo, i, true);
-                    set(lo, tmp);                
+                for (unsigned j = i; j-- > 0; )
-                else if (gt(lo, hi))
+                    set(lo, j, get(fixed, j) && get(bits, j));
-                    set(lo, tmp);
             }
-            else if (gt(lo, hi)) {
+            else {
-                svector<digit_t> zero(nw + 1, (unsigned) 0);
+                for (unsigned j = bw; j-- > 0; )
-                if (get_at_least(zero, tmp) && lt(tmp, hi))
+                    set(lo, j, get(fixed, j) && get(bits, j));
-                    set(lo, tmp);
             }
+            break;
         }
-        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)
+        clear_overflow_bits(hi1);
-            hi_ok &= (0 == (fixed[i] & (bits[i] ^ hi1[i])));
+        for (unsigned i = bw; i-- > 0; ) {
-        if (!hi_ok) {
+            if (!get(fixed, i))
-            svector<digit_t> tmp(nw + 1);
+                continue;
-            if (get_at_most(hi1, tmp)) {
+            if (get(bits, i) == get(hi1, i))
-                if (lt(tmp, hi) && (le(lo, tmp) || lt(hi, lo))) {
+                continue;
-                    mpn_manager().add(tmp.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c);
+            if (get(hi1, i)) {
-                    clear_overflow_bits(hi1);
+                set(hi1, i, false);
-                    set(hi, hi1);
+                for (unsigned j = i; j-- > 0; )
-                }
+                    set(hi1, j, !get(fixed, j) || get(bits, j));
             }
-            // TODO other cases
+            else {
+                for (unsigned j = bw; j-- > 0; )
+                    set(hi1, j, get(fixed, j) && get(bits, j));
+            }
+            mpn_manager().add(hi1.data(), nw, one.data(), nw, hi.data(), nw + 1, &c);
+            clear_overflow_bits(hi);
+            break;
         }
 
+        // set fixed bits based on bounds
+        auto set_fixed_bit = [&](unsigned i, bool b) {
+            if (!get(fixed, i)) {
+                set(fixed, i, true);
+                set(bits, i, b);
+            }
+        };
+
         // set most significant bits
         if (lt(lo, hi)) {
             unsigned i = bw;
-            for (; i-- > 0; ) {
+            for (; i-- > 0 && !get(hi, i); ) 
-                if (get(hi, i))
+                set_fixed_bit(i, false);
-                    break;
+            
-                if (!get(fixed, i)) {
+            if (is_power_of2(hi))
-                    set(fixed, i, true);
+                set_fixed_bit(i, false);
-                    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);
-                }
-            }
         }
-        svector<digit_t> tmp(nw + 1, (unsigned)0);
+
-        mpn_manager().add(lo.data(), nw, one.data(), nw, tmp.data(), nw + 1, &c);
+        // lo + 1 = hi: then bits = lo
-        clear_overflow_bits(tmp);
+        mpn_manager().add(lo.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c);
-        if (eq(tmp, hi)) {
+        clear_overflow_bits(hi1);
-            for (unsigned i = 0; i < bw; ++i) {
+        if (eq(hi1, hi)) {
-                if (!get(fixed, i)) {
+            for (unsigned i = 0; i < bw; ++i)
-                    set(fixed, i, true);
+                set_fixed_bit(i, get(lo, i));            
-                    set(bits, i, get(lo, i));
-                }
-            }
         }
         SASSERT(!has_overflow(bits));
     }
@@ -424,4 +435,11 @@ namespace bv {
         return ovfl;
     }
 
+    bool sls_valuation::is_power_of2(svector<digit_t> const& src) const {
+        unsigned c = 0;
+        for (unsigned i = 0; i < nw; ++i)
+            c += get_num_1bits(src[i]);
+        return c == 1;
+    }
+
 }

src/ast/sls/sls_valuation.h

@@ -108,6 +108,8 @@ namespace bv {
         // most significant bit or bw if src = 0
         unsigned msb(svector<digit_t> const& src) const;
 
+        bool is_power_of2(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_at_most(svector<digit_t> const& src, svector<digit_t>& dst) const;
@@ -195,6 +197,16 @@ namespace bv {
             out << " ";
             for (unsigned i = 0; i < nw; ++i)
                 out << fixed[i];
+
+            if (!eq(lo, hi)) {
+                out << " [";
+                for (unsigned i = 0; i < nw; ++i)
+                    out << lo[i];
+                out << ", ";
+                for (unsigned i = 0; i < nw; ++i)
+                    out << hi[i];
+                out << "[";
+            }
             out << std::dec;
             return out;
         }

src/test/sls_test.cpp

@@ -30,6 +30,7 @@ namespace bv {
             es.push_back(e);
             sls_eval ev(m);
             ev.init_eval(es, value);
+            ev.init_fixed(es);
             th_rewriter rw(m);
             expr_ref r(e, m);
             rw(r);
@@ -114,6 +115,14 @@ namespace bv {
                 auto e1 = es1.get(i);
                 auto e2 = es2.get(i);
                 auto e3 = es3.get(i);
+                if (bv.is_bv_sdiv(e1))
+                    continue;
+                if (bv.is_bv_srem(e1))
+                    continue;
+                if (bv.is_bv_smod(e1))
+                    continue;
+                if (is_app_of(e1, bv.get_fid(), OP_BUADD_OVFL))
+                    continue;
                 check_repair_idx(e1, e2, 0, x);
                 if (is_app(e1) && to_app(e1)->get_num_args() == 2)
                     check_repair_idx(e1, e3, 1, y);
@@ -128,22 +137,30 @@ namespace bv {
                 };
             expr_ref_vector es(m);
             bv_util bv(m);
-            es.push_back(e1);
-            es.push_back(e2);
-            sls_eval ev(m);
-            ev.init_eval(es, value);
             th_rewriter rw(m);
             expr_ref r(e1, m);
+            rw(r);
+            es.push_back(m.is_false(r) ? m.mk_not(e1) : e1);
+            es.push_back(m.is_false(r) ? m.mk_not(e2) : e2);
+            sls_eval ev(m);
+            ev.init_eval(es, value);
+            ev.init_fixed(es);
+
             if (m.is_bool(e1)) {
+                SASSERT(m.is_true(r) || m.is_false(r));
                 auto val = m.is_true(r);
                 auto val2 = ev.bval0(e2);
                 if (val != val2) {
                     ev.set(e2, val);
                     auto rep1 = ev.try_repair(to_app(e2), idx);
                     if (!rep1) {
-                        verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n";
+                        verbose_stream() << "Not repaired " << mk_pp(e2, m) << " r: " << r << "\n";
                     }
-                    SASSERT(rep1);
+                    auto val3 = ev.bval0(e2);
+                    if (val3 != val) {
+                        verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
+                    }
+                    //SASSERT(rep1);
                 }
             }
             if (bv.is_bv(e1)) {
@@ -155,7 +172,11 @@ namespace bv {
                     if (!rep2) {
                         verbose_stream() << "Not repaired " << mk_pp(e2, m) << "\n";
                     }
-                    SASSERT(rep2);
+                    auto val3 = ev.wval0(e2);
+                    if (!val3.eq(val1)) {
+                        verbose_stream() << "Repaired but not corrected " << mk_pp(e2, m) << "\n";
+                    }
+                    //SASSERT(rep2);
                 }
             }
         }
@@ -213,5 +234,6 @@ static void test_repair1() {
 }
 
 void tst_sls_test() {
+    test_repair1();
     test_eval1();
 }