diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 71980eeab..4f8f2d1d3 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -51,10 +51,17 @@ namespace sat {
         m_max_sum(0) {
         for (unsigned i = 0; i < wlits.size(); ++i) {
             m_wlits[i] = wlits[i];
-            if (m_max_sum + wlits[i].first < m_max_sum) {
+        }
+        update_max_sum();
+    }
+
+    void card_extension::pb::update_max_sum() {
+        m_max_sum = 0;
+        for (unsigned i = 0; i < size(); ++i) {
+            if (m_max_sum + m_wlits[i].first < m_max_sum) {
                 throw default_exception("addition of pb coefficients overflows");
             }
-            m_max_sum += wlits[i].first;
+            m_max_sum += m_wlits[i].first;
         }
     }
 
@@ -196,13 +203,12 @@ namespace sat {
     // pb:
 
     void card_extension::copy_pb(card_extension& result) {
-        for (unsigned i = 0; i < m_pbs.size(); ++i) {
+        for (pb* p : m_pbs) {
             svector<wliteral> wlits;
-            pb& p = *m_pbs[i];
-            for (unsigned i = 0; i < p.size(); ++i) {
-                wlits.push_back(p[i]);
+            for (wliteral w : *p) {
+                wlits.push_back(w);
             }
-            result.add_pb_ge(p.lit(), wlits, p.k());
+            result.add_pb_ge(p->lit(), wlits, p->k());
         }
     }
 
@@ -437,6 +443,151 @@ namespace sat {
         }
     }
 
+    void card_extension::unit_propagation_simplification(literal lit, literal_vector const& lits) {
+        if (lit == null_literal) {
+            for (literal l : lits) {
+                if (value(l) == l_undef) {
+                    s().assign(l, justification());
+                }
+            }
+        }
+        else {
+            // add clauses for: p.lit() <=> conjunction of undef literals
+            SASSERT(value(lit) == l_undef);
+            literal_vector cl;
+            cl.push_back(lit);
+            for (literal l : lits) {
+                if (value(l) == l_undef) {
+                    s().mk_clause(~lit, l);
+                    cl.push_back(~l);
+                }
+            }    
+            s().mk_clause(cl);
+        }
+    }
+
+    bool card_extension::is_cardinality(pb const& p) {
+        if (p.size() == 0) return false;
+        unsigned w = p[0].first;
+        for (unsigned i = 1; i < p.size(); ++i) {
+            if (w != p[i].first) return false;
+        }
+        return true;
+    }
+
+    void card_extension::simplify2(pb& p) {
+        if (is_cardinality(p)) {
+            literal_vector lits(p.literals());
+            unsigned k = (p.k() + p[0].first - 1) / p[0].first;
+            add_at_least(p.lit(), lits, k);
+            remove_constraint(p);
+            return;
+        }
+        if (p.lit() == null_literal) {
+            unsigned max_sum = p.max_sum();
+            unsigned sz = p.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                wliteral wl = p[i];
+                if (p.k() > max_sum - wl.first) {
+                    std::cout << "unit literal\n";
+                }
+            }
+        }
+    }
+
+    void card_extension::simplify(pb& p) {
+        s().pop_to_base_level();
+        if (p.lit() != null_literal && value(p.lit()) == l_false) {
+            return;
+            init_watch(p, !p.lit().sign());
+            std::cout << "pb: flip sign\n";
+        }
+        if (p.lit() != null_literal && value(p.lit()) == l_true) {
+            std::cout << "literal is assigned at base level " << s().at_base_lvl() << "\n";
+            SASSERT(lvl(p.lit()) == 0);
+            nullify_tracking_literal(p);
+        }
+
+        SASSERT(p.lit() == null_literal || value(p.lit()) == l_undef);
+
+        unsigned true_val = 0, slack = 0, num_false = 0;
+        for (wliteral wl : p) {
+            switch (value(wl.second)) {
+            case l_true: true_val += wl.first; break;
+            case l_false: ++num_false; break;
+            default: slack += wl.first; break;
+            }
+        }
+        if (true_val == 0 && num_false == 0) {
+            // no op
+        }
+        else if (true_val >= p.k()) {
+            std::cout << "tautology\n";
+            if (p.lit() != null_literal) {
+                std::cout << "tautology at level 0\n";
+                s().assign(p.lit(), justification());
+            }        
+            remove_constraint(p);
+        }
+        else if (slack + true_val < p.k()) {
+            if (p.lit() != null_literal) {
+                s().assign(~p.lit(), justification());
+            }
+            else {
+                std::cout << "unsat during simplification\n";
+                s().set_conflict(justification());
+            }
+            remove_constraint(p);
+        }
+        else if (slack + true_val == p.k()) {
+            std::cout << "unit propagation\n";
+            literal_vector lits(p.literals());
+            unit_propagation_simplification(p.lit(), lits);
+            remove_constraint(p);
+        }
+        else {
+            std::cout << "pb value at base: " << true_val << " false: " <<  num_false << " size: " << p.size() << " k: " << p.k() << "\n";
+            unsigned sz = p.size();
+            clear_watch(p);
+            for (unsigned i = 0; i < sz; ++i) {
+                if (value(p[i].second) != l_undef) {
+                    --sz;
+                    p.swap(i, sz);
+                    --i;
+                }
+            }
+            std::cout << "new size: " << sz << " old size " << p.size() << "\n";
+            p.update_size(sz);
+            p.update_k(p.k() - true_val);
+            // display(std::cout, c, true);
+            if (p.lit() == null_literal) {
+                init_watch(p, true);
+            }
+            else {
+                SASSERT(value(p.lit()) == l_undef);
+                // c will be watched once c.lit() is assigned.
+            }
+            simplify2(p);
+        }
+    }
+
+    void card_extension::nullify_tracking_literal(pb& p) {
+        if (p.lit() != null_literal) {
+            get_wlist(p.lit()).erase(watched(p.index()));
+            get_wlist(~p.lit()).erase(watched(p.index()));
+            p.nullify_literal();
+        }
+    }
+
+    void card_extension::remove_constraint(pb& p) {
+        clear_watch(p);
+        nullify_tracking_literal(p);
+        m_pbs[index2position(p.index())] = 0;
+        dealloc(&p);   
+    }
+
+
+
     void card_extension::display(std::ostream& out, pb const& p, bool values) const {
         if (p.lit() != null_literal) out << p.lit() << " == ";
         if (p.lit() != null_literal && values) {
@@ -469,13 +620,10 @@ namespace sat {
     // xor:
 
     void card_extension::copy_xor(card_extension& result) {
-        for (unsigned i = 0; i < m_xors.size(); ++i) {
+        for (xor* x : m_xors) {
             literal_vector lits;
-            xor& x = *m_xors[i];
-            for (literal l : x) {
-                lits.push_back(l);
-            }
-            result.add_xor(x.lit(), lits);
+            for (literal l : *x) lits.push_back(l);
+            result.add_xor(x->lit(), lits);
         }
     }
 
@@ -872,7 +1020,7 @@ namespace sat {
         for (unsigned i = 0; 0 <= slack && i < m_active_vars.size(); ++i) { 
             bool_var v = m_active_vars[i];
             int coeff = get_coeff(v);
-            lbool val = m_solver->value(v);
+            lbool val = s().value(v);
             bool is_true = val == l_true;
             bool append = coeff != 0 && val != l_undef && (coeff < 0 == is_true);
             if (append) {
@@ -1004,22 +1152,8 @@ namespace sat {
 
     card_extension::~card_extension() {
         m_stats.reset();
-    }
-
-    void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
-        unsigned index = 4*m_cards.size();
-        SASSERT(is_card_index(index));
-        card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
-        m_cards.push_back(c);
-        if (lit == null_literal) {
-            // it is an axiom.
-            init_watch(*c, true);
-            m_card_axioms.push_back(c);
-        }
-        else {
-            get_wlist(lit).push_back(index);
-            get_wlist(~lit).push_back(index);
-            m_index_trail.push_back(index);
+        while (!m_index_trail.empty()) {
+            clear_index_trail_back();
         }
     }
 
@@ -1028,19 +1162,42 @@ namespace sat {
         add_at_least(lit, lits, k);
     }
 
+    void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
+        unsigned index = 4*m_cards.size();
+        SASSERT(is_card_index(index));
+        card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
+        if (lit != null_literal) s().set_external(lit.var());
+        m_cards.push_back(c);
+        init_watch(*c);
+    }
+   
+    void card_extension::init_watch(card& c) {
+        unsigned index = c.index();
+        literal lit = c.lit();
+        m_index_trail.push_back(index);
+        if (lit == null_literal) {
+            // it is an axiom.
+            init_watch(c, true);
+        }
+        else {
+            get_wlist(lit).push_back(index);
+            get_wlist(~lit).push_back(index);
+        }
+    }
+
     void card_extension::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k) {
         unsigned index = 4*m_pbs.size() + 0x3;
         SASSERT(is_pb_index(index));
         pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
         m_pbs.push_back(p);
+        m_index_trail.push_back(index);
         if (lit == null_literal) {
             init_watch(*p, true);
-            m_pb_axioms.push_back(p);
         }
         else {
+            s().set_external(lit.var());
             get_wlist(lit).push_back(index);
             get_wlist(~lit).push_back(index);
-            m_index_trail.push_back(index);
         }
     }
 
@@ -1059,6 +1216,8 @@ namespace sat {
         SASSERT(is_xor_index(index));
         xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, lit, lits);
         m_xors.push_back(x);
+        s().set_external(lit.var());
+        for (literal l : lits) s().set_external(l.var());
         get_wlist(lit).push_back(index);
         get_wlist(~lit).push_back(index);
         m_index_trail.push_back(index);
@@ -1069,8 +1228,9 @@ namespace sat {
         TRACE("sat", tout << l << " " << idx << "\n";);
         if (is_pb_index(idx)) {
             pb& p = index2pb(idx);
-            if (l.var() == p.lit().var()) {
+            if (p.lit() != null_literal && l.var() == p.lit().var()) {
                 init_watch(p, !l.sign());
+                keep = true;
             }
             else if (p.lit() != null_literal && value(p.lit()) != l_true) {
                 keep = false;
@@ -1081,8 +1241,9 @@ namespace sat {
         }
         else if (is_card_index(idx)) {
             card& c = index2card(idx);
-            if (l.var() == c.lit().var()) {
+            if (c.lit() != null_literal && l.var() == c.lit().var()) {
                 init_watch(c, !l.sign());
+                keep = true;
             }
             else if (c.lit() != null_literal && value(c.lit()) != l_true) {
                 keep = false;
@@ -1263,6 +1424,10 @@ namespace sat {
         }
     }
 
+    void card_extension::simplify(xor& x) {
+        // no-op
+    }
+
     void card_extension::get_card_antecedents(literal l, card const& c, literal_vector& r) {
         DEBUG_CODE(
             bool found = false;
@@ -1313,6 +1478,109 @@ namespace sat {
         }
     }
 
+    void card_extension::nullify_tracking_literal(card& c) {
+        if (c.lit() != null_literal) {
+            get_wlist(c.lit()).erase(watched(c.index()));
+            get_wlist(~c.lit()).erase(watched(c.index()));
+            c.nullify_literal();
+        }
+    }
+
+    void card_extension::remove_constraint(card& c) {
+        clear_watch(c);
+        nullify_tracking_literal(c);
+        m_cards[index2position(c.index())] = 0;
+        dealloc(&c);   
+    }
+
+    void card_extension::simplify(card& c) {
+        SASSERT(c.lit() == null_literal || value(c.lit()) != l_false);
+        if (c.lit() != null_literal && value(c.lit()) == l_false) {
+            std::ofstream ous("unit.txt");
+            s().display(ous);
+            s().display_watches(ous);
+            display(ous, c, true);
+            exit(1);
+            return;
+            init_watch(c, !c.lit().sign());
+            std::cout << "card: flip sign\n";
+        }
+        if (c.lit() != null_literal && value(c.lit()) == l_true) {
+            std::cout << "literal is assigned at base level " << value(c.lit()) << " " << s().at_base_lvl() << "\n";
+            SASSERT(lvl(c.lit()) == 0);
+            nullify_tracking_literal(c);
+        }
+        if (c.lit() == null_literal && c.k() == 1) {            
+            std::cout << "create clause\n";
+            literal_vector lits;
+            for (literal l : c) lits.push_back(l);
+            s().mk_clause(lits);
+            remove_constraint(c);
+            return;
+        }
+
+        SASSERT(c.lit() == null_literal || value(c.lit()) == l_undef);
+
+        unsigned num_true = 0, num_false = 0;
+        for (literal l : c) {
+            switch (value(l)) {
+            case l_true: ++num_true; break;
+            case l_false: ++num_false; break;
+            default: break;
+            }
+        }
+
+        if (num_false + num_true == 0) {
+            // no simplification
+            return;
+        }
+        else if (num_true >= c.k()) {
+            std::cout << "tautology\n";
+            if (c.lit() != null_literal) {
+                std::cout << "tautology at level 0\n";
+                s().assign(c.lit(), justification());                        
+            }
+            remove_constraint(c);
+        }
+        else if (num_false + c.k() > c.size()) {
+            if (c.lit() != null_literal) {
+                std::cout << "falsity at level 0\n";
+                s().assign(~c.lit(), justification());                
+                remove_constraint(c);
+            }
+            else {
+                std::cout << "unsat during simplification\n";
+            }
+        }
+        else if (num_false + c.k() == c.size()) {
+            std::cout << "unit propagations : " << c.size() - num_false - num_true << "\n";
+            literal_vector lits(c.literals());
+            unit_propagation_simplification(c.lit(), lits);
+            remove_constraint(c);
+        }
+        else {
+            std::cout << "literals assigned at base: " << num_true + num_false << " " << c.size() << " k: " << c.k() << "\n";
+            unsigned sz = c.size();
+            clear_watch(c);
+            for (unsigned i = 0; i < sz; ++i) {
+                if (value(c[i]) != l_undef) {
+                    --sz;
+                    c.swap(i, sz);
+                    --i;
+                }
+            }
+            std::cout << "new size: " << sz << " old size " << c.size() << "\n";
+            c.update_size(sz);
+            c.update_k(c.k() - num_true);
+            if (c.lit() == null_literal) {
+                init_watch(c, true);
+            }
+            else {
+                SASSERT(value(c.lit()) == l_undef);
+                // c will be watched once c.lit() is assigned.
+            }
+        }
+    }
 
     lbool card_extension::add_assign(card& c, literal alit) {
         // literal is assigned to false.        
@@ -1380,51 +1648,110 @@ namespace sat {
         m_index_lim.push_back(m_index_trail.size());
     }
 
+    void card_extension::clear_index_trail_back() {
+        unsigned index = m_index_trail.back();
+        m_index_trail.pop_back();
+        if (is_card_index(index)) {
+            card* c = m_cards.back();
+            if (c) {
+                SASSERT(c->index() == index);
+                clear_watch(*c); // can skip during finalization
+                dealloc(c);
+            }
+            m_cards.pop_back();
+        }
+        else if (is_pb_index(index)) {
+            pb* p = m_pbs.back();
+            if (p) {
+                SASSERT(p->index() == index);
+                clear_watch(*p); // can skip during finalization
+                dealloc(p);
+            }
+            m_pbs.pop_back();
+        }
+        else if (is_xor_index(index)) {
+            xor* x = m_xors.back();
+            if (x) {
+                SASSERT(x->index() == index);
+                clear_watch(*x); // can skip during finalization
+                dealloc(x);
+            }
+            m_xors.pop_back();
+        }
+        else {
+            UNREACHABLE();
+        }
+    }
+
     void card_extension::pop(unsigned n) {        
         TRACE("sat_verbose", tout << "pop:" << n << "\n";);
         unsigned new_lim = m_index_lim.size() - n;
         unsigned sz = m_index_lim[new_lim];
         while (m_index_trail.size() > sz) {
-            unsigned index = m_index_trail.back();
-            m_index_trail.pop_back();
-            if (is_card_index(index)) {
-                SASSERT(m_cards.back()->index() == index);
-                clear_watch(*m_cards.back());
-                dealloc(m_cards.back());
-                m_cards.pop_back();
-            }
-            else if (is_pb_index(index)) {
-                SASSERT(m_pbs.back()->index() == index);
-                clear_watch(*m_pbs.back());
-                dealloc(m_pbs.back());
-                m_pbs.pop_back();
-            }
-            else if (is_xor_index(index)) {
-                SASSERT(m_xors.back()->index() == index);
-                clear_watch(*m_xors.back());
-                dealloc(m_xors.back());
-                m_xors.pop_back();
-            }
-            else {
-                UNREACHABLE();
-            }
+            clear_index_trail_back();
         }
         m_index_lim.resize(new_lim);
         m_num_propagations_since_pop = 0;
     }
 
-    void card_extension::simplify() {}
+    void card_extension::simplify() {
+        s().pop_to_base_level();
+        for (card* c : m_cards) {
+            if (c) simplify(*c);
+        }
+        for (pb* p : m_pbs) {
+            if (p) simplify(*p);
+        }
+        for (xor* x : m_xors) {
+            if (x) simplify(*x);
+        }
+        gc();
+    }
+
+    void card_extension::gc() {
+        
+        // remove constraints where indicator literal isn't used.
+        sat::use_list use_list;
+        use_list.init(s().num_vars());
+        svector<bool> var_used(s().num_vars(), false);
+        for (clause* c : s().m_clauses) if (!c->frozen()) use_list.insert(*c);
+        for (card* c : m_cards) if (c) for (literal l : *c) var_used[l.var()] = true;
+        for (pb* p : m_pbs) if (p) for (wliteral wl : *p) var_used[wl.second.var()] = true;
+        for (xor* x : m_xors) if (x) for (literal l : *x) var_used[l.var()] = true;
+        for (card* c : m_cards) {
+            if (c && c->lit() != null_literal && !var_used[c->lit().var()] && use_list.get(c->lit()).empty() && use_list.get(~c->lit()).empty()) {
+                remove_constraint(*c);
+            }
+        }
+        for (pb* p : m_pbs) {
+            if (p && p->lit() != null_literal && !var_used[p->lit().var()] && use_list.get(p->lit()).empty() && use_list.get(~p->lit()).empty()) {
+                remove_constraint(*p);
+            }
+        }
+        // take ownership of interface variables
+        for (card* c : m_cards) if (c && c->lit() != null_literal) var_used[c->lit().var()] = true;
+        for (pb* p : m_pbs) if (p && p->lit() != null_literal) var_used[p->lit().var()] = true;
+        // set variables to be non-external if they are not used in theory constraints.
+        unsigned ext = 0;
+        for (unsigned v = 0; v < s().num_vars(); ++v) {
+            if (s().is_external(v) && !var_used[v]) {
+                s().set_non_external(v);
+                ++ext;
+            }            
+        }
+        std::cout << "non-external variables " << ext << "\n";
+
+    }
+
     void card_extension::clauses_modifed() {}
+
     lbool card_extension::get_phase(bool_var v) { return l_undef; }
 
     void card_extension::copy_card(card_extension& result) {
-        for (unsigned i = 0; i < m_cards.size(); ++i) {
+        for (card* c : m_cards) {
             literal_vector lits;
-            card& c = *m_cards[i];
-            for (unsigned i = 0; i < c.size(); ++i) {
-                lits.push_back(c[i]);
-            }
-            result.add_at_least(c.lit(), lits, c.k());
+            for (literal l : *c) lits.push_back(l);
+            result.add_at_least(c->lit(), lits, c->k());
         }
     }
     extension* card_extension::copy(solver* s) {
@@ -1537,13 +1864,13 @@ namespace sat {
 
     std::ostream& card_extension::display(std::ostream& out) const {
         for (card* c : m_cards) {
-            display(out, *c, false);
+            if (c) display(out, *c, false);
         }
         for (pb* p : m_pbs) {
-            display(out, *p, false);
+            if (p) display(out, *p, false);
         }
         for (xor* x : m_xors) {
-            display(out, *x, false);
+            if (x) display(out, *x, false);
         }
         return out;
     }
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index 37b368e70..64553795b 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -59,10 +59,16 @@ namespace sat {
             unsigned index() const { return m_index; }
             literal lit() const { return m_lit; }
             literal operator[](unsigned i) const { return m_lits[i]; }
+            literal const* begin() const { return m_lits; }
+            literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
             unsigned k() const { return m_k; }
             unsigned size() const { return m_size; }
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
-            void negate();                       
+            void negate();                     
+            void update_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; }
+            void update_k(unsigned k) { m_k = k; }
+            void nullify_literal() { m_lit = null_literal; }
+            literal_vector literals() const { return literal_vector(m_size, m_lits); }
         };
         
         typedef std::pair<unsigned, literal> wliteral;
@@ -76,6 +82,7 @@ namespace sat {
             unsigned       m_num_watch;
             unsigned       m_max_sum;
             wliteral       m_wlits[0];
+            void update_max_sum();
         public:
             static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
             pb(unsigned index, literal lit, svector<wliteral> const& wlits, unsigned k);
@@ -83,7 +90,7 @@ namespace sat {
             literal lit() const { return m_lit; }
             wliteral operator[](unsigned i) const { return m_wlits[i]; }
             wliteral const* begin() const { return m_wlits; }
-            wliteral const* end() const { return (wliteral const*)m_wlits + m_size; }
+            wliteral const* end() const { return static_cast<wliteral const*>(m_wlits) + m_size; }
 
             unsigned k() const { return m_k; }
             unsigned size() const { return m_size; }
@@ -94,6 +101,10 @@ namespace sat {
             void set_num_watch(unsigned s) { m_num_watch = s; }
             void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
             void negate();                       
+            void update_size(unsigned sz) { m_size = sz; update_max_sum(); }
+            void update_k(unsigned k) { m_k = k; }            
+            void nullify_literal() { m_lit = null_literal; }
+            literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
         };
 
         class xor {
@@ -109,7 +120,7 @@ namespace sat {
             literal operator[](unsigned i) const { return m_lits[i]; }
             unsigned size() const { return m_size; }
             literal const* begin() const { return m_lits; }
-            literal const* end() const { return (literal const*)m_lits + m_size; }
+            literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
             void negate() { m_lits[0].neg(); }
         };
@@ -131,9 +142,6 @@ namespace sat {
         ptr_vector<xor>     m_xors;
         ptr_vector<pb>      m_pbs;
 
-        scoped_ptr_vector<card> m_card_axioms;
-        scoped_ptr_vector<pb>   m_pb_axioms;
-
         // watch literals
         unsigned_vector     m_index_trail;
         unsigned_vector     m_index_lim;       
@@ -157,7 +165,14 @@ namespace sat {
         void     inc_parity(bool_var v);
         void     reset_parity(bool_var v);
 
+        void clear_index_trail_back();
+
         solver& s() const { return *m_solver; }
+
+        void gc();
+
+        // cardinality
+        void init_watch(card& c);
         void init_watch(card& c, bool is_true);
         void init_watch(bool_var v);
         void assign(card& c, literal lit);
@@ -170,6 +185,10 @@ namespace sat {
         void unwatch_literal(literal w, card& c);
         void get_card_antecedents(literal l, card const& c, literal_vector & r);
         void copy_card(card_extension& result);
+        void simplify(card& c);
+        void nullify_tracking_literal(card& c);
+        void remove_constraint(card& c);
+        void unit_propagation_simplification(literal lit, literal_vector const& lits);
 
         // xor specific functionality
         void copy_xor(card_extension& result);
@@ -177,17 +196,19 @@ namespace sat {
         void watch_literal(xor& x, literal lit);
         void unwatch_literal(literal w, xor& x);
         void init_watch(xor& x, bool is_true);
-        void assign(xor& x, literal lit);
+        void assign(xor& x, literal lit);        
         void set_conflict(xor& x, literal lit);
         bool parity(xor const& x, unsigned offset) const;
         lbool add_assign(xor& x, literal alit);
         void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
         void get_xor_antecedents(literal l, xor const& x, literal_vector & r);
+        void simplify(xor& x);
 
 
         bool is_card_index(unsigned idx) const { return 0x0 == (idx & 0x3); }
         bool is_xor_index(unsigned idx) const { return 0x1 == (idx & 0x3); }
         bool is_pb_index(unsigned idx) const { return 0x3 == (idx & 0x3); }
+        unsigned index2position(unsigned idx) const { return idx >> 2; }
         card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; }
         xor& index2xor(unsigned idx) const { SASSERT(is_xor_index(idx)); return *m_xors[idx >> 2]; }
         pb&  index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pbs[idx >> 2]; }
@@ -205,6 +226,11 @@ namespace sat {
         void assign(pb& p, literal l);
         void unwatch_literal(literal w, pb& p);
         void get_pb_antecedents(literal l, pb const& p, literal_vector & r);
+        void simplify(pb& p);
+        void simplify2(pb& p);
+        bool is_cardinality(pb const& p);
+        void nullify_tracking_literal(pb& p);
+        void remove_constraint(pb& p);
 
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
         inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 8901c276f..81de935b1 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -32,6 +32,13 @@ namespace sat {
     void model_converter::reset() {
         m_entries.finalize();
     }
+
+    model_converter& model_converter::operator=(model_converter const& other) {
+        reset();
+        m_entries.append(other.m_entries);
+        return *this;
+    }
+
     
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index b89e6e784..e35f2a0aa 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -59,6 +59,7 @@ namespace sat {
         model_converter();
         ~model_converter();
         void operator()(model & m) const;
+        model_converter& operator=(model_converter const& other);
 
         entry & mk(kind k, bool_var v);
         void insert(entry & e, clause const & c);
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b53b920dd..4750f8e76 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -35,10 +35,6 @@ namespace sat {
     void use_list::insert(clause & c) {
         unsigned sz = c.size();
         for (unsigned i = 0; i < sz; i++) {
-            if (m_use_list.size() <= c[i].index()) {
-                std::cout << c[i] << "\n";
-                std::cout << m_use_list.size() << "\n";
-            }
             m_use_list[c[i].index()].insert(c);
         }
     }
@@ -86,14 +82,11 @@ namespace sat {
 
     void simplifier::register_clauses(clause_vector & cs) {
         std::stable_sort(cs.begin(), cs.end(), size_lt());
-        clause_vector::iterator it  = cs.begin();
-        clause_vector::iterator end = cs.end();
-        for (; it != end; ++it) {
-            clause & c = *(*it);
-            if (!c.frozen()) {
-                m_use_list.insert(c);
-                if (c.strengthened())
-                    m_sub_todo.insert(c);
+        for (clause* c : cs) {
+            if (!c->frozen()) {
+                m_use_list.insert(*c);
+                if (c->strengthened())
+                    m_sub_todo.insert(*c);
             }
         }
     }
@@ -1358,16 +1351,12 @@ namespace sat {
         TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
         unsigned before_clauses = num_pos + num_neg;
         unsigned after_clauses  = 0;
-        clause_wrapper_vector::iterator it1  = m_pos_cls.begin();
-        clause_wrapper_vector::iterator end1 = m_pos_cls.end();
-        for (; it1 != end1; ++it1) {
-            clause_wrapper_vector::iterator it2  = m_neg_cls.begin();
-            clause_wrapper_vector::iterator end2 = m_neg_cls.end();
-            for (; it2 != end2; ++it2) {
+        for (clause_wrapper& c1 : m_pos_cls) {
+            for (clause_wrapper& c2 : m_neg_cls) {
                 m_new_cls.reset();
-                if (resolve(*it1, *it2, pos_l, m_new_cls)) {
-                    TRACE("resolution_detail", tout << *it1 << "\n" << *it2 << "\n-->\n";
-                          for (unsigned i = 0; i < m_new_cls.size(); i++) tout << m_new_cls[i] << " "; tout << "\n";);
+                if (resolve(c1, c2, pos_l, m_new_cls)) {
+                    TRACE("resolution_detail", tout << c1 << "\n" << c2 << "\n-->\n";
+                          for (literal l : m_new_cls) tout << l << " "; tout << "\n";);
                     after_clauses++;
                     if (after_clauses > before_clauses) {
                         TRACE("resolution", tout << "too many after clauses: " << after_clauses << "\n";);
@@ -1393,16 +1382,12 @@ namespace sat {
 
         m_elim_counter -= num_pos * num_neg + before_lits;
 
-        it1  = m_pos_cls.begin();
-        end1 = m_pos_cls.end();
-        for (; it1 != end1; ++it1) {
-            clause_wrapper_vector::iterator it2  = m_neg_cls.begin();
-            clause_wrapper_vector::iterator end2 = m_neg_cls.end();
-            for (; it2 != end2; ++it2) {
+        for (auto & c1 : m_pos_cls) {
+            for (auto & c2 : m_neg_cls) {
                 m_new_cls.reset();
-                if (!resolve(*it1, *it2, pos_l, m_new_cls))
+                if (!resolve(c1, c2, pos_l, m_new_cls))
                     continue;
-                TRACE("resolution_new_cls", tout << *it1 << "\n" << *it2 << "\n-->\n" << m_new_cls << "\n";);
+                TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
                 if (cleanup_clause(m_new_cls))
                     continue; // clause is already satisfied.
                 switch (m_new_cls.size()) {
@@ -1470,7 +1455,7 @@ namespace sat {
         for (bool_var v : vars) {
             checkpoint();
             if (m_elim_counter < 0)
-                return;
+                break;
             if (try_eliminate(v)) {
                 m_num_elim_vars++;
             }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 405b44b21..2aa944087 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -66,6 +66,7 @@ namespace sat {
     }
 
     solver::~solver() {
+		m_ext = 0;
         SASSERT(check_invariant());
         TRACE("sat", tout << "Delete clauses\n";);
         del_clauses(m_clauses.begin(), m_clauses.end());
@@ -159,6 +160,7 @@ namespace sat {
         m_user_scope_literals.reset();
         m_user_scope_literals.append(src.m_user_scope_literals);
 
+        m_mc = src.m_mc;
     }
 
     // -----------------------
@@ -198,6 +200,10 @@ namespace sat {
         return v;
     }
 
+    void solver::set_non_external(bool_var v) {
+        m_external[v] = false;
+    }
+
     void solver::set_external(bool_var v) {
         if (m_external[v]) return;
         m_external[v] = true;
@@ -1444,6 +1450,20 @@ namespace sat {
             if (m_next_simplify > m_conflicts_since_init + m_config.m_simplify_max)
                 m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max;
         }
+
+#if 1
+        static unsigned file_no = 0;
+        #pragma omp critical (print_sat)
+        {
+            ++file_no;
+            std::ostringstream ostrm;
+            ostrm << "s" << file_no << ".txt";
+            std::ofstream ous(ostrm.str());
+            display(ous);
+        }
+#endif
+
+
     }
 
     void solver::sort_watch_lits() {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 0dcd9837f..c534ae828 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -274,6 +274,7 @@ namespace sat {
         unsigned num_restarts() const { return m_restarts; }
         bool is_external(bool_var v) const { return m_external[v] != 0; }
         void set_external(bool_var v);
+        void set_non_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 295a04a67..febe171d1 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -113,6 +113,17 @@ public:
         if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
         result->m_internalized = m_internalized;
         result->m_internalized_converted = m_internalized_converted;
+#if 0
+        static unsigned file_no = 0;
+        #pragma omp critical (print_sat)
+        {
+            ++file_no;
+            std::ostringstream ostrm;
+            ostrm << "s" << file_no << ".txt";
+            std::ofstream ous(ostrm.str());
+            result->m_solver.display(ous);
+        }
+#endif
         return result;
     }
 
@@ -538,7 +549,7 @@ private:
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         TRACE("sat", g->display_with_dependencies(tout););
-        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true, is_lemma);
+        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
             std::stringstream strm;
diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp
index b00f17c38..1b294351f 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -60,7 +60,7 @@ namespace sat {
                 out << "(" << it->get_blocked_literal() << " " << *(ca.get_clause(it->get_clause_offset())) << ")";
                 break;
             case watched::EXT_CONSTRAINT:
-                out << it->get_ext_constraint_idx();
+                out << "ext: " << it->get_ext_constraint_idx();
                 break;
             default: 
                 UNREACHABLE();