diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index c47dacc96..3573d44f3 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -181,6 +181,17 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
+    unsigned m_keypos;
+
+    void start_rewrite() {
+        m_keypos = m_keys.size();
+    }
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits) {
+        for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
+            const2bits.insert(m_keys[i].get(), m_values[i].get());
+        }
+    }
+
     template<typename V>
     app * mk_mkbv(V const & bits) {
         return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@@ -635,6 +646,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
     }
     void push() { m_cfg.push(); }
     void pop(unsigned s) { m_cfg.pop(s); }
+    void start_rewrite() { m_cfg.start_rewrite(); }
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits) { m_cfg.end_rewrite(const2bits); }
     unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
 };
 
@@ -683,3 +696,10 @@ unsigned bit_blaster_rewriter::get_num_scopes() const {
     return m_imp->get_num_scopes();
 }
 
+void bit_blaster_rewriter::start_rewrite() {
+    m_imp->start_rewrite();
+}
+
+void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits) {
+    m_imp->end_rewrite(const2bits);
+}
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
index 6ffed00ae..2463bd086 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
@@ -33,7 +33,9 @@ public:
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();
-    obj_map<func_decl, expr*> const& const2bits() const; 
+    obj_map<func_decl, expr*> const& const2bits() const;     
+    void start_rewrite();
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits);
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index 666f79d97..2118c85eb 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -670,6 +670,14 @@ private:
         return peek(pos) == "<=" || peek(pos) == "=<";
     }
 
+    bool peek_minus_infty(unsigned pos) {
+        return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
+    }
+
+    bool peek_plus_infty(unsigned pos) {
+        return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
+    }
+
     void parse_indicator(symbol& var, rational& val) {
         if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
             var = peek(0);
@@ -703,11 +711,15 @@ private:
             v = peek(2);
             update_lower(lhs, v);
             tok.next(3);
-            if (peek_le(0) && tok.peek_num(1)) {
-                rational rhs = tok.get_num(1);
-                update_upper(v, rhs);
-                tok.next(2);
-            }
+            parse_upper(v);
+        }
+        else if (peek_minus_infty(0) && peek_le(2)) {
+            v = peek(3);
+            tok.next(4);
+            parse_upper(v);
+        }
+        else if (peek_plus_infty(2) && peek_le(1)) {
+            tok.next(4);            
         }
         else if (peek_le(1) && tok.peek_num(2)) {
             v = peek(0);
@@ -721,6 +733,18 @@ private:
         }
     }
 
+    void parse_upper(symbol const& v) {
+        if (peek_le(0) && tok.peek_num(1)) {
+            rational rhs = tok.get_num(1);
+            update_upper(v, rhs);
+            tok.next(2);
+        }
+        else if (peek_le(0) && peek_plus_infty(1)) {
+            tok.next(3);            
+        }
+
+    }
+
     void update_lower(rational const& r, symbol const& v) {
         bound b;
         m_bounds.find(v, b);
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 6adaa1ef6..d1a0c7403 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -47,16 +47,6 @@ namespace sat {
         return static_cast<pb const&>(*this);
     }
 
-    ba_solver::eq& ba_solver::constraint::to_eq() {
-        SASSERT(is_eq());
-        return static_cast<eq&>(*this);
-    }
-
-    ba_solver::eq const& ba_solver::constraint::to_eq() const{
-        SASSERT(is_eq());
-        return static_cast<eq const&>(*this);
-    }
-
     ba_solver::xr& ba_solver::constraint::to_xr() {
         SASSERT(is_xr());
         return static_cast<xr&>(*this);
@@ -95,15 +85,6 @@ namespace sat {
             }            
             break;
         }
-        case ba_solver::eq_t: {
-            ba_solver::eq const& e = cnstr.to_eq();
-            for (ba_solver::eliteral wl : e) {
-                if (wl.weight != 1) out << wl.weight << " * ";
-                out << wl.lit << " ";
-            }
-            out << " = " << e.k();
-            break;
-        }
         default:
             UNREACHABLE();
         }
@@ -205,33 +186,6 @@ namespace sat {
     }
 
 
-    // -----------------------------------
-    // eq
-
-    ba_solver::eq::eq(unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
-        constraint(eq_t, id, lit, wlits.size(), eq::get_obj_size(wlits.size())),
-        m_lo(0),
-        m_hi(0),
-        m_max(0),        
-        m_k(k)        
-    {
-        unsigned i = 0;        
-        for (wliteral const& w : wlits) {
-            m_wlits[i++] = eliteral(w.first, w.second);
-            m_max += w.first;
-        }
-        m_hi = m_max;
-        m_trail_sz = 0;
-    }
-
-    unsigned ba_solver::eq::index(literal l) const {
-        for (unsigned i = 0; i < size(); ++i) {
-            if (l.var() == m_wlits[i].lit.var()) return i;
-        }
-        UNREACHABLE();
-        return UINT_MAX;
-    }
-
     // -----------------------------------
     // xr
     
@@ -271,7 +225,7 @@ namespace sat {
         }
         if (root != null_literal) {
             if (!is_watched(root, c)) watch_literal(root, c);
-            if (!is_watched(~root, c)) watch_literal(~root, c);
+            if (!c.is_pure() && !is_watched(~root, c)) watch_literal(~root, c);
         }
         TRACE("ba", display(tout << "init watch: ", c, true););
         SASSERT(root == null_literal || value(root) == l_true);
@@ -925,251 +879,6 @@ namespace sat {
         out << ">= " << p.k()  << "\n";
     }
 
-    // --------------------
-    // eq:
-
-    ba_solver::constraint* ba_solver::add_eq(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
-        void * mem = m_allocator.allocate(eq::get_obj_size(wlits.size()));
-        eq* e = new (mem) eq(next_id(), lit, wlits, k);
-        e->set_learned(learned);
-        add_constraint(e);
-        for (eliteral const& wl : *e) {
-            watch_literal(wl.lit, *e);
-            watch_literal(~(wl.lit), *e);
-        }        
-        return e;
-    }
-
-    void ba_solver::display(std::ostream& out, eq const& e, bool values) const {
-        display_lit(out, e.lit(), e.size(), values);
-        if (values) {
-            if (e.trail_sz() > 0) {
-                out << "trail: ";
-                for (unsigned i = 0; i < e.trail_sz(); ++i) {
-                    out << e[i].tweight << " * " << e[i].tlit << " ";
-                }
-            }
-            out << "[" << e.lo() << ":" << e.hi() << "] ";
-        }
-        for (eliteral wl : e) {
-            literal l = wl.lit;
-            unsigned w = wl.weight;
-            if (w > 1) out << w << " * ";
-            out << l;
-            if (values) {
-                out << "@(" << value(l);
-                if (value(l) != l_undef) {
-                    out << ":" << lvl(l);
-                }
-                out << ") ";
-            }
-            else {
-                out << " ";
-            }
-        }
-        out << "= " << e.k()  << "\n";
-    }
-
-    bool ba_solver::init_watch(eq& e) {
-        return true;
-    }
-
-    void ba_solver::clear_watch(eq& e) {
-        for (eliteral const& wl : e) {
-            unwatch_literal(wl.lit, e);
-            unwatch_literal(~(wl.lit), e);
-        }
-        if (e.lit() != null_literal) {
-            unwatch_literal(e.lit(), e);
-            unwatch_literal(~e.lit(), e);
-        }
-    }
-
-    /*
-     * \update the bounds for [lo,hi] based on what is unassigned on the trail.
-     */
-    void ba_solver::pop_eq(eq& e) {
-        unsigned idx = e.trail_sz() - 1;
-        literal tlit = e[idx].tlit;
-        if (tlit.sign()) {
-            e.inc_hi(e[idx].tweight);
-        }
-        else {
-            e.dec_lo(e[idx].tweight);
-        }
-        e.set_trail_sz(idx);
-    }
-
-    lbool ba_solver::add_assign(eq& e, literal nl) {
-        //IF_VERBOSE(0, verbose_stream() << nl << "@" << lvl(nl) << ": " << e << "\n");
-        SASSERT(value(nl) == l_false);
-        if (nl.var() == e.lit().var()) {
-            // no-op
-        }
-        else {
-            unsigned i = e.index(nl);
-            eliteral wl = e[i];
-            if (wl.lit == nl) {
-                e.dec_hi(wl);
-            }
-            else {
-                SASSERT(wl.lit == ~nl);
-                e.inc_lo(wl);
-            }
-            m_eq_to_pop.push_back(&e);
-        }
-        if (e.lo() > e.k() || e.hi() < e.k()) {
-            if (e.lit() == null_literal || value(e.lit()) == l_true) {
-                set_conflict(e, nl);
-                return l_false;
-            }
-            if (e.lit() != null_literal && value(e.lit()) == l_undef) {
-                assign(e, ~e.lit());
-            }
-        }
-        else if (e.lo() == e.hi()) {
-            SASSERT(e.lo() == e.k());
-            if (e.lit() != null_literal && value(e.lit()) == l_false) {
-                set_conflict(e, nl);
-                return l_false;
-            }
-            if (e.lit() != null_literal && value(e.lit()) == l_undef) {
-                assign(e, e.lit());
-            }
-        }
-        else if ((e.lit() == null_literal || value(e.lit()) == l_true)) {
-            if (e.lo() == e.k()) {
-                for (eliteral el : e) {
-                    if (value(el.lit) == l_undef) {
-                        //IF_VERBOSE(0, display(verbose_stream() << "proapgate " << ~el.lit << " ", e, true));
-                        assign(e, ~el.lit);
-                    }
-                }
-            }
-            else if (e.hi() == e.k()) {
-                for (eliteral el : e) {
-                    if (value(el.lit) == l_undef) {
-                        //IF_VERBOSE(0, display(verbose_stream() << "proapgate " << el.lit << " ", e, true));
-                        assign(e, el.lit);
-                    }
-                }
-            }
-        }
-        return l_true;
-    }
-
-    void ba_solver::simplify(eq& e) {
-        // no-op for now
-    }
-
-    void ba_solver::recompile(eq& e) {
-        for (eliteral const& el : e) {
-            m_weights[el.lit.index()] += el.weight;
-        }
-        unsigned k = e.k(), sz = e.size();
-        unsigned j = 0;
-        bool is_false = false;
-        for (unsigned i = 0; i < sz; ++i) {
-            eliteral el = e[i];
-            unsigned w1 = m_weights[el.lit.index()];
-            unsigned w2 = m_weights[(~el.lit).index()];
-            if (w1 == 0 || w1 < w2) continue;
-            if (k < w2) {
-                is_false = true;
-                break;
-            }            
-            k  -= w2;
-            w1 -= w2;
-            if (w1 == 0) continue;            
-            e[j++] = eliteral(w1, el.lit);            
-        }
-        sz = j;
-        for (eliteral const& el : e) {
-            m_weights[el.lit.index()] = 0;
-            m_weights[(~el.lit).index()] = 0;
-        }        
-        if (is_false) {
-            if (e.lit() == null_literal) {
-                s().mk_clause(0, 0, true);
-            }
-            else {
-                literal lit = ~e.lit();
-                s().mk_clause(1, &lit, true);
-            }
-            remove_constraint(e, "recompiled to false");
-            return;
-        }
-        // update trail
-        e.set_size(sz);
-        e.set_k(k);
-        for (unsigned i = 0; i < sz; ++i) {
-            e[i].tlit = null_literal;
-        }                
-        e.set_trail_sz(0);
-        e.reset_lo();
-        e.reset_hi();
-        for (eliteral const& el : e) {            
-            switch (value(el.lit)) {
-            case l_true:  e.inc_lo(el); break;
-            case l_false: e.dec_hi(el); break;
-            default: break;
-            }
-        }
-    }
-
-    void ba_solver::split_root(eq& e) {
-        NOT_IMPLEMENTED_YET();
-    }
-
-    void ba_solver::get_antecedents(literal l, eq const& e, literal_vector& r) {
-        for (eliteral wl : e) {
-            if (wl.lit.var() == l.var()) continue;
-            switch (value(wl.lit)) {
-            case l_true: r.push_back(wl.lit); break;
-            case l_false: r.push_back(~wl.lit); break;
-            default: break;
-            }
-        }
-        if (e.lit() != null_literal && l.var() != e.lit().var()) {
-            switch (value(e.lit())) {
-            case l_true: r.push_back(e.lit()); break;
-            case l_false: r.push_back(~e.lit()); break;
-            default: break;
-            }            
-        }
-    }
-
-    lbool ba_solver::eval(eq const& e) const {
-        unsigned trues = 0, undefs = 0;
-        for (eliteral wl : e) {
-            switch (value(wl.lit)) {
-            case l_true: trues += wl.weight; break;
-            case l_undef: undefs += wl.weight; break;
-            default: break;
-            }
-        }
-        if (trues + undefs < e.k()) return l_false;
-        if (trues > e.k()) return l_false;
-        if (trues == e.k() && undefs == 0) return l_true;
-        return l_undef;        
-    }
-
-    lbool ba_solver::eval(model const& m, eq const& e) const {
-        unsigned trues = 0, undefs = 0;
-        for (eliteral wl : e) {
-            switch (value(m, wl.lit)) {
-            case l_true: trues += wl.weight; break;
-            case l_undef: undefs += wl.weight; break;
-            default: break;
-            }
-        }
-        if (trues + undefs < e.k()) return l_false;
-        if (trues > e.k()) return l_false;
-        if (trues == e.k() && undefs == 0) return l_true;
-        return l_undef;        
-    }
-
-
     // --------------------
     // xr:
 
@@ -1512,17 +1221,6 @@ namespace sat {
                     for (literal l : m_lemma) process_antecedent(~l, offset);
                     break;
                 }
-                case eq_t: {
-                    eq& e = cnstr.to_eq();
-                    m_lemma.reset();
-                    inc_bound(offset);
-                    inc_coeff(consequent, offset);
-                    get_antecedents(consequent, e, m_lemma);
-                    TRACE("ba", display(tout, e, true); tout << m_lemma << "\n";);
-                    for (literal l : m_lemma) process_antecedent(~l, offset);
-                    break;
-
-                }
                 default:
                     UNREACHABLE();
                     break;
@@ -1888,7 +1586,6 @@ namespace sat {
         case card_t: return init_watch(c.to_card()); 
         case pb_t: return init_watch(c.to_pb());
         case xr_t: return init_watch(c.to_xr()); 
-        case eq_t: return init_watch(c.to_eq());
         }
         UNREACHABLE();
         return false;
@@ -1899,7 +1596,6 @@ namespace sat {
         case card_t: return add_assign(c.to_card(), l); 
         case pb_t: return add_assign(c.to_pb(), l); 
         case xr_t: return add_assign(c.to_xr(), l);
-        case eq_t: return add_assign(c.to_eq(), l);
         }
         UNREACHABLE();
         return l_undef;
@@ -1950,7 +1646,7 @@ namespace sat {
             init_watch(c);
             return true;
         }
-        else if (c.lit() != null_literal && value(c.lit()) != l_true && c.tag() != eq_t) {
+        else if (c.lit() != null_literal && value(c.lit()) != l_true) {
             return true;
         }
         else {
@@ -2005,7 +1701,6 @@ namespace sat {
         case card_t: return get_reward(c.to_card(), occs);
         case pb_t: return get_reward(c.to_pb(), occs); 
         case xr_t: return 0;
-        case eq_t: return 1;
         default: UNREACHABLE(); return 0;
         }
     }
@@ -2310,6 +2005,7 @@ namespace sat {
     }
 
     void ba_solver::watch_literal(literal lit, constraint& c) {
+        if (c.is_pure() && lit == ~c.lit()) return;
         get_wlist(~lit).push_back(watched(c.index()));
     }
 
@@ -2318,7 +2014,6 @@ namespace sat {
         case card_t: get_antecedents(l, c.to_card(), r); break;
         case pb_t: get_antecedents(l, c.to_pb(), r); break;
         case xr_t: get_antecedents(l, c.to_xr(), r); break;
-        case eq_t: get_antecedents(l, c.to_eq(), r); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -2342,9 +2037,6 @@ namespace sat {
         case xr_t:
             clear_watch(c.to_xr());
             break;
-        case eq_t:
-            clear_watch(c.to_eq());
-            break;
         default:
             UNREACHABLE();
         }
@@ -2367,7 +2059,6 @@ namespace sat {
         case card_t:  return validate_unit_propagation(c.to_card(), l); 
         case pb_t: return validate_unit_propagation(c.to_pb(), l);
         case xr_t: return true;
-        case eq_t: return validate_unit_propagation(c.to_eq(), l);
         default: UNREACHABLE(); break;
         }
         return false;
@@ -2383,7 +2074,6 @@ namespace sat {
         case card_t: return eval(v1, eval(c.to_card())); 
         case pb_t:   return eval(v1, eval(c.to_pb()));
         case xr_t:  return eval(v1, eval(c.to_xr()));
-        case eq_t:  return eval(v1, eval(c.to_eq()));
         default: UNREACHABLE(); break;
         }
         return l_undef;        
@@ -2395,7 +2085,6 @@ namespace sat {
         case card_t: return eval(v1, eval(m, c.to_card())); 
         case pb_t:   return eval(v1, eval(m, c.to_pb()));
         case xr_t:   return eval(v1, eval(m, c.to_xr()));
-        case eq_t:   return eval(v1, eval(m, c.to_eq()));
         default: UNREACHABLE(); break;
         }
         return l_undef;        
@@ -2730,7 +2419,6 @@ namespace sat {
 
     void ba_solver::push() {
         m_constraint_to_reinit_lim.push_back(m_constraint_to_reinit.size());
-        m_eq_to_pop_lim.push_back(m_eq_to_pop.size());
     }
 
     void ba_solver::pop(unsigned n) {        
@@ -2739,13 +2427,6 @@ namespace sat {
         m_constraint_to_reinit_last_sz = m_constraint_to_reinit_lim[new_lim];
         m_constraint_to_reinit_lim.shrink(new_lim);
         m_num_propagations_since_pop = 0;
-
-        new_lim = m_eq_to_pop_lim.size() - n;
-        for (unsigned i = m_eq_to_pop_lim[new_lim]; i < m_eq_to_pop.size(); ++i) {
-            pop_eq(*m_eq_to_pop[i]);
-        }
-        m_eq_to_pop.shrink(m_eq_to_pop_lim[new_lim]);
-        m_eq_to_pop_lim.shrink(new_lim);
     }
 
     void ba_solver::pop_reinit() {
@@ -2772,9 +2453,6 @@ namespace sat {
         case xr_t:
             simplify(c.to_xr());
             break;
-        case eq_t:
-            simplify(c.to_eq());
-            break;
         default:
             UNREACHABLE();
         }                
@@ -2798,6 +2476,7 @@ namespace sat {
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
             cleanup_clauses();
             cleanup_constraints();
+            update_pure();
         }        
         while (m_simplify_change || trail_sz < s().init_trail_size());
 
@@ -2814,7 +2493,41 @@ namespace sat {
         // IF_VERBOSE(0, s().display(verbose_stream()));
         // mutex_reduction();
         // if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
+    }
 
+    /*
+     * ~lit does not occur in clauses
+     * ~lit is only in one constraint use list
+     * lit == C 
+     * -> ignore assignemnts to ~lit for C
+     * 
+     * ~lit does not occur in clauses
+     * lit is only in one constraint use list
+     * lit == C
+     * -> negate: ~lit == ~C
+     */
+    void ba_solver::update_pure() {
+        // return;
+        for (constraint* cp : m_constraints) {
+            literal lit = cp->lit();
+            if (lit != null_literal && 
+                !cp->is_pure() &&
+                value(lit) == l_undef && 
+                get_wlist(~lit).size() == 1 &&                 
+                m_clause_use_list.get(lit).empty()) {
+                clear_watch(*cp);
+                cp->negate();
+                lit.neg();
+            }
+            if (lit != null_literal && 
+                !cp->is_pure() &&
+                m_cnstr_use_list[(~lit).index()].size() == 1 &&
+                get_wlist(lit).size() == 1 && 
+                m_clause_use_list.get(~lit).empty()) { 
+                cp->set_pure();
+                get_wlist(~lit).erase(watched(cp->index())); // just ignore assignments to false
+            }
+        }
     }
 
     void ba_solver::mutex_reduction() {
@@ -2930,9 +2643,6 @@ namespace sat {
         case pb_t:
             recompile(c.to_pb());
             break;
-        case eq_t:
-            recompile(c.to_eq());
-            break;            
         case xr_t:
             NOT_IMPLEMENTED_YET();
             break;
@@ -3144,7 +2854,6 @@ namespace sat {
         case card_t: split_root(c.to_card()); break;
         case pb_t: split_root(c.to_pb()); break;
         case xr_t: NOT_IMPLEMENTED_YET(); break;
-        case eq_t: split_root(c.to_eq()); break;
         }
     }
 
@@ -3265,15 +2974,6 @@ namespace sat {
                 }             
                 break;
             }
-            case eq_t: {
-                eq& e = cp->to_eq();
-                for (eliteral wl : e) {
-                    literal l = wl.lit;
-                    m_cnstr_use_list[l.index()].push_back(&e);
-                    m_cnstr_use_list[(~l).index()].push_back(&e);
-                }
-                break;
-            }
             }
         }
     }
@@ -3296,8 +2996,6 @@ namespace sat {
                 }
                 break;
             }
-            case eq_t: 
-                break;
             default:
                 break;
             }
@@ -3372,8 +3070,6 @@ namespace sat {
             if (p.k() > 1) subsumption(p);
             break;
         }
-        case eq_t: 
-            break;
         default:
             break;                
         }
@@ -3464,30 +3160,32 @@ namespace sat {
         return c1_exclusive + c2.k() + comp.size() <= c1.k();
     }
 
-    bool ba_solver::subsumes(card& c1, clause& c2, literal_vector & comp) {
-        unsigned c2_exclusive = 0;
-        unsigned common = 0;
-        comp.reset();
+    /*
+      \brief L + A >= k subsumes L + C if |A| < k
+             A + L + B >= k self-subsumes A + ~L + C >= 1
+             if k + 1 - |B| - |C| - |L| > 0
+     */
+    bool ba_solver::subsumes(card& c1, clause& c2, bool& self) {
+        unsigned common = 0, complement = 0, c2_exclusive = 0;
+        self = false;
+        
         for (literal l : c2) {
             if (is_marked(l)) {
                 ++common;
             }
             else if (is_marked(~l)) {
-                comp.push_back(l);
+                ++complement;
             }
             else {
                 ++c2_exclusive;
             }
         }
-
-        unsigned c1_exclusive = c1.size() - common - comp.size();
-        bool result = c1_exclusive + 1 <= c1.k();
-
-        if (!comp.empty() && result) {
-            IF_VERBOSE(10, verbose_stream() << "self-subsume clause " << c2 << " is TBD\n";);
-            return false;
+        unsigned c1_exclusive = c1.size() - common - complement;
+        if (complement > 0 && c1.k() + 1 > c1_exclusive + c2_exclusive + common) {
+            self = true;
+            return true; 
         }
-        return result;
+        return c1.size() - common < c1.k();
     }
 
     /*
@@ -3517,8 +3215,6 @@ namespace sat {
             case pb_t: 
                 s = subsumes(p1, c->to_pb()); 
                 break;
-            case eq_t:
-                break;
             default: 
                 break;
             }
@@ -3582,23 +3278,22 @@ namespace sat {
 
     void ba_solver::clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses) {
         SASSERT(!c1.was_removed());
-        literal_vector slit;
-        clause_use_list::iterator it = m_clause_use_list.get(lit).mk_iterator();
+        clause_use_list& occurs = m_clause_use_list.get(lit);
+        clause_use_list::iterator it = occurs.mk_iterator();
         while (!it.at_end()) {
             clause& c2 = it.curr();
-            if (!c2.was_removed() && subsumes(c1, c2, slit)) {
-                if (slit.empty()) {
+            bool self;
+            if (!c2.was_removed() && subsumes(c1, c2, self)) {
+                if (self) {
+                    // self-subsumption is TBD
+                }
+                else {
                     TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";);
                     removed_clauses.push_back(&c2);
                     ++m_stats.m_num_clause_subsumes;
                     c1.set_learned(false);
-                }
-                else {
-                    IF_VERBOSE(11, verbose_stream() << "self-subsume clause is TBD\n";);
-                    // remove literal slit from c2.
-                    TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";);
-                }
-            }            
+                }            
+            }
             it.next();
         }
     }
@@ -3615,7 +3310,7 @@ namespace sat {
             watched w = *it;
             if (w.is_binary_clause() && is_marked(w.get_literal())) {
                 ++m_stats.m_num_bin_subsumes;
-                // IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
+                IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
                 if (!w.is_learned()) {
                     c1.set_learned(false);
                 }
@@ -3745,15 +3440,6 @@ namespace sat {
                 result->add_xr(lits, x.learned());        
                 break;
             }
-            case eq_t: {
-                eq const& e = cp->to_eq();
-                wlits.reset();
-                for (eliteral w : e) {
-                    wlits.push_back(wliteral(w.weight, w.lit));
-                }
-                result->add_eq(e.lit(), wlits, e.k(), e.learned());
-                break;
-            }
             default:
                 UNREACHABLE();
             }                
@@ -3791,14 +3477,6 @@ namespace sat {
                 }
                 break;
             }
-            case eq_t: {
-                eq const& e = cp->to_eq();
-                for (eliteral w : e) {
-                    ul.insert(w.lit, idx);
-                    ul.insert(~(w.lit), idx);
-                }
-                break;
-            }
             default:
                 UNREACHABLE();
             }                            
@@ -3840,8 +3518,6 @@ namespace sat {
             }
             return weight >= p.k();
         }
-        case eq_t:
-            break;
         default:
             break;
         }
@@ -3963,7 +3639,6 @@ namespace sat {
         case card_t: display(out, c.to_card(), values); break;
         case pb_t: display(out, c.to_pb(), values); break;
         case xr_t: display(out, c.to_xr(), values); break;
-        case eq_t: display(out, c.to_eq(), values); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -4280,13 +3955,6 @@ namespace sat {
                 if (lxr != null_literal) ineq.push(~lxr, offset);
                 break;
             }
-            case eq_t: {
-                eq& e = cnstr.to_eq();
-                ineq.reset(e.k());
-                for (eliteral wl : e) ineq.push(wl.lit, wl.weight);
-                if (e.lit() != null_literal) ineq.push(~e.lit(), e.k());
-                break;
-            }
             default:
                 UNREACHABLE();
                 break;
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index e63cd5333..9b5a31774 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -51,14 +51,12 @@ namespace sat {
         enum tag_t {
             card_t,
             pb_t,
-            xr_t,
-            eq_t
+            xr_t
         };
 
         class card;
         class pb;
         class xr;
-        class eq;
 
         class constraint {
         protected:
@@ -72,9 +70,10 @@ namespace sat {
             size_t         m_obj_size;
             bool           m_learned;
             unsigned       m_id;
+            bool           m_pure;        // is the constraint pure (only positive occurrences)
         public:
             constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): 
-            m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
+            m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {}
             ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
             unsigned id() const { return m_id; }
             tag_t tag() const { return m_tag; }
@@ -95,20 +94,19 @@ namespace sat {
             void set_watch() { m_watch = m_lit; }
             void clear_watch() { m_watch = null_literal; }
             bool is_clear() const { return m_watch == null_literal && m_lit != null_literal; }
+            bool is_pure() const { return m_pure; }
+            void set_pure() { m_pure = true; }
 
             size_t obj_size() const { return m_obj_size; }
             card& to_card();
             pb&  to_pb();
             xr& to_xr();
-            eq& to_eq();
             card const& to_card() const;
             pb const&  to_pb() const;
             xr const& to_xr() const;
-            eq const& to_eq() const;
             bool is_card() const { return m_tag == card_t; }
             bool is_pb() const { return m_tag == pb_t; }
             bool is_xr() const { return m_tag == xr_t; }
-            bool is_eq() const { return m_tag == eq_t; }
             
             virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
             virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
@@ -185,60 +183,6 @@ namespace sat {
             virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
         };
 
-        struct eliteral {
-            unsigned weight;
-            literal  lit;
-            unsigned tweight;
-            literal  tlit;
-            eliteral(unsigned w, literal lit):
-                weight(w), lit(lit), tweight(0), tlit(null_literal)
-            {}
-            eliteral(): weight(0), lit(null_literal), tweight(0), tlit(null_literal) {}
-        };
-        class eq : public constraint {
-            unsigned       m_lo, m_hi, m_max, m_k, m_trail_sz;
-            eliteral       m_wlits[0];
-        public:
-            static size_t get_obj_size(unsigned num_lits) { return sizeof(eq) + num_lits * sizeof(eliteral); }
-            eq(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
-            literal lit() const { return m_lit; }
-            eliteral operator[](unsigned i) const { return m_wlits[i]; }
-            eliteral& operator[](unsigned i) { return m_wlits[i]; }
-            eliteral const* begin() const { return m_wlits; }
-            eliteral const* end() const { return begin() + m_size; }
-            unsigned index(literal l) const;            
-            unsigned k() const { return m_k; }
-            void reset_lo() { m_lo = 0; }
-            void reset_hi() { m_hi = m_max; }
-            unsigned lo() const { return m_lo; }
-            unsigned hi() const { return m_hi; }
-            void inc_hi(unsigned d) { m_hi += d; }
-            void dec_lo(unsigned d) { SASSERT(d <= m_lo); m_lo -= d; }
-            // increment/decrement lo/hi save delta and variable in a trail.
-            void inc_lo(eliteral const& e) { 
-                m_lo += e.weight; 
-                m_wlits[m_trail_sz].tlit = literal(e.lit.var(), false); 
-                m_wlits[m_trail_sz++].tweight = e.weight; 
-            }
-            void dec_hi(eliteral const& e) { 
-                m_hi -= e.weight; 
-                m_wlits[m_trail_sz].tlit = literal(e.lit.var(), true); 
-                m_wlits[m_trail_sz++].tweight = e.weight; 
-            }
-            unsigned trail_sz() const { return m_trail_sz; }
-            void set_trail_sz(unsigned sz) { m_trail_sz = sz; }
-
-            virtual void negate() { SASSERT(lit() != null_literal); m_lit.neg(); }
-            virtual void set_k(unsigned k) { m_k = k; }
-            virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
-            virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.lit); return lits; }
-            virtual bool is_watching(literal l) const { return true; }
-            virtual literal get_lit(unsigned i) const { return m_wlits[i].lit; }
-            virtual void set_lit(unsigned i, literal l) { m_wlits[i].lit = l; }
-            virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].weight; }
-            
-        };
-
         class xr : public constraint {
             literal        m_lits[0];
         public:
@@ -281,8 +225,6 @@ namespace sat {
         unsigned_vector        m_constraint_to_reinit_lim;
         unsigned               m_constraint_to_reinit_last_sz;
         unsigned               m_constraint_id;
-        ptr_vector<eq>         m_eq_to_pop;
-        unsigned_vector        m_eq_to_pop_lim;
 
         // conflict resolution
         unsigned          m_num_marks;
@@ -340,7 +282,7 @@ namespace sat {
         unsigned_vector           m_weights;
         svector<wliteral>         m_wlits;
         bool subsumes(card& c1, card& c2, literal_vector& comp);
-        bool subsumes(card& c1, clause& c2, literal_vector& comp);
+        bool subsumes(card& c1, clause& c2, bool& self);
         bool subsumed(card& c1, literal l1, literal l2);
         bool subsumes(pb const& p1, pb_base const& p2);
         void subsumes(pb& p1, literal lit);
@@ -363,6 +305,7 @@ namespace sat {
         void gc_half(char const* _method);
         void update_psm(constraint& c) const;
         void mutex_reduction();
+        void update_pure();
 
         unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
 
@@ -451,19 +394,6 @@ namespace sat {
         lbool eval(model const& m, pb const& p) const;
         double get_reward(pb const& p, literal_occs_fun& occs) const;
 
-        // eq functionality
-        void pop_eq(eq& e);
-        bool init_watch(eq& e);
-        void clear_watch(eq& e);
-        lbool add_assign(eq& e, literal alit);
-        void get_antecedents(literal l, eq const& e, literal_vector& r);
-        void simplify(eq& e);
-        void recompile(eq& e);
-        void split_root(eq& e);
-        void calibrate(eq& e);
-        lbool eval(eq const& e) const;
-        lbool eval(model const& m, eq const& e) const;
-
         // access solver
         inline lbool value(bool_var v) const { return value(literal(v, false)); }
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
@@ -541,13 +471,11 @@ namespace sat {
         void display(std::ostream& out, card const& c, bool values) const;
         void display(std::ostream& out, pb const& p, bool values) const;
         void display(std::ostream& out, xr const& c, bool values) const;
-        void display(std::ostream& out, eq const& e, bool values) const;
         void display_lit(std::ostream& out, literal l, unsigned sz, bool values) const;
 
         constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
         constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
         constraint* add_xr(literal_vector const& lits, bool learned);
-        constraint* add_eq(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
 
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
@@ -561,7 +489,6 @@ namespace sat {
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xr(literal_vector const& lits);
-        void    add_eq(literal l, svector<wliteral> const& wlits, unsigned k) { add_eq(l, wlits, k, false); }
 
         virtual bool propagate(literal l, ext_constraint_idx idx);
         virtual lbool resolve_conflict();
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 64b1d5e67..8b7c55797 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -87,8 +87,6 @@ namespace sat {
             IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
             if (num_elim == 0)
                 break;
-            if (false && num_elim > 1000) 
-                i = 0;
         }        
         IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) 
                           verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg
index b04b5ff01..5ee140ab9 100644
--- a/src/sat/sat_asymm_branch_params.pyg
+++ b/src/sat/sat_asymm_branch_params.pyg
@@ -2,7 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_asymm_branch_params',
                   export=True,
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
-                          ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
+                          ('asymm_branch.rounds', UINT, 2, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
                           ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
                           ('asymm_branch.sampled', BOOL, True, 'use sampling based asymmetric branching based on binary implication graph'),
                           ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index c820aa4f8..0acc5e7cb 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -169,6 +169,7 @@ namespace sat {
         unsigned idx = 0;
         unsigned elim = 0;
         for (watch_list & wlist : s.m_watches) {
+            if (s.inconsistent()) break;
             literal u = to_literal(idx++);
             watch_list::iterator it     = wlist.begin();
             watch_list::iterator itprev = it;
@@ -179,6 +180,10 @@ namespace sat {
                     literal v = w.get_literal();
                     if (reaches(u, v) && u != get_parent(v)) {
                         ++elim;
+                        if (find_binary_watch(wlist, ~v)) {
+                            IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
+                            s.assign(~u, justification());
+                        }
                         // could turn non-learned non-binary tautology into learned binary.
                         s.get_wlist(~v).erase(watched(~u, w.is_learned()));
                         continue;
@@ -189,6 +194,7 @@ namespace sat {
             }
             wlist.set_end(itprev);
         }
+        s.propagate(false);
         return elim;
     }
 
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 381692654..c37312ae7 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -72,6 +72,10 @@ namespace sat {
         m_num_threads     = p.threads();
         m_local_search    = p.local_search();
         m_local_search_threads = p.local_search_threads();
+        if (p.local_search_mode() == symbol("gsat"))
+            m_local_search_mode = local_search_mode::gsat;
+        else
+            m_local_search_mode = local_search_mode::wsat;
         m_unit_walk       = p.unit_walk();
         m_unit_walk_threads = p.unit_walk_threads();
         m_lookahead_simplify = p.lookahead_simplify();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index d70ae0cb7..b42761f4b 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -73,6 +73,11 @@ namespace sat {
         adaptive_psat_cutoff
     };
 
+    enum local_search_mode {
+        gsat,
+        wsat
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -90,6 +95,7 @@ namespace sat {
         unsigned           m_num_threads;
         unsigned           m_local_search_threads;
         bool               m_local_search;
+        local_search_mode  m_local_search_mode;
         unsigned           m_unit_walk_threads;
         bool               m_unit_walk;
         bool               m_lookahead_simplify;
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index b178c52e2..54a5d54ba 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -223,6 +223,7 @@ namespace sat {
     }
 
     void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
+        TRACE("elim_eqs", tout << "before bin cleanup\n"; m_solver.display(tout););
         cleanup_bin_watches(roots);
         TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););
         cleanup_clauses(roots, m_solver.m_clauses);
@@ -232,5 +233,6 @@ namespace sat {
         save_elim(roots, to_elim);
         m_solver.propagate(false);
         SASSERT(check_clauses(roots));
+        TRACE("elim_eqs", tout << "after full cleanup\n"; m_solver.display(tout););
     }
 };
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 5e5f49eb4..1b5f09e4d 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -72,9 +72,12 @@ namespace sat {
     void local_search::init_cur_solution() {
         for (unsigned v = 0; v < num_vars(); ++v) {
             // use bias with a small probability
-            if (m_rand() % 100 < 2) {
+            if (m_rand() % 10 < 5) {
                 m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
             }
+            else {
+                m_vars[v].m_value = (m_rand() % 2) == 0;
+            }
         }
     }
 
@@ -449,7 +452,6 @@ namespace sat {
         m_best_unsat_rate = 1;
         m_last_best_unsat_rate = 1;
 
-
         reinit();
         timer timer;
         timer.start();
@@ -457,20 +459,23 @@ namespace sat {
         PROGRESS(tries, total_flips);
         
         for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
-            if (m_unsat_stack.size() < m_best_unsat) {
-                m_best_unsat = m_unsat_stack.size();
-                m_last_best_unsat_rate = m_best_unsat_rate;
-                m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
-            }
             for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
                 pick_flip_walksat();
+                if (m_unsat_stack.size() < m_best_unsat) {
+                    m_best_unsat = m_unsat_stack.size();
+                    m_last_best_unsat_rate = m_best_unsat_rate;
+                    m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();                                        
+                }
             }
             total_flips += step;
             PROGRESS(tries, total_flips);
-            if (m_par && tries % 1 == 0) {
-                m_par->get_phase(*this);
+            if (m_par && m_par->get_phase(*this)) {
                 reinit();
             }
+            if (tries % 10 == 0 && !m_unsat_stack.empty()) {
+                reinit();
+            }
+            
         }
     }
 
@@ -490,7 +495,10 @@ namespace sat {
                     if (m_best_objective_value >= m_best_known_value) {
                         break;
                     }
-                }                
+                }          
+                if (m_unsat_stack.size() < m_best_unsat) {
+                    m_best_unsat = m_unsat_stack.size();
+                }
                 flipvar = pick_var_gsat();
                 flip_gsat(flipvar);
                 m_vars[flipvar].m_time_stamp = step++;
@@ -563,6 +571,9 @@ namespace sat {
         unsigned num_unsat = m_unsat_stack.size();
         constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
         SASSERT(c.m_k < constraint_value(c));
+        unsigned reflipped = 0;
+        bool is_core = m_unsat_stack.size() <= 10;
+    reflip:
         // TBD: dynamic noise strategy 
         //if (m_rand() % 100 < 98) {
         if (m_rand() % 10000 <= m_noise) {
@@ -635,6 +646,10 @@ namespace sat {
             }
         }
         flip_walksat(best_var);
+        if (false && is_core && c.m_k < constraint_value(c)) {
+            ++reflipped;
+            goto reflip;
+        }
     }
 
     void local_search::flip_walksat(bool_var flipvar) {
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index b0483c5b9..475bd5f25 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -21,17 +21,13 @@
 
 #include "util/vector.h"
 #include "sat/sat_types.h"
+#include "sat/sat_config.h"
 #include "util/rlimit.h"
 
 namespace sat {
 
     class parallel;
 
-    enum local_search_mode {
-        gsat,
-        wsat
-    };
-
     class local_search_config {
         unsigned m_seed;
         unsigned m_strategy_id;
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index 462439499..8e50a1f91 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -229,7 +229,6 @@ namespace sat {
                     break;
                 }
             }
-            IF_VERBOSE(1, verbose_stream() << "set phase: " << m_num_clauses << " " << s.m_clauses.size() << " " << m_solver_copy << "\n";);
         }
         if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) {
             // time to update local search with new clauses.
@@ -268,10 +267,13 @@ namespace sat {
         }
     }
 
-   void parallel::get_phase(local_search& s) {
+    bool parallel::get_phase(local_search& s) {
+        bool copied = false;
         #pragma omp critical (par_solver)
         {
+            m_consumer_ready = true;
             if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
+                copied = true;
                 s.import(*m_solver_copy.get(), true);
             }
             for (unsigned i = 0; i < m_phase.size(); ++i) {
@@ -280,6 +282,7 @@ namespace sat {
             }
             m_phase.reserve(s.num_vars(), l_undef);
         }
+        return copied;
     }
 
     void parallel::set_phase(local_search& s) {
diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h
index f37c99151..256623380 100644
--- a/src/sat/sat_parallel.h
+++ b/src/sat/sat_parallel.h
@@ -106,7 +106,7 @@ namespace sat {
         
         void set_phase(local_search& s);
 
-        void get_phase(local_search& s);
+        bool get_phase(local_search& s);
 
         bool copy_solver(solver& s);
     };
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index c702941f6..7f6d1f718 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -38,6 +38,7 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
+                          ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
 	                  ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
                           ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
                           ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 3010c92f2..7821b32ca 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -232,6 +232,7 @@ namespace sat {
         if (m_scc_tr) {
             reduce_tr();
         }
+        TRACE("scc_detail", m_solver.display(tout););
         return to_elim.size();
     }
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index c52b36417..be0222d3b 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -198,7 +198,7 @@ namespace sat {
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());
-        TRACE("before_simplifier", s.display(tout););
+        TRACE("sat_simplifier", s.display(tout););
 
         s.m_cleaner(true);
         TRACE("after_cleanup", s.display(tout););
@@ -254,7 +254,7 @@ namespace sat {
         }
 
         CASSERT("sat_solver", s.check_invariant());
-        TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
+        TRACE("sat_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
         finalize();
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8c7450a61..4f2752fe6 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -332,6 +332,14 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
+        if (find_binary_watch(get_wlist(~l1), ~l2)) {
+            assign(l1, justification());
+            return;
+        }
+        if (find_binary_watch(get_wlist(~l2), ~l1)) {
+            assign(l2, justification());
+            return;
+        }
         watched* w0 = find_binary_watch(get_wlist(~l1), l2);
         if (w0) {
             if (w0->is_learned() && !learned) {
@@ -355,7 +363,7 @@ namespace sat {
         }
         m_stats.m_mk_bin_clause++;
         get_wlist(~l1).push_back(watched(l2, learned));
-        get_wlist(~l2).push_back(watched(l1, learned));        
+        get_wlist(~l2).push_back(watched(l1, learned));
     }
 
     bool solver::propagate_bin_clause(literal l1, literal l2) {
@@ -1023,6 +1031,7 @@ namespace sat {
         scoped_limits scoped_rl(rlimit());
         local_search srch;
         srch.config().set_seed(m_config.m_random_seed);
+        srch.config().set_mode(m_config.m_local_search_mode);
         srch.import(*this, false);
         scoped_rl.push_child(&srch.rlimit());
         lbool r = srch.check(num_lits, lits, 0);
@@ -1047,6 +1056,7 @@ namespace sat {
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
             l->config().set_seed(m_config.m_random_seed + i);
+            l->config().set_mode(m_config.m_local_search_mode);
             l->import(*this, false);
             ls.push_back(l);
         }
@@ -1095,7 +1105,7 @@ namespace sat {
                     r = par.get_solver(i).check(num_lits, lits);
                 }
                 else if (IS_LOCAL_SEARCH(i)) {
-                    r = ls[i-local_search_offset]->check(num_lits, lits);
+                    r = ls[i-local_search_offset]->check(num_lits, lits, &par);
                 }
                 else if (IS_UNIT_WALK(i)) {
                     r = uw[i-unit_walk_offset]->check(num_lits, lits);
@@ -1519,9 +1529,9 @@ namespace sat {
 
         m_scc();
         CASSERT("sat_simplify_bug", check_invariant());
-        
-
+      
         m_simplifier(false);
+
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
         if (!m_learned.empty()) {
@@ -1536,6 +1546,7 @@ namespace sat {
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
         m_asymm_branch(false);
+
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
         if (m_ext) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 0f74fac8b..ed8f48762 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -60,7 +60,8 @@ class inc_sat_solver : public solver {
     sat::literal_vector m_asms;
     goal_ref_buffer     m_subgoals;
     proof_converter_ref m_pc;
-    mutable model_converter_ref m_mc0;
+    sref_vector<model_converter> m_mcs;
+    mutable model_converter_ref m_mc0;         // TBD: should be saved/retained under push/pop
     mutable obj_hashtable<func_decl>  m_inserted_const2bits;
     mutable ref<sat2goal::mc>   m_sat_mc;
     mutable model_converter_ref m_cached_mc;
@@ -88,6 +89,7 @@ public:
         m_internalized_converted(false), 
         m_internalized_fmls(m) {
         updt_params(p);
+        m_mcs.push_back(nullptr);
         init_preprocess();
         m_solver.set_incremental(incremental_mode && !override_incremental());
     }
@@ -119,7 +121,7 @@ public:
         for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
         for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
         for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
-        if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
+        if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr));
         if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
         // copy m_bb_rewriter?
         result->m_internalized_converted = m_internalized_converted;
@@ -186,6 +188,7 @@ public:
         if (r != l_true) return r;
 
         init_reason_unknown();
+        m_internalized_converted = false;
         try {
             // IF_VERBOSE(0, m_solver.display(verbose_stream()));
             r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@@ -217,6 +220,7 @@ public:
         internalize_formulas();
         m_solver.user_push();
         ++m_num_scopes;
+        m_mcs.push_back(m_mcs.back());
         m_fmls_lim.push_back(m_fmls.size());
         m_asms_lim.push_back(m_asmsf.size());
         m_fmls_head_lim.push_back(m_fmls_head);
@@ -234,7 +238,9 @@ public:
         SASSERT(n <= m_num_scopes);
         m_solver.user_pop(n);
         m_num_scopes -= n;
+        // ? m_internalized_converted = false;
         while (n > 0) {
+            m_mcs.pop_back();
             m_fmls_head = m_fmls_head_lim.back();
             m_fmls.resize(m_fmls_lim.back());
             m_fmls_lim.pop_back();
@@ -448,12 +454,10 @@ public:
         if (m_cached_mc)
             return m_cached_mc;
         if (is_internalized() && m_internalized_converted) {            
-            insert_const2bits();
             m_sat_mc->flush_smc(m_solver, m_map);
-            m_cached_mc = m_mc0.get();
+            m_cached_mc = m_mcs.back();
             m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
             m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
-            // IF_VERBOSE(0, m_cached_mc->display(verbose_stream() << "get-model-converter\n"););
             return m_cached_mc;
         }
         else {
@@ -493,12 +497,10 @@ public:
         simp2_p.set_bool("elim_and", true);
         simp2_p.set_bool("blast_distinct", true);
         m_preprocess =
-            and_then(mk_card2bv_tactic(m, m_params),
+            and_then(mk_card2bv_tactic(m, m_params),                  // updates model converter
                      using_params(mk_simplify_tactic(m), simp2_p),
                      mk_max_bv_sharing_tactic(m),
-                     mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
-                     //mk_aig_tactic(),
-                     //mk_propagate_values_tactic(m, simp2_p),
+                     mk_bit_blaster_tactic(m, m_bb_rewriter.get()),   // updates model converter
                      using_params(mk_simplify_tactic(m), simp2_p));
         while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
             m_bb_rewriter->push();
@@ -508,22 +510,6 @@ public:
 
 private:
 
-    void insert_const2bits() const {
-        if (!m_bb_rewriter) return;
-        obj_map<func_decl, expr*> to_insert;
-        obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
-        for (auto const& kv : const2bits) {
-            if (!m_inserted_const2bits.contains(kv.m_key)) {
-                m_inserted_const2bits.insert(kv.m_key);
-                to_insert.insert(kv.m_key, kv.m_value);
-            }
-        }
-        if (!to_insert.empty()) {
-            m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, to_insert));
-        }
-    }
-
-
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_pc.reset();
         m_subgoals.reset();
@@ -543,15 +529,15 @@ private:
             m_preprocess = 0;
             m_bb_rewriter = 0;
             return l_undef;
-        }
+        }        
         if (m_subgoals.size() != 1) {
-            IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
+            IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
             return l_undef;
         }
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         m_pc = g->pc();
-        m_mc0 = concat(m_mc0.get(), g->mc());
+        m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
         TRACE("sat", g->display_with_dependencies(tout););
 
         // ensure that if goal is already internalized, then import mc from m_solver.
@@ -591,8 +577,8 @@ private:
     }
 
     lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            internalize_var(vars[i], bvars);
+        for (expr* v : vars) {
+            internalize_var(v, bvars);
         }
         return l_true;
     }
@@ -604,7 +590,6 @@ private:
         bool internalized = false;
         if (is_uninterp_const(v) && m.is_bool(v)) {
             sat::bool_var b = m_map.to_bool_var(v);
-
             if (b != sat::null_bool_var) {
                 bvars.push_back(b);
                 internalized = true;
@@ -614,10 +599,9 @@ private:
             SASSERT(bvutil.is_bv(bv));
             app* abv = to_app(bv);
             internalized = true;
-            unsigned sz = abv->get_num_args();
-            for (unsigned j = 0; j < sz; ++j) {
-                SASSERT(is_uninterp_const(abv->get_arg(j)));
-                sat::bool_var b = m_map.to_bool_var(abv->get_arg(j));
+            for (expr* arg : *abv) {
+                SASSERT(is_uninterp_const(arg));
+                sat::bool_var b = m_map.to_bool_var(arg);
                 if (b == sat::null_bool_var) {
                     internalized = false;
                 }
@@ -625,7 +609,7 @@ private:
                     bvars.push_back(b);
                 }
             }
-            CTRACE("sat", internalized, tout << "var: "; for (unsigned j = 0; j < sz; ++j) tout << bvars[bvars.size()-sz+j] << " "; tout << "\n";);
+            CTRACE("sat", internalized, tout << "var: " << bvars << "\n";);
         }
         else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
             // variable does not occur in assertions, so is unconstrained.
@@ -813,18 +797,18 @@ private:
             //IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
             (*m_sat_mc)(mdl);
         }
-        insert_const2bits();
-        if (m_mc0) {            
+        if (m_mcs.back()) {            
             //IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
-            (*m_mc0)(mdl);
+            (*m_mcs.back())(mdl);
         }
         TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
         
         // IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
 
 #if 0
-        IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
+        IF_VERBOSE(0, verbose_streamm() << "Verifying solution\n";);
         model_evaluator eval(*mdl);
+        bool all_true = true;
         for (expr * f : m_fmls) {
             expr_ref tmp(m);
             eval(f, tmp);
@@ -833,13 +817,20 @@ private:
                    model_smt2_pp(tout, m, *(mdl.get()), 0););
             if (!m.is_true(tmp)) {
                 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
-                IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
-                IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
-                IF_VERBOSE(0, if (m_mc0) m_mc0->display(verbose_stream() << "mc0\n"););
-                break;
+                all_true = false;
+            }
+            else {
+                VERIFY(m.is_true(tmp));                                
             }
-            VERIFY(m.is_true(tmp));                                
         }
+        if (!all_true) {
+            IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
+            IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
+            IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"););
+            //IF_VERBOSE(0, m_solver.display(verbose_stream()));
+            IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n";);
+        }
+
 #endif
     }
 };
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 7323dc6b8..305bed175 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -573,28 +573,6 @@ struct goal2sat::imp {
 
     void convert_eq_k(app* t, rational const& k, bool root, bool sign) {
         SASSERT(k.is_unsigned());
-#if 0
-        IF_VERBOSE(0, verbose_stream() << t->get_id() << ": " << mk_pp(t, m) << "\n";);
-        svector<wliteral> wlits;
-        convert_pb_args(t, wlits);
-        if (root && !sign) {
-            m_ext->add_eq(sat::null_literal, wlits, k.get_unsigned());
-            m_result_stack.reset();
-        }
-        else {
-            sat::bool_var v = m_solver.mk_var();
-            sat::literal l(v, false);
-            m_ext->add_eq(l, wlits, k.get_unsigned());
-            m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_cache.insert(t, l);
-            if (sign) l.neg();
-            m_result_stack.push_back(l);
-            if (root) {
-                mk_clause(l);
-                m_result_stack.reset();
-            }
-        }
-#else
         sat::literal_vector lits;
         convert_pb_args(t->get_num_args(), lits);
         sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
@@ -625,7 +603,6 @@ struct goal2sat::imp {
                 m_result_stack.reset();
             }
         }
-#endif
     }
 
     void ensure_extension() {
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 989427ee7..39300b7dc 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -62,6 +62,7 @@ class bit_blaster_tactic : public tactic {
             TRACE("before_bit_blaster", g->display(tout););
             m_num_steps = 0;
             
+            m_rewriter->start_rewrite();
             expr_ref   new_curr(m());
             proof_ref  new_pr(m());
             unsigned size = g->size();
@@ -78,13 +79,16 @@ class bit_blaster_tactic : public tactic {
                 }
                 if (curr != new_curr) {
                     change = true;                    
-                    TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";);
+                    TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << new_curr << "\n";);
                     g->update(idx, new_curr, new_pr, g->dep(idx));
                 }
             }
             
-            if (change && g->models_enabled())  
-                g->add(mk_bit_blaster_model_converter(m(), m_rewriter->const2bits()));
+            if (change && g->models_enabled()) {
+                obj_map<func_decl, expr*> const2bits;
+                m_rewriter->end_rewrite(const2bits);
+                g->add(mk_bit_blaster_model_converter(m(), const2bits));
+            }
             g->inc_depth();
             result.push_back(g.get());
             TRACE("after_bit_blaster", g->display(tout); if (g->mc()) g->mc()->display(tout); tout << "\n";);
@@ -148,6 +152,7 @@ public:
         return m_imp->get_num_steps();
     }
 
+
 };
 
 
@@ -158,3 +163,4 @@ tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
 tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p) {
     return clean(alloc(bit_blaster_tactic, m, rw, p));
 }
+