diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index a53ba90c1..295ef6443 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -241,7 +241,7 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
         return BR_FAILED;
     }
 
-    CTRACE("bv", st != BR_FAILED, tout << mk_pp(f, m) << "\n";
+    CTRACE("bv_verbose", st != BR_FAILED, tout << mk_pp(f, m) << "\n";
            for (unsigned i = 0; i < num_args; ++i)
                tout << " " << mk_bounded_pp(args[i], m) << "\n";
            tout << mk_bounded_pp(result, m, 3) << "\n");
diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp
index 37e36e609..80681d718 100644
--- a/src/ast/sls/sls_array_plugin.cpp
+++ b/src/ast/sls/sls_array_plugin.cpp
@@ -82,11 +82,16 @@ namespace sls {
         for (auto p : euf::enode_parents(n->get_root()))
             if (a.is_select(p->get_expr()))
                 add_map_axiom(g, n, p);       
+        for (auto arg : euf::enode_args(n)) {
+            SASSERT(a.is_array(arg->get_expr()));
+            for (auto p : euf::enode_parents(arg->get_root()))
+                if (a.is_select(p->get_expr()))
+                    add_map_axiom(g, n, p);
+        }
     }
 
     void array_plugin::add_map_axiom(euf::egraph& g, euf::enode * n, euf::enode* sel) {
         func_decl* f = nullptr;
-        VERIFY(sel->get_arg(0)->get_root() == n->get_root());
         SASSERT(a.is_map(n->get_expr()));
         VERIFY(a.is_map(n->get_decl(), f));
         expr_ref apply_map(m);
@@ -101,7 +106,9 @@ namespace sls {
         auto nsel = mk_select(g, n, sel);
         auto nmap = g.find(f_map);
         if (!nmap) 
-            nmap = g.mk(f_map, 0, eargs.size(), eargs.data());        
+            nmap = g.mk(f_map, 0, eargs.size(), eargs.data()); 
+        if (nmap->get_root() == nsel->get_root())
+            return;
         if (are_distinct(nsel, nmap)) {
             expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m);
             ctx.add_clause(eq);
diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index a78dba875..f9d1bca70 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -94,7 +94,7 @@ namespace sls {
 
     void bv_eval::init_eval_bv(app* e) {
         if (bv.is_bv(e)) 
-            eval(e).commit_eval();               
+            eval(e).commit_eval_check_tabu();               
     }
     
     bool bv_eval::can_eval1(app* e) const {
@@ -938,7 +938,7 @@ namespace sls {
 
     bool bv_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
-            m_tmp[i] = ~a.fixed[i] & (e[i] | (~b.bits()[i] & random_bits()));
+            m_tmp[i] = ~a.fixed(i) & (e[i] | (~b.bits()[i] & random_bits()));
         return a.set_repair(random_bool(), m_tmp);
     }
 
@@ -952,7 +952,7 @@ namespace sls {
 
         bvval& a = wval(t, i);
         for (unsigned j = 0; j < a.nw; ++j) 
-            m_tmp[j] = ~a.fixed[j] & (e[j] | (~m_tmp2[j] & random_bits()));
+            m_tmp[j] = ~a.fixed(j) & (e[j] | (~m_tmp2[j] & random_bits()));
 
         return a.set_repair(random_bool(), m_tmp);
     }
@@ -1453,13 +1453,13 @@ namespace sls {
         if (msb > a.msb(t)) {
             unsigned num_flex = 0;
             for (unsigned i = e.bw; i-- >= msb;) 
-                if (!a.fixed.get(i))
+                if (!a.fixed().get(i))
                     ++num_flex;
             if (num_flex == 0)
                 return false;
             unsigned n = m_rand(num_flex);
             for (unsigned i = e.bw; i-- >= msb;) {
-                if (!a.fixed.get(i)) {
+                if (!a.fixed().get(i)) {
                     if (n == 0) {
                         t.set(i, true);
                         break;
@@ -1519,7 +1519,7 @@ namespace sls {
         else {
             for (unsigned i = 0; i < 4; ++i) {
                 for (unsigned i = a.bw; !(t <= clze) && i-- > 0; )
-                    if (!b.fixed.get(i))
+                    if (!b.fixed().get(i))
                         t.set(i, false);
                 if (t <= clze && b.set_repair(random_bool(), t))
                     return true;                
@@ -1654,13 +1654,13 @@ namespace sls {
 
     bool bv_eval::try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
         if (i == 0) {
-            if (a.is_zero(e) && a.is_ones(a.fixed) && a.is_ones())
+            if (a.is_zero(e) && a.is_ones(a.fixed()) && a.is_ones())
                 return false;            
             if (b.is_zero()) 
                 return false;            
             if (!a.is_ones(e)) {
                 for (unsigned i = 0; i < a.nw; ++i)
-                    m_tmp[i] = ~a.fixed[i] | a.bits()[i];
+                    m_tmp[i] = ~a.fixed()[i] | a.bits()[i];
                 a.clear_overflow_bits(m_tmp);
                 if (e > m_tmp)
                     return false;
@@ -1765,14 +1765,14 @@ namespace sls {
     bool bv_eval::add_overflow_on_fixed(bvval const& a, bvect 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];
+            m_tmp3[i] = a.fixed(i) & a.bits(i);
         return a.set_add(m_tmp4, t, m_tmp3);
     }
 
     bool bv_eval::mul_overflow_on_fixed(bvval const& a, bvect 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];
+            m_tmp3[i] = a.fixed(i) & a.bits(i);
         return a.set_mul(m_tmp4, m_tmp3, t);
     }
 
@@ -1976,10 +1976,10 @@ namespace sls {
             return true;
 
         for (unsigned i = 0; i < v.nw; ++i) 
-            if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) 
+            if (0 != (v.fixed(i) & (v.bits(i) ^ v.eval[i]))) 
                 return false;
 
-        if (!v.commit_eval())
+        if (!v.commit_eval_check_tabu())
             return false;
 
         ctx.new_value_eh(e);
@@ -1995,15 +1995,14 @@ namespace sls {
     void bv_eval::commit_eval(expr* p, app* e) {
         if (!bv.is_bv(e))
             return;
-        SASSERT(wval(e).commit_eval());
-        VERIFY(wval(e).commit_eval());
+        VERIFY(wval(e).commit_eval_check_tabu());
     }
 
     void bv_eval::set_random(app* e) {
         if (bv.is_bv(e)) {
             auto& v = wval(e);
             if (v.set_random(m_rand))
-                VERIFY(v.commit_eval());
+                VERIFY(v.commit_eval_check_tabu());
         }
     }
 
diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h
index b9729f196..aaf847472 100644
--- a/src/ast/sls/sls_bv_eval.h
+++ b/src/ast/sls/sls_bv_eval.h
@@ -51,7 +51,7 @@ namespace sls {
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;
-        bool_vector         m_fixed;
+        bool_vector         m_is_fixed;
         unsigned            m_lookahead_steps = 0;
         unsigned            m_lookahead_phase_size = 10;
         
@@ -170,7 +170,7 @@ namespace sls {
 
         void set(expr* e, sls::bv_valuation const& val);
 
-        bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
+        bool is_fixed0(expr* e) const { return m_is_fixed.get(e->get_id(), false); }
         
         sls::bv_valuation& eval(app* e) const;
 
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index 96e9e1579..b2d9f639e 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -8,7 +8,7 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2024-02-07
-    
+
 --*/
 
 #include "ast/ast_pp.h"
@@ -19,15 +19,18 @@ Author:
 
 namespace sls {
 
-    bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx):
+    bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx) :
         ev(ev),
         terms(terms),
         m(ev.m),
         bv(ev.bv),
         ctx(ctx)
-    {}
+    {
+    }
 
-    void bv_fixed::init() {  
+    void bv_fixed::init() {
+
+        return;
 
         for (auto e : ctx.subterms())
             set_fixed(e);
@@ -40,12 +43,12 @@ namespace sls {
                 continue;
             if (is_app(a))
                 init_range(to_app(a), lit.sign());
-            ev.m_fixed.setx(a->get_id(), true, false);
+            ev.m_is_fixed.setx(a->get_id(), true, false);
         }
         //ctx.display(verbose_stream());
 
         for (auto e : ctx.subterms())
-            propagate_range_up(e);  
+            propagate_range_up(e);
 
         //ctx.display(verbose_stream());
     }
@@ -64,24 +67,24 @@ namespace sls {
                 auto p = rational::power_of_two(bv.get_bv_size(s));
                 add_range(e, valt.lo() * p, valt.hi() * p, false);
             }
-        }        
+        }
         else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) {
             auto& val = ev.wval(t);
-            if (val.lo() != val.hi()) 
-                add_range(e, v + val.lo(), v + val.hi(), false);  
+            if (val.lo() != val.hi())
+                add_range(e, v + val.lo(), v + val.hi(), false);
         }
         else if (bv.is_bv_add(e, t, s) && bv.is_numeral(s, v)) {
             auto& val = ev.wval(t);
-            if (val.lo() != val.hi()) 
-                add_range(e, v + val.lo(), v + val.hi(), false);          
+            if (val.lo() != val.hi())
+                add_range(e, v + val.lo(), v + val.hi(), false);
         }
         // x in [1, 4[   => -x in [-3, 0[
         // x in [lo, hi[ => -x in [-hi + 1, -lo + 1[
-        else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) && 
+        else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) &&
             v + 1 == rational::power_of_two(bv.get_bv_size(e))) {
             auto& val = ev.wval(t);
             if (val.lo() != val.hi())
-                add_range(e, -val.hi() + 1, - val.lo() + 1, false);
+                add_range(e, -val.hi() + 1, -val.lo() + 1, false);
         }
     }
 
@@ -94,7 +97,7 @@ namespace sls {
         auto N = [&](expr* s) {
             auto b = bv.get_bv_size(s);
             return b > 0 ? rational::power_of_two(b - 1) : rational(0);
-        };
+            };
         if (bv.is_ule(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
@@ -104,22 +107,22 @@ namespace sls {
             get_offset(s, x, a);
             get_offset(t, y, b);
             return init_range(y, b, x, a, !sign);
-        }            
+        }
         else if (bv.is_uge(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
             return init_range(y, b, x, a, sign);
-        }            
+        }
         else if (bv.is_ugt(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
             return init_range(x, a, y, b, !sign);
-        }            
+        }
         else if (bv.is_sle(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
             return init_range(x, a + N(s), y, b + N(s), sign);
-        }            
+        }
         else if (bv.is_slt(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
@@ -147,7 +150,7 @@ namespace sls {
         else if (bv.is_bit2bool(e, s, idx)) {
             auto& val = ev.wval(s);
             val.try_set_bit(idx, !sign);
-            val.fixed.set(idx, true);
+            val.set_fixed_bit(idx, !sign);
             val.tighten_range();
             return true;
         }
@@ -155,10 +158,10 @@ namespace sls {
         return false;
     }
 
-    bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {     
+    bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {
         unsigned lo, hi;
         rational b(0);
-        expr* s = nullptr;        
+        expr* s = nullptr;
         if (sign && true)
             // 1 <= t - a
             init_range(nullptr, rational(1), t, -a, false);
@@ -185,19 +188,19 @@ namespace sls {
             if (hi == lo) {
                 auto sign1 = sign ? a == 1 : a == 0;
                 auto& val = ev.wval(s);
-                if (val.try_set_bit(lo, !sign1)) 
-                    val.fixed.set(lo, true);
-
+                val.try_set_bit(lo, !sign1);
+                val.set_fixed_bit(lo, !sign1);
                 val.tighten_range();
 
             }
             else if (!sign) {
                 auto& val = ev.wval(s);
-                for (unsigned i = lo; i <= hi; ++i) 
-                    if (val.try_set_bit(i, a.get_bit(i - lo)))
-                        val.fixed.set(i, true);                
+                for (unsigned i = lo; i <= hi; ++i) {
+                    val.try_set_bit(i, a.get_bit(i - lo));
+                    val.set_fixed_bit(i, a.get_bit(i - lo));
+                }
                 val.tighten_range();
-            }            
+            }
 
             if (!sign && hi + 1 == bv.get_bv_size(s)) {
                 // s < 2^lo * (a + 1) 
@@ -223,11 +226,11 @@ namespace sls {
     bool bv_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
         if (!x && !y)
             return false;
-        if (!x) 
+        if (!x)
             return add_range(y, a - b, -b, sign);
-        else if (!y) 
-            return add_range(x, -a, b - a + 1, sign);        
-        else if (x == y) 
+        else if (!y)
+            return add_range(x, -a, b - a + 1, sign);
+        else if (x == y)
             return add_range(x, -a, -b, sign);
         return false;
     }
@@ -240,6 +243,7 @@ namespace sls {
             return false;
         if (sign)
             std::swap(lo, hi);
+        rational r;
         v.add_range(lo, hi);
         expr* x, * y;
         if (v.lo() == 0 && bv.is_concat(e, x, y)) {
@@ -256,6 +260,15 @@ namespace sls {
                 add_range(x, lo, hi, false);
             }
         }
+        else if (bv.is_bv_mul(e, x, y) &&
+            hi != lo &&
+            bv.is_numeral(x, r) &&
+            r + 1 == rational::power_of_two(bv.get_bv_size(e))) {
+            add_range(y, 1 - hi, 1 - lo, false);
+        }
+        else if (bv.is_bv_add(e, x, y) && bv.is_numeral(x, r)) {
+            add_range(y, lo - r, hi - r, false);
+        }
         return true;
     }
 
@@ -287,19 +300,19 @@ namespace sls {
             return false;
         return all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); });
     }
-    
+
     void bv_fixed::set_fixed(expr* _e) {
         if (!is_app(_e))
             return;
         auto e = to_app(_e);
-        
+
         if (e->get_family_id() == bv.get_family_id() && all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) {
-            if (bv.is_bv(e)) {    
+            if (bv.is_bv(e)) {
                 auto& v = ev.wval(e);
                 for (unsigned i = 0; i < v.bw; ++i)
-                    v.fixed.set(i, true);
+                    v.set_fixed_bit(i, v.bits().get(i));
             }
-            ev.m_fixed.setx(e->get_id(), true, false);
+            ev.m_is_fixed.setx(e->get_id(), true, false);
             return;
         }
 
@@ -310,9 +323,11 @@ namespace sls {
         if (m.is_ite(e)) {
             auto& val_th = ev.wval(e->get_arg(1));
             auto& val_el = ev.wval(e->get_arg(2));
-            for (unsigned i = 0; i < v.nw; ++i)
-                v.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i));
-            return;
+            for (unsigned i = 0; i < v.nw; ++i) {
+                auto mask = val_el.fixed(i) & val_th.fixed(i) & ~(val_el.bits(i) ^ val_th.bits(i));
+                v.set_fixed_word(i, mask, v.bits(i));
+                return;
+            }
         }
 
         if (e->get_family_id() != bv.get_fid())
@@ -323,8 +338,10 @@ namespace sls {
                 auto& a = ev.wval(e->get_arg(0));
                 auto& b = ev.wval(e->get_arg(1));
                 // (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits)
-                for (unsigned i = 0; i < a.nw; ++i)
-                    v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i));
+                for (unsigned i = 0; i < a.nw; ++i) {
+                    auto mask = (a.fixed(i) & b.fixed(i)) | (a.fixed(i) & ~a.bits(i)) | (b.fixed(i) & ~b.bits(i));
+                    v.set_fixed_word(i, mask, v.bits(i));
+                }
             }
             break;
         }
@@ -333,8 +350,10 @@ namespace sls {
                 auto& a = ev.wval(e->get_arg(0));
                 auto& b = ev.wval(e->get_arg(1));
                 // (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits)
-                for (unsigned i = 0; i < a.nw; ++i)
-                    v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i));
+                for (unsigned i = 0; i < a.nw; ++i) {
+                    auto mask = (a.fixed(i) & b.fixed(i)) | (a.fixed(i) & a.bits(i)) | (b.fixed(i) & b.bits(i));
+                    v.set_fixed_word(i, mask, v.bits(i));
+                }
             }
             break;
         }
@@ -343,14 +362,14 @@ namespace sls {
                 auto& a = ev.wval(e->get_arg(0));
                 auto& b = ev.wval(e->get_arg(1));
                 for (unsigned i = 0; i < a.nw; ++i)
-                    v.fixed[i] = a.fixed[i] & b.fixed[i];
+                    v.set_fixed_word(i, a.fixed(i) & b.fixed(i), v.bits(i));
             }
             break;
         }
         case OP_BNOT: {
             auto& a = ev.wval(e->get_arg(0));
             for (unsigned i = 0; i < a.nw; ++i)
-                v.fixed[i] = a.fixed[i];
+                v.set_fixed_word(i, a.fixed(i), v.bits(i));
             break;
         }
         case OP_BADD: {
@@ -358,9 +377,10 @@ namespace sls {
             for (unsigned i = 0; i < v.bw; ++i) {
                 for (unsigned j = 0; pfixed && j < e->get_num_args(); ++j) {
                     auto& a = ev.wval(e->get_arg(j));
-                    pfixed &= a.fixed.get(i);
+                    pfixed &= a.fixed().get(i);
                 }
-                v.fixed.set(i, pfixed);
+                if (pfixed)
+                    v.set_fixed_bit(i, v.get_bit(i));
             }
             break;
         }
@@ -373,36 +393,36 @@ namespace sls {
                 // i'th bit depends on bits j + k = i
                 // if the first j, resp k bits are 0, the bits j + k are 0  
                 for (; j < v.bw; ++j)
-                    if (!a.fixed.get(j))
+                    if (!a.fixed().get(j))
                         break;
                 for (; k < v.bw; ++k)
-                    if (!b.fixed.get(k))
+                    if (!b.fixed().get(k))
                         break;
                 for (; zj < v.bw; ++zj)
-                    if (!a.fixed.get(zj) || a.get_bit(zj))
+                    if (!a.fixed().get(zj) || a.get_bit(zj))
                         break;
                 for (; zk < v.bw; ++zk)
-                    if (!b.fixed.get(zk) || b.get_bit(zk))
+                    if (!b.fixed().get(zk) || b.get_bit(zk))
                         break;
                 for (; hzj < v.bw; ++hzj)
-                    if (!a.fixed.get(v.bw - hzj - 1) || a.get_bit(v.bw - hzj - 1))
+                    if (!a.fixed().get(v.bw - hzj - 1) || a.get_bit(v.bw - hzj - 1))
                         break;
                 for (; hzk < v.bw; ++hzk)
-                    if (!b.fixed.get(v.bw - hzk - 1) || b.get_bit(v.bw - hzk - 1))
+                    if (!b.fixed().get(v.bw - hzk - 1) || b.get_bit(v.bw - hzk - 1))
                         break;
 
 
                 if (j > 0 && k > 0) {
                     for (unsigned i = 0; i < std::min(k, j); ++i) {
                         SASSERT(!v.get_bit(i));
-                        v.fixed.set(i, true);
+                        v.set_fixed_bit(i, false);
                     }
                 }
                 // lower zj + jk bits are 0
                 if (zk > 0 || zj > 0) {
                     for (unsigned i = 0; i < zk + zj; ++i) {
                         SASSERT(!v.get_bit(i));
-                        v.fixed.set(i, true);
+                        v.set_fixed_bit(i, false);
                     }
                 }
                 // upper bits are 0, if enough high order bits of a, b are 0.
@@ -412,7 +432,7 @@ namespace sls {
                     hzk = v.bw - hzk;
                     for (unsigned i = hzj + hzk - 1; i < v.bw; ++i) {
                         SASSERT(!v.get_bit(i));
-                        v.fixed.set(i, true);
+                        v.set_fixed_bit(i, false);
                     }
                 }
             }
@@ -421,9 +441,10 @@ namespace sls {
                 for (unsigned i = 0; i < v.bw; ++i) {
                     for (unsigned j = 0; pfixed && j < e->get_num_args(); ++j) {
                         auto& a = ev.wval(e->get_arg(j));
-                        pfixed &= a.fixed.get(i);
+                        pfixed &= a.fixed().get(i);
                     }
-                    v.fixed.set(i, pfixed);
+                    if (pfixed)
+                        v.set_fixed_bit(i, v.get_bit(i));
                 }
             }
             break;
@@ -433,7 +454,8 @@ namespace sls {
             for (unsigned i = e->get_num_args(); i-- > 0; ) {
                 auto& a = ev.wval(e->get_arg(i));
                 for (unsigned j = 0; j < a.bw; ++j)
-                    v.fixed.set(bw + j, a.fixed.get(j));
+                    if (a.fixed().get(j))
+                        v.set_fixed_bit(bw + j, v.get_bit(bw + j));
                 bw += a.bw;
             }
             break;
@@ -444,19 +466,18 @@ namespace sls {
             VERIFY(bv.is_extract(e, lo, hi, child));
             auto& a = ev.wval(child);
             for (unsigned i = lo; i <= hi; ++i)
-                v.fixed.set(i - lo, a.fixed.get(i));
+                if (a.fixed().get(i))
+                    v.set_fixed_bit(i - lo, v.get_bit(i));
             break;
         }
         case OP_BNEG: {
             auto& a = ev.wval(e->get_arg(0));
             bool pfixed = true;
             for (unsigned i = 0; i < v.bw; ++i) {
-                if (pfixed && a.fixed.get(i))
-                    v.fixed.set(i, true);
-                else {
+                if (pfixed && a.fixed().get(i))
+                    v.set_fixed_bit(i, v.get_bit(i));
+                else
                     pfixed = false;
-                    v.fixed.set(i, false);
-                }
             }
             break;
         }
@@ -488,7 +509,7 @@ namespace sls {
         case OP_BUREM0:
         case OP_BSMOD:
         case OP_BSMOD_I:
-        case OP_BSMOD0:       
+        case OP_BSMOD0:
         case OP_BXNOR:
             // NOT_IMPLEMENTED_YET();
             break;
@@ -505,7 +526,7 @@ namespace sls {
         case OP_BSMUL_OVFL:
         case OP_BUMUL_NO_OVFL:
         case OP_BUMUL_OVFL:
-        case OP_BIT2BOOL: 
+        case OP_BIT2BOOL:
         case OP_ULEQ:
         case OP_UGEQ:
         case OP_UGT:
@@ -516,6 +537,6 @@ namespace sls {
         case OP_SLT:
             UNREACHABLE();
             break;
-        }      
+        }
     }
 }
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index dc8cfcd71..ff59c674b 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -163,6 +163,10 @@ namespace sls {
                 if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0)
                     e = to_app(ctx.atom(lit.var()));
         }
+        CTRACE("bv", !e, tout << "no candidate\n";
+        ctx.display(tout);
+        display_weights(tout););
+
         if (!e)
             return m_empty_vars;
 
@@ -347,45 +351,38 @@ namespace sls {
     * Rehearse an update. The update is revered while a score is computed and returned.
     * Walk all parents, until hitting predicates where their scores are computed.
     */
-    double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) {
-        SASSERT(bv.is_bv(e));
-        SASSERT(is_uninterp(e));
+    double bv_lookahead::lookahead_update(expr* t, bvect const& new_value) {
+        SASSERT(bv.is_bv(t));
+        SASSERT(is_uninterp(t));
         SASSERT(m_restore.empty());
-
-        bool has_tabu = false;
         double score = m_top_score;
 
-        wval(e).eval = new_value;
-        if (!insert_update(e)) {
-            restore_lookahead();
-            m_in_update_stack.reset();
+        if (!wval(t).can_set(new_value))
             return -1000000;
-        }
-        insert_update_stack(e);
-        unsigned max_depth = get_depth(e);
+
+        wval(t).eval = new_value;
+        insert_update(t);
+        insert_update_stack(t);
+        unsigned max_depth = get_depth(t);
         for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
-            for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
+            for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
                 auto a = m_update_stack[depth][i];
                 if (bv.is_bv(a)) {
-                    if (a == e || (m_ev.eval(a), insert_update(a))) { // do not insert e twice
-                        for (auto p : ctx.parents(a)) {
-                            insert_update_stack(p);
-                            max_depth = std::max(max_depth, get_depth(p));
-                        }
+                    if (a != t) {
+                        m_ev.eval(a);
+                        insert_update(a);
                     }
-                    else {
-                        IF_VERBOSE(3, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << " " << wval(a) << "\n");
-                        has_tabu = true;
+                    for (auto p : ctx.parents(a)) {
+                        insert_update_stack(p);
+                        max_depth = std::max(max_depth, get_depth(p));
                     }
                 }
-                else if (is_root(a)) {
-                     score += get_weight(a) * (new_score(a) - old_score(a));
-                }
+                else if (is_root(a)) 
+                    score += get_weight(a) * (new_score(a) - old_score(a));                
                 else if (m.is_bool(a))
                     continue;
                 else {
                     IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n");
-                    has_tabu = true;
                 }
             }
             m_update_stack[depth].reset();
@@ -393,10 +390,8 @@ namespace sls {
         m_in_update_stack.reset();
         restore_lookahead();
 
-        TRACE("sls_verbose", tout << mk_bounded_pp(e, m) << " := " << new_value << " score: " << m_top_score << "\n");
+        TRACE("sls_verbose", tout << mk_bounded_pp(t, m) << " := " << new_value << " score: " << m_top_score << "\n");
 
-        if (has_tabu)
-            return -10000;
         return score;
     }
 
@@ -476,7 +471,7 @@ namespace sls {
         wval(e).eval = new_value;
         double old_top_score = m_top_score;
 
-        VERIFY(wval(e).commit_eval());
+        VERIFY(wval(e).commit_eval_check_tabu());
         insert_update_stack(e);
         unsigned max_depth = get_depth(e);
         for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
@@ -484,12 +479,7 @@ namespace sls {
                 auto e = m_update_stack[depth][i];
                 if (bv.is_bv(e)) {
                     m_ev.eval(e); // updates wval(e).eval
-                    if (!wval(e).commit_eval()) {
-                        TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
-                        IF_VERBOSE(3, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
-                        // bv_plugin::is_sat picks up discrepancies
-                        continue;
-                    }
+                    wval(e).commit_eval_ignore_tabu();
                     for (auto p : ctx.parents(e)) {
                         insert_update_stack(p);
                         max_depth = std::max(max_depth, get_depth(p));
@@ -515,13 +505,13 @@ namespace sls {
         return true;
     }
 
-    bool bv_lookahead::insert_update(expr* e) {
+    void bv_lookahead::insert_update(expr* e) {
         auto& v = wval(e);
         m_restore.push_back(e);
         m_on_restore.mark(e);
         TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << " " << v << "\n");
         v.save_value();
-        return v.commit_eval();
+        v.commit_eval_ignore_tabu();
     }
 
     void bv_lookahead::insert_update_stack(expr* e) {
@@ -597,10 +587,11 @@ namespace sls {
             if (!is_bv_literal(lit))
                 continue;
             auto a = to_app(ctx.atom(lit.var()));
-            out
+            out << lit << ": "
                 << get_weight(a) << " "
                 << mk_bounded_pp(a, m) << " "
-                << old_score(a) << "\n";
+                << old_score(a) << " " 
+                << new_score(a) << "\n";
         }
         return out;
     }
diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h
index 0c505e039..a77598fa3 100644
--- a/src/ast/sls/sls_bv_lookahead.h
+++ b/src/ast/sls/sls_bv_lookahead.h
@@ -84,7 +84,7 @@ namespace sls {
         bv_valuation& wval(expr* e) const;
 
         void insert_update_stack(expr* e);
-        bool insert_update(expr* e);        
+        void insert_update(expr* e);        
         void restore_lookahead();
 
         bool_info& get_bool_info(expr* e);
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 3342dcba2..8798a3084 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -62,6 +62,7 @@ namespace sls {
         auto a = to_app(e);
 
         if (!m_eval.eval_is_correct(a)) {
+            TRACE("sls", tout << "incorrect eval " << lit << ": " << mk_bounded_pp(e, m) << "\n";);
             IF_VERBOSE(20, verbose_stream() << "repair " << lit << " " << mk_bounded_pp(e, m) << "\n");
             ctx.new_value_eh(e);
         }
@@ -89,6 +90,7 @@ namespace sls {
         bool is_sat = true;
         for (auto t : ctx.subterms())
             if (is_app(t) && bv.is_bv(t) && to_app(t)->get_family_id() == bv.get_fid() && !m_eval.eval_is_correct(to_app(t))) {
+                TRACE("sls", tout << "incorrect eval: " << mk_bounded_pp(t, m) << " " << m_eval.wval(t) << "\n";);
                 ctx.new_value_eh(t);
                 is_sat = false;
             }
@@ -106,7 +108,7 @@ namespace sls {
         VERIFY(bv.is_numeral(v, val));
         auto& w = m_eval.eval(to_app(e));
         w.set_value(w.eval, val);
-        return w.commit_eval();
+        return w.commit_eval_check_tabu();
     }
 
     bool bv_plugin::repair_down(app* e) {
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
index d23471a2c..9630a9a66 100644
--- a/src/ast/sls/sls_bv_valuation.cpp
+++ b/src/ast/sls/sls_bv_valuation.cpp
@@ -155,12 +155,13 @@ namespace sls {
         m_hi.set_bw(bw);
         m_bits.set_bw(bw);
         m_tmp.set_bw(bw);
-        fixed.set_bw(bw);
+        m_is_fixed.set_bw(bw);
+        m_fixed_values.set_bw(bw);
         eval.set_bw(bw);
         // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated        
         for (unsigned i = 0; i < nw; ++i)
-            m_lo[i] = 0, m_hi[i] = 0, m_bits[i] = 0, fixed[i] = 0, eval[i] = 0;
-        fixed[nw - 1] = ~mask;
+            m_lo[i] = 0, m_hi[i] = 0, m_bits[i] = 0, m_is_fixed[i] = 0, eval[i] = 0, m_fixed_values[i] = 0;
+        m_is_fixed[nw - 1] = ~mask;
     }
 
     void bv_valuation::set_bw(unsigned b) {
@@ -171,21 +172,22 @@ namespace sls {
             mask = ~(digit_t)0;
     }
 
-    bool bv_valuation::commit_eval() { 
+    bool bv_valuation::commit_eval_check_tabu() { 
         for (unsigned i = 0; i < nw; ++i)
-            if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))                 
-                return false;
-            
+            if (0 != (m_is_fixed[i] & (m_fixed_values[i] ^ eval[i])))                 
+                return false;            
         if (!in_range(eval)) 
-            return false;
-        
-        for (unsigned i = 0; i < nw; ++i) 
-            m_bits[i] = eval[i]; 
-
-        SASSERT(well_formed()); 
+            return false;        
+        commit_eval_ignore_tabu();
         return true;
     }
 
+    void bv_valuation::commit_eval_ignore_tabu() {
+        for (unsigned i = 0; i < nw; ++i)
+            m_bits[i] = eval[i];
+        SASSERT(well_formed());
+    }
+
     bool bv_valuation::in_range(bvect const& bits) const {
         mpn_manager m;
         auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw);
@@ -306,21 +308,21 @@ namespace sls {
 
     void bv_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {      
         for (unsigned i = bw; !is_feasible(dst) && i-- > 0; )
-            if (!fixed.get(i) && dst.get(i))
+            if (!m_is_fixed.get(i) && dst.get(i))
                 dst.set(i, false);      
         repair_sign_bits(dst);
     }
 
     void bv_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
         for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i)
-            if (!fixed.get(i) && !dst.get(i))
+            if (!m_is_fixed.get(i) && !dst.get(i))
                 dst.set(i, true);
         repair_sign_bits(dst);
     }
 
     void bv_valuation::set_random_above(bvect& dst, random_gen& r) {
         for (unsigned i = 0; i < nw; ++i)
-            dst[i] = dst[i] | (random_bits(r) & ~fixed[i]);
+            dst[i] = dst[i] | (random_bits(r) & ~m_is_fixed[i]);
         repair_sign_bits(dst);
     }
 
@@ -329,21 +331,21 @@ namespace sls {
             return;
         unsigned n = 0, idx = UINT_MAX;
         for (unsigned i = 0; i < bw; ++i)
-            if (dst.get(i) && !fixed.get(i) && (r() % ++n) == 0)
+            if (dst.get(i) && !m_is_fixed.get(i) && (r() % ++n) == 0)
                 idx = i;                
 
         if (idx == UINT_MAX)
             return;
         dst.set(idx, false);
         for (unsigned i = 0; i < idx; ++i) 
-            if (!fixed.get(i))
+            if (!m_is_fixed.get(i))
                 dst.set(i, r() % 2 == 0);
         repair_sign_bits(dst);
     }
 
     bool bv_valuation::set_repair(bool try_down, bvect& dst) {
         for (unsigned i = 0; i < nw; ++i)
-            dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
+            dst[i] = (~m_is_fixed[i] & dst[i]) | (m_is_fixed[i] & m_bits[i]);
         clear_overflow_bits(dst);
         repair_sign_bits(dst);
         if (in_range(dst)) {
@@ -354,18 +356,18 @@ namespace sls {
         dst.set_bw(bw);
         if (m_lo < m_hi) {
             for (unsigned i = bw; m_hi <= dst && !in_range(dst) && i-- > 0; )
-                if (!fixed.get(i) && dst.get(i))
+                if (!m_is_fixed.get(i) && dst.get(i))
                     dst.set(i, false);
             for (unsigned i = 0; i < bw && dst < m_lo && !in_range(dst); ++i)
-                if (!fixed.get(i) && !dst.get(i))
+                if (!m_is_fixed.get(i) && !dst.get(i))
                     dst.set(i, true);
         }
         else {
             for (unsigned i = 0; !in_range(dst) && i < bw; ++i)
-                if (!fixed.get(i) && !dst.get(i))
+                if (!m_is_fixed.get(i) && !dst.get(i))
                     dst.set(i, true);
             for (unsigned i = bw; !in_range(dst) && i-- > 0;)
-                if (!fixed.get(i) && dst.get(i))
+                if (!m_is_fixed.get(i) && dst.get(i))
                     dst.set(i, false);
         }
         repair_sign_bits(dst);
@@ -382,7 +384,7 @@ namespace sls {
             m_lo.copy_to(nw, out);        
         else {
             for (unsigned i = 0; i < nw; ++i)
-                out[i] = fixed[i] & m_bits[i];
+                out[i] = m_is_fixed[i] & m_bits[i];
         }
         repair_sign_bits(out);
         SASSERT(!has_overflow(out));
@@ -395,7 +397,7 @@ namespace sls {
         }
         else {
             for (unsigned i = 0; i < nw; ++i)
-                out[i] = ~fixed[i] | m_bits[i];
+                out[i] = ~m_is_fixed[i] | m_bits[i];
         }
         repair_sign_bits(out);
         SASSERT(!has_overflow(out));
@@ -438,7 +440,7 @@ namespace sls {
 
     void bv_valuation::get_variant(bvect& dst, random_gen& r) const {
         for (unsigned i = 0; i < nw; ++i)
-            dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
+            dst[i] = (random_bits(r) & ~m_is_fixed[i]) | (m_is_fixed[i] & m_bits[i]);
         repair_sign_bits(dst);
         clear_overflow_bits(dst);
     }
@@ -466,11 +468,11 @@ namespace sls {
         set_add(m_tmp, m_tmp, m_lo);
         // respect fixed bits
         for (unsigned i = 0; i < bw; ++i)
-            if (fixed.get(i))
+            if (m_is_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))
+            if (!m_is_fixed.get(i))
                 m_tmp.set(i, false);
         repair_sign_bits(m_tmp);
         return try_set(m_tmp);      
@@ -482,12 +484,12 @@ namespace sls {
         bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1);
         for (unsigned i = bw; i-- > bw - m_signed_prefix; ) {
             if (dst.get(i) != sign) {
-                if (fixed.get(i)) {
+                if (m_is_fixed.get(i)) {
                     unsigned j = bw - m_signed_prefix;
-                    if (j > 0 && !fixed.get(j - 1))
+                    if (j > 0 && !m_is_fixed.get(j - 1))
                         dst.set(j - 1, !sign);
                     for (unsigned i = bw; i-- > bw - m_signed_prefix; )
-                        if (!fixed.get(i))
+                        if (!m_is_fixed.get(i))
                             dst.set(i, !sign);
                     return;
                 }
@@ -505,13 +507,12 @@ namespace sls {
     bool bv_valuation::can_set(bvect const& new_bits) const {
         SASSERT(!has_overflow(new_bits));
         for (unsigned i = 0; i < nw; ++i)
-            if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i]))
+            if (0 != ((new_bits[i] ^ m_fixed_values[i]) & m_is_fixed[i]))
                 return false;
         return in_range(new_bits);
     }
 
     unsigned bv_valuation::to_nat(unsigned max_n) const {
-
         bvect const& d = m_bits;
         SASSERT(!has_overflow(d));
         return d.to_nat(max_n);
@@ -586,7 +587,7 @@ namespace sls {
     unsigned bv_valuation::diff_index(bvect const& a) const {
         unsigned index = 0;
         for (unsigned i = nw; i-- > 0; ) {
-            auto diff = fixed[i] & (m_bits[i] ^ a[i]);
+            auto diff = m_is_fixed[i] & (m_fixed_values[i] ^ a[i]);
             if (diff != 0 && index == 0)
                 index = 1 + i * 8 * sizeof(digit_t) + log2(diff);
         }
@@ -603,13 +604,13 @@ namespace sls {
         --lo_index;
 
         // decrement a[lo_index:0] maximally
-        SASSERT(a.get(lo_index) != m_bits.get(lo_index));
-        SASSERT(fixed.get(lo_index));
+        SASSERT(a.get(lo_index) != m_fixed_values.get(lo_index));
+        SASSERT(m_is_fixed.get(lo_index));
         for (unsigned i = 0; i <= lo_index; ++i) {
-            if (!fixed.get(i))
+            if (!m_is_fixed.get(i))
                 a.set(i, false);
-            else if (fixed.get(i))
-                a.set(i, m_bits.get(i));
+            else if (m_is_fixed.get(i))
+                a.set(i, m_fixed_values.get(i));
         }
 
         // the previous value of a[lo_index] was 0.
@@ -619,7 +620,7 @@ namespace sls {
 
         // find the minimal increment within a[:lo_index+1]
         for (unsigned i = lo_index + 1; i < bw; ++i) {
-            if (!fixed.get(i) && !a.get(i)) {
+            if (!m_is_fixed.get(i) && !a.get(i)) {
                 a.set(i, true);
                 return;
             }
@@ -627,7 +628,7 @@ namespace sls {
         // there is no feasiable value a' >= a, so find the least
         // feasiable value a' >= 0.
         for (unsigned i = 0; i < bw; ++i)
-            if (!fixed.get(i))
+            if (!m_is_fixed.get(i))
                 a.set(i, false);
     }
 
@@ -639,15 +640,15 @@ namespace sls {
         if (hi_index == 0)
             return;
         --hi_index;
-        SASSERT(a.get(hi_index) != m_bits.get(hi_index));
-        SASSERT(fixed.get(hi_index));
+        SASSERT(a.get(hi_index) != m_fixed_values.get(hi_index));
+        SASSERT(m_is_fixed.get(hi_index));
 
         // increment a[hi_index:0] maximally
         for (unsigned i = 0; i <= hi_index; ++i) {
-            if (!fixed.get(i))
+            if (!m_is_fixed.get(i))
                 a.set(i, true);
-            else if (fixed.get(i))
-                a.set(i, m_bits.get(i));
+            else if (m_is_fixed.get(i))
+                a.set(i, m_fixed_values.get(i));
         }
 
         // If a[hi_index:0] was decremented, then no need to adjust bits a[:hi_index+1]
@@ -656,7 +657,7 @@ namespace sls {
 
         // find the minimal decrement within a[:hi_index+1]
         for (unsigned i = hi_index + 1; i < bw; ++i) {
-            if (!fixed.get(i) && a.get(i)) {
+            if (!m_is_fixed.get(i) && a.get(i)) {
                 a.set(i, false);
                 return;
             }
@@ -665,14 +666,14 @@ 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)) 
+            if (!m_is_fixed.get(i)) 
                 a.set(i, true);       
     }
 
     void bv_valuation::tighten_range() {
         
         // verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
-        if (m_lo == m_hi)
+        if (!has_range())
             return;     
 
         inf_feasible(m_lo);
@@ -685,16 +686,23 @@ namespace sls {
         add1(hi1);
         hi1.copy_to(nw, m_hi);
 
-        if (has_range() && !in_range(m_bits)) 
+        if (!has_range())
+            return;
+
+        if (!in_range(m_bits)) {
+            if (!can_set(m_lo))
+                return;
+            m_lo.copy_to(nw, m_fixed_values);
             m_lo.copy_to(nw, m_bits);
+        }        
 
         if (mod(lo() + 1, rational::power_of_two(bw)) == hi())
             for (unsigned i = 0; i < nw; ++i)
-                fixed[i] = ~0;      
+                m_is_fixed[i] = ~0;      
         if (lo() < hi() && hi() < rational::power_of_two(bw - 1))
             for (unsigned i = 0; i < bw; ++i)
                 if (hi() < rational::power_of_two(i))
-                    fixed.set(i, true);
+                    m_is_fixed.set(i, true);
         
         // verbose_stream() << "post tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
         SASSERT(well_formed());
diff --git a/src/ast/sls/sls_bv_valuation.h b/src/ast/sls/sls_bv_valuation.h
index 9156c934f..bc04c2cd6 100644
--- a/src/ast/sls/sls_bv_valuation.h
+++ b/src/ast/sls/sls_bv_valuation.h
@@ -107,7 +107,8 @@ namespace sls {
     class bv_valuation {
     protected:
         bvect m_bits;
-        bvect m_lo, m_hi;        // range assignment to bit-vector, as wrap-around interval
+        bvect m_lo, m_hi;                   // range assignment to bit-vector, as wrap-around interval
+        bvect m_is_fixed, m_fixed_values;   // fixed values
         bvect m_tmp;
         unsigned m_signed_prefix = 0;
 
@@ -119,7 +120,6 @@ namespace sls {
     public:
         unsigned bw;                     // bit-width
         unsigned nw;                     // num words
-        bvect fixed;                     // bit assignment and don't care bit
         bvect eval;                      // current evaluation
 
         
@@ -133,13 +133,18 @@ 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; }
+        bvect const& fixed() const { return m_is_fixed; }
+        digit_t fixed(unsigned i) const { return m_is_fixed[i]; }
+        void set_fixed_bit(unsigned i, bool bit) { m_is_fixed.set(i, true); m_fixed_values.set(i, bit); }
+        void set_fixed_word(unsigned i, digit_t mask, digit_t value) { m_is_fixed[i] = mask; m_fixed_values[i] = value; }
+        bool commit_eval_check_tabu();
+        void commit_eval_ignore_tabu();
+        bool is_fixed() const { for (unsigned i = bw; i-- > 0; ) if (!m_is_fixed.get(i)) return false; return true; }
 
         bool get_bit(unsigned i) const { return m_bits.get(i); }
         bool try_set_bit(unsigned i, bool b) {
             SASSERT(in_range(m_bits));
-            if (fixed.get(i) && get_bit(i) != b)
+            if (m_is_fixed.get(i) && m_fixed_values.get(i) != b)
                 return false;
             m_bits.set(i, b);   
             eval.set(i, b);
@@ -307,7 +312,7 @@ namespace sls {
 
         bool try_set_range(bvect& dst, unsigned lo, unsigned hi, bool b) {
             for (unsigned i = lo; i < hi; ++i)
-                if (fixed.get(i) && get_bit(i) != b)
+                if (m_is_fixed.get(i) && get_bit(i) != b)
                     return false;
             for (unsigned i = lo; i < hi; ++i)
                 dst.set(i, b);
@@ -330,17 +335,15 @@ namespace sls {
         std::ostream& display(std::ostream& out) const {
             out << m_bits;
             out << " ev: " << eval;
-            if (!is_zero(fixed)) {
-                out << " fix:";
-                out << fixed;
-            }
+            if (!is_zero(m_is_fixed)) 
+                out << " fix:" << m_is_fixed << " " << m_fixed_values;            
             if (m_lo != m_hi) 
                 out << " [" << m_lo << ", " << m_hi << "[";            
             return out;
         }
 
         bool well_formed() const {
-            return !has_overflow(m_bits) && (!has_range() || in_range(m_bits));
+            return !has_overflow(m_bits) && (!has_range() || in_range(m_fixed_values));
         }
 
     };