diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 0157ca9ff..179773c34 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -610,7 +610,7 @@ struct pb2bv_rewriter::imp {
             m_keep_pb_constraints(false),
             m_pb_num_system(false),
             m_pb_totalizer(false),
-            m_min_arity(3)
+            m_min_arity(9)
         {}
 
         bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@@ -797,7 +797,7 @@ struct pb2bv_rewriter::imp {
             m_trail.push_back(l);
             return l;
         }
-        literal fresh(char const* n) {
+        literal fresh(char const* n) {                      
             expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m);
             m_imp.m_fresh.push_back(to_app(fr)->get_decl());
             return trail(fr);
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index d265ada75..ccc453650 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -47,6 +47,16 @@ 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);
@@ -85,6 +95,15 @@ 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();
         }
@@ -186,6 +205,33 @@ 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
     
@@ -451,7 +497,6 @@ namespace sat {
             // display(verbose_stream(), c, true);
             _bad_id = 11111111;
             SASSERT(p.well_formed());
-            if (p.is_pb()) simplify2(p.to_pb());
             m_simplify_change = true;
         }
     }
@@ -847,28 +892,6 @@ namespace sat {
         }
     }
 
-    void ba_solver::simplify2(pb& p) {
-        return;
-
-        if (p.is_cardinality()) {
-            literal_vector lits(p.literals());
-            unsigned k = (p.k() + p[0].first - 1) / p[0].first;
-            add_at_least(p.lit(), lits, k, p.learned());
-            remove_constraint(p, "simplified to cardinality");
-        }
-        else if (p.lit() == null_literal) {
-            for (wliteral wl : p) {
-                if (p.k() > p.max_sum() - wl.first) {
-                    TRACE("ba", 
-                          tout << "unit literal " << wl.second << "\n";
-                          display(tout, p, true););
-                    
-                    s().assign(wl.second, justification());
-                }
-            }
-        }
-    }
-
     void ba_solver::display(std::ostream& out, pb const& p, bool values) const {
         if (p.lit() != null_literal) out << p.lit() << " == ";
         if (values) {
@@ -902,6 +925,250 @@ 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:
@@ -1245,6 +1512,17 @@ 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;
@@ -1487,7 +1765,7 @@ namespace sat {
     void ba_solver::process_card(card& c, unsigned offset) {
         literal lit = c.lit();
         SASSERT(c.k() <= c.size());       
-        SASSERT(lit == null_literal || value(lit) == l_true);
+        SASSERT(lit == null_literal || value(lit) != l_undef);
         SASSERT(0 < offset);
         for (unsigned i = c.k(); i < c.size(); ++i) {
             process_antecedent(c[i], offset);
@@ -1500,9 +1778,12 @@ namespace sat {
             if (offset1 > UINT_MAX) {
                 m_overflow = true;
             }
-            else {
+            if (value(lit) == l_true) {
                 process_antecedent(~lit, static_cast<unsigned>(offset1));
             }
+            else {
+                process_antecedent(lit, static_cast<unsigned>(offset1));
+            }
         }
     }
 
@@ -1607,6 +1888,7 @@ 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;
@@ -1616,7 +1898,8 @@ namespace sat {
         switch (c.tag()) {
         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 xr_t: return add_assign(c.to_xr(), l);
+        case eq_t: return add_assign(c.to_eq(), l);
         }
         UNREACHABLE();
         return l_undef;
@@ -1667,7 +1950,7 @@ namespace sat {
             init_watch(c);
             return true;
         }
-        else if (c.lit() != null_literal && value(c.lit()) != l_true) {
+        else if (c.lit() != null_literal && value(c.lit()) != l_true && c.tag() != eq_t) {
             return true;
         }
         else {
@@ -1722,6 +2005,7 @@ 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;
         }
     }
@@ -1982,8 +2266,9 @@ namespace sat {
             }
             SASSERT(found););
         
-        if (c.lit() != null_literal) r.push_back(c.lit());
-        SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
+        // IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n");
+        SASSERT(c.lit() == null_literal || value(c.lit()) != l_false);
+        if (c.lit() != null_literal) r.push_back(value(c.lit()) == l_true ? c.lit() : ~c.lit());
         for (unsigned i = c.k(); i < c.size(); ++i) {
             SASSERT(value(c[i]) == l_false);
             r.push_back(~c[i]);
@@ -2033,6 +2318,7 @@ 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;
         }
     }
@@ -2056,6 +2342,9 @@ namespace sat {
         case xr_t:
             clear_watch(c.to_xr());
             break;
+        case eq_t:
+            clear_watch(c.to_eq());
+            break;
         default:
             UNREACHABLE();
         }
@@ -2078,6 +2367,7 @@ 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;
@@ -2093,6 +2383,7 @@ 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;        
@@ -2103,7 +2394,8 @@ namespace sat {
         switch (c.tag()) {
         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 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;        
@@ -2360,6 +2652,10 @@ namespace sat {
 
         SASSERT(0 < bound && bound <= sz);
         if (bound == sz) {
+            if (c.lit() != null_literal && value(c.lit()) == l_undef) {
+                assign(c, ~c.lit());
+                return inconsistent() ? l_false : l_true;
+            }
             set_conflict(c, alit);
             return l_false;
         }
@@ -2391,6 +2687,10 @@ namespace sat {
         // conflict
         if (bound != index && value(c[bound]) == l_false) {
             TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";);
+            if (c.lit() != null_literal && value(c.lit()) == l_undef) {
+                assign(c, ~c.lit());
+                return inconsistent() ? l_false : l_true;
+            }
             set_conflict(c, alit);
             return l_false;
         }
@@ -2403,6 +2703,11 @@ namespace sat {
         if (index != bound) {
             c.swap(index, bound);
         }        
+
+        if (c.lit() != null_literal && value(c.lit()) == l_undef) {
+            return l_true;
+        }
+
         for (unsigned i = 0; i < bound; ++i) {
             assign(c, c[i]);
         }
@@ -2425,6 +2730,7 @@ 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) {        
@@ -2433,6 +2739,13 @@ 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() {
@@ -2451,16 +2764,16 @@ namespace sat {
         SASSERT(s().at_base_lvl());
         switch (c.tag()) {
         case card_t:
-            if (!clausify(c.to_card())) 
-                simplify(c.to_card());
+            simplify(c.to_card());
             break;
         case pb_t:
-            if (!clausify(c.to_pb()))
-                simplify(c.to_pb());
+            simplify(c.to_pb());
             break;
         case xr_t:
-            if (!clausify(c.to_xr()))
-                simplify(c.to_xr());
+            simplify(c.to_xr());
+            break;
+        case eq_t:
+            simplify(c.to_eq());
             break;
         default:
             UNREACHABLE();
@@ -2498,6 +2811,7 @@ namespace sat {
                    << " :gc " << m_stats.m_num_gc
                    << ")\n";);
 
+        // IF_VERBOSE(0, s().display(verbose_stream()));
         // mutex_reduction();
         // if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
 
@@ -2616,6 +2930,9 @@ 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;
@@ -2631,7 +2948,6 @@ namespace sat {
         if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
         // IF_VERBOSE(0, verbose_stream() << c << "\n";);
         m_weights.resize(2*s().num_vars(), 0);
-        // for (unsigned w : m_weights) VERIFY(w == 0);
         for (literal l : c) {
             ++m_weights[l.index()];
         }
@@ -2828,6 +3144,7 @@ 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;
         }
     }
 
@@ -2948,6 +3265,15 @@ 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;
+            }
             }
         }
     }
@@ -2970,6 +3296,8 @@ namespace sat {
                 }
                 break;
             }
+            case eq_t: 
+                break;
             default:
                 break;
             }
@@ -3044,6 +3372,8 @@ namespace sat {
             if (p.k() > 1) subsumption(p);
             break;
         }
+        case eq_t: 
+            break;
         default:
             break;                
         }
@@ -3185,6 +3515,8 @@ namespace sat {
             case pb_t: 
                 s = subsumes(p1, c->to_pb()); 
                 break;
+            case eq_t:
+                break;
             default: 
                 break;
             }
@@ -3413,6 +3745,15 @@ 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();
             }                
@@ -3450,6 +3791,14 @@ 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();
             }                            
@@ -3491,6 +3840,8 @@ namespace sat {
             }
             return weight >= p.k();
         }
+        case eq_t:
+            break;
         default:
             break;
         }
@@ -3555,20 +3906,24 @@ namespace sat {
         out << "\n";
     }
 
-    void ba_solver::display(std::ostream& out, card const& c, bool values) const {
-        if (c.lit() != null_literal) {
+    void ba_solver::display_lit(std::ostream& out, literal lit, unsigned sz, bool values) const {
+        if (lit != null_literal) {
             if (values) {
-                out << c.lit() << "[" << c.size() << "]";
-                out << "@(" << value(c.lit());
-                if (value(c.lit()) != l_undef) {
-                    out << ":" << lvl(c.lit());
+                out << lit << "[" << sz << "]";
+                out << "@(" << value(lit);
+                if (value(lit) != l_undef) {
+                    out << ":" << lvl(lit);
                 }
                 out << "): ";
             }
             else {
-                out << c.lit() << " == ";
+                out << lit << " == ";
             }
         }
+    }
+
+    void ba_solver::display(std::ostream& out, card const& c, bool values) const {
+        display_lit(out, c.lit(), c.size(), values);
         for (unsigned i = 0; i < c.size(); ++i) {
             literal l = c[i];
             out << l;
@@ -3608,6 +3963,7 @@ 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;
         }
     }
@@ -3924,6 +4280,13 @@ 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 390025d63..e63cd5333 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -51,12 +51,14 @@ namespace sat {
         enum tag_t {
             card_t,
             pb_t,
-            xr_t
+            xr_t,
+            eq_t
         };
 
         class card;
         class pb;
         class xr;
+        class eq;
 
         class constraint {
         protected:
@@ -98,12 +100,15 @@ namespace sat {
             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(); }
@@ -180,6 +185,60 @@ 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:
@@ -222,6 +281,8 @@ 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;
@@ -390,6 +451,19 @@ 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); }
@@ -467,10 +541,13 @@ 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);
@@ -484,6 +561,7 @@ 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_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b4f5ffeca..c52b36417 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1052,10 +1052,10 @@ namespace sat {
         // Find literals that are in the intersection of all resolvents with l.
         //
         bool resolution_intersection(literal l, bool adding) {
-            if (!process_var(l.var())) return false;
-            bool first = true;
             reset_intersection();
             m_tautology.reset();
+            if (!process_var(l.var())) return false;
+            bool first = true;
             for (watched & w : s.get_wlist(l)) {
                 // when adding a blocked clause, then all non-learned clauses have to be considered for the
                 // resolution intersection.
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index c6d6b4cac..0f74fac8b 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -60,7 +60,6 @@ class inc_sat_solver : public solver {
     sat::literal_vector m_asms;
     goal_ref_buffer     m_subgoals;
     proof_converter_ref m_pc;
-    model_converter_ref m_mc;
     mutable model_converter_ref m_mc0;
     mutable obj_hashtable<func_decl>  m_inserted_const2bits;
     mutable ref<sat2goal::mc>   m_sat_mc;
@@ -120,7 +119,6 @@ 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_mc) result->m_mc = m_mc->translate(tr);
         if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
         if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
         // copy m_bb_rewriter?
@@ -189,6 +187,7 @@ public:
 
         init_reason_unknown();
         try {
+            // IF_VERBOSE(0, m_solver.display(verbose_stream()));
             r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         }
         catch (z3_exception& ex) {
@@ -526,7 +525,6 @@ private:
 
 
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
-        m_mc.reset();
         m_pc.reset();
         m_subgoals.reset();
         init_preprocess();
@@ -553,7 +551,7 @@ private:
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         m_pc = g->pc();
-        m_mc = g->mc();
+        m_mc0 = concat(m_mc0.get(), g->mc());
         TRACE("sat", g->display_with_dependencies(tout););
 
         // ensure that if goal is already internalized, then import mc from m_solver.
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index d6d6c0892..7323dc6b8 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -491,6 +491,7 @@ struct goal2sat::imp {
     }
 
     void convert_pb_eq(app* t, bool root, bool sign) {
+        IF_VERBOSE(0, verbose_stream() << "pbeq: " << mk_pp(t, m) << "\n";);
         rational k = pb.get_k(t);
         SASSERT(k.is_unsigned());
         svector<wliteral> wlits;
@@ -515,11 +516,13 @@ struct goal2sat::imp {
             mk_clause(~l, l1);
             mk_clause(~l, l2);
             mk_clause(~l1, ~l2, l);
+            m_cache.insert(t, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_result_stack.push_back(sign ? ~l : l);
+            if (sign) l.neg();
+            m_result_stack.push_back(l);
             if (root) {
                 m_result_stack.reset();
-                mk_clause(~l);
+                mk_clause(l);
             }
         }
     }
@@ -535,8 +538,10 @@ struct goal2sat::imp {
         }
         else {
             sat::bool_var v = m_solver.mk_var(true);
-            sat::literal lit(v, sign);
+            sat::literal lit(v, false);
             m_ext->add_at_least(v, lits, k.get_unsigned());
+            m_cache.insert(t, lit);
+            if (sign) lit.neg();
             TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
             m_result_stack.shrink(sz - t->get_num_args());
             m_result_stack.push_back(lit);
@@ -557,15 +562,39 @@ struct goal2sat::imp {
         }
         else {
             sat::bool_var v = m_solver.mk_var(true);
-            sat::literal lit(v, sign);
+            sat::literal lit(v, false);
             m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
+            m_cache.insert(t, lit);
             m_result_stack.shrink(sz - t->get_num_args());
+            if (sign) lit.neg();
             m_result_stack.push_back(lit);
         }        
     }
 
     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);
@@ -587,13 +616,16 @@ struct goal2sat::imp {
             mk_clause(~l, l1);
             mk_clause(~l, l2);
             mk_clause(~l1, ~l2, l);
+            m_cache.insert(t, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_result_stack.push_back(sign ? ~l : l);
+            if (sign) l.neg();
+            m_result_stack.push_back(l);
             if (root) {
-                mk_clause(~l);
+                mk_clause(l);
                 m_result_stack.reset();
             }
         }
+#endif
     }
 
     void ensure_extension() {
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index e598b876d..9f9288753 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -15,24 +15,6 @@ Author:
 
 Notes:
 
---*/
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    lia2card_tactic.cpp
-
-Abstract:
-
-    Convert 0-1 integer variables cardinality constraints to built-in cardinality operator.
-
-Author:
- 
-    Nikolaj Bjorner (nbjorner) 2013-11-5
-
-Notes:
-
 --*/
 #include "util/cooperate.h"
 #include "ast/ast_pp.h"