diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt
index d88a73708..41051fd40 100644
--- a/contrib/cmake/src/sat/CMakeLists.txt
+++ b/contrib/cmake/src/sat/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(sat
   SOURCES
+    card_extension.cpp
     dimacs.cpp
     sat_asymm_branch.cpp
     sat_clause.cpp
diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
new file mode 100644
index 000000000..985579f18
--- /dev/null
+++ b/src/sat/card_extension.cpp
@@ -0,0 +1,686 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    card_extension.cpp
+
+Abstract:
+
+    Extension for cardinality reasoning.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-01-30
+
+Revision History:
+
+--*/
+
+#include"card_extension.h"
+#include"sat_types.h"
+
+namespace sat {
+
+    card_extension::card::card(unsigned index, literal lit, literal_vector const& lits, unsigned k):
+        m_index(index),
+        m_lit(lit),
+        m_k(k),
+        m_size(lits.size()), 
+        m_lits(lits) {
+    }
+
+    void card_extension::card::negate() {
+        m_lit.neg();
+        for (unsigned i = 0; i < m_size; ++i) {
+            m_lits[i].neg();
+        }
+        m_k = m_size - m_k + 1;
+        SASSERT(m_size >= m_k && m_k > 0);
+    }
+
+    void card_extension::init_watch(bool_var v) {
+        if (m_var_infos.size() <= static_cast<unsigned>(v)) {
+            m_var_infos.resize(static_cast<unsigned>(v)+100);
+        }
+    }
+
+    void card_extension::init_watch(card& c, bool is_true) {
+        clear_watch(c);
+        if (c.lit().sign() == is_true) {
+            c.negate();
+        }
+        SASSERT(s().value(c.lit()) == l_true);
+        unsigned j = 0, sz = c.size(), bound = c.k();
+        if (bound == sz) {
+            for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
+                assign(c, c[i]);
+            }
+            return;
+        }
+        // put the non-false literals into the head.
+        for (unsigned i = 0; i < sz; ++i) {
+            if (s().value(c[i]) != l_false) {
+                if (j != i) {
+                    c.swap(i, j);
+                }
+                ++j;
+            }
+        }
+        DEBUG_CODE(
+            bool is_false = false;
+            for (unsigned k = 0; k < sz; ++k) {
+                SASSERT(!is_false || s().value(c[k]) == l_false);
+                is_false = s().value(c[k]) == l_false;
+            });
+
+        // j is the number of non-false, sz - j the number of false.
+        if (j < bound) {
+            SASSERT(0 < bound && bound < sz);
+            literal alit = c[j];
+            
+            //
+            // we need the assignment level of the asserting literal to be maximal.
+            // such that conflict resolution can use the asserting literal as a starting
+            // point.
+            //
+
+            for (unsigned i = bound; i < sz; ++i) {                
+                if (s().lvl(alit) < s().lvl(c[i])) {
+                    c.swap(i, j);
+                    alit = c[j];
+                }
+            }
+            set_conflict(c, alit);
+        }
+        else if (j == bound) {
+            for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
+                assign(c, c[i]);                
+            }
+        }
+        else {
+            for (unsigned i = 0; i <= bound; ++i) {
+                watch_literal(c, c[i]);
+            }
+        }
+    }
+
+    void card_extension::clear_watch(card& c) {
+        unsigned sz = std::min(c.k() + 1, c.size());
+        for (unsigned i = 0; i < sz; ++i) {
+            unwatch_literal(c[i], &c);            
+        }
+    }
+
+    void card_extension::unwatch_literal(literal lit, card* c) {
+        if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
+            return;
+        }
+        ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
+        if (cards) {
+            remove(*cards, c);        
+        }
+    }
+
+    void card_extension::remove(ptr_vector<card>& cards, card* c) {
+        for (unsigned j = 0; j < cards.size(); ++j) {
+            if (cards[j] == c) {                        
+                std::swap(cards[j], cards[cards.size()-1]);
+                cards.pop_back();
+                break;
+            }
+        }
+    }
+
+    void card_extension::assign(card& c, literal lit) {
+        if (s().value(lit) == l_true) {
+            return;
+        }
+        m_stats.m_num_propagations++;
+        //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
+        SASSERT(validate_unit_propagation(c));
+        s().assign(lit, justification::mk_ext_justification(c.index()));
+        
+    }
+
+    void card_extension::watch_literal(card& c, literal lit) {
+        init_watch(lit.var());
+        ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
+        if (cards == 0) {
+            cards = alloc(ptr_vector<card>);
+            m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
+        }
+        cards->push_back(&c);
+    }
+
+    void card_extension::set_conflict(card& c, literal lit) {
+        SASSERT(validate_conflict(c));
+        literal_vector& lits = get_literals();
+        SASSERT(s().value(lit) == l_false);
+        SASSERT(s().value(c.lit()) == l_true);
+        lits.push_back(~c.lit()); 
+        lits.push_back(lit);
+        unsigned sz = c.size();
+        for (unsigned i = c.k(); i < sz; ++i) {
+            SASSERT(s().value(c[i]) == l_false);
+            lits.push_back(c[i]);
+        }
+
+        m_stats.m_num_conflicts++;
+        if (!resolve_conflict(c, lits)) {
+            s().mk_clause_core(lits.size(), lits.c_ptr(), true);
+        }
+        SASSERT(s().inconsistent());
+    }
+    
+    void card_extension::normalize_active_coeffs() {
+        while (!m_active_var_set.empty()) m_active_var_set.erase();
+        unsigned i = 0, j = 0, sz = m_active_vars.size();
+        for (; i < sz; ++i) {
+            bool_var v = m_active_vars[i];
+            if (!m_active_var_set.contains(v) && get_coeff(v) != 0) {
+                m_active_var_set.insert(v);
+                if (j != i) {
+                    m_active_vars[j] = m_active_vars[i];
+                }
+                ++j;
+            }
+        }
+        sz = j;
+        m_active_vars.shrink(sz);
+    }
+
+    void card_extension::inc_coeff(literal l, int offset) {
+        SASSERT(offset > 0);
+        bool_var v = l.var();
+        SASSERT(v != null_bool_var);
+        if (static_cast<bool_var>(m_coeffs.size()) <= v) {
+            m_coeffs.resize(v + 1, 0);
+        }
+        int coeff0 = m_coeffs[v];
+        if (coeff0 == 0) {
+            m_active_vars.push_back(v);
+        }
+        
+        int inc = l.sign() ? -offset : offset;
+        int coeff1 = inc + coeff0;
+        m_coeffs[v] = coeff1;
+
+        if (coeff0 > 0 && inc < 0) {
+            m_bound -= coeff0 - std::max(0, coeff1);
+        }
+        else if (coeff0 < 0 && inc > 0) {
+            m_bound -= std::min(0, coeff1) - coeff0;
+        }
+    }
+
+    int card_extension::get_coeff(bool_var v) const {
+        return m_coeffs.get(v, 0);
+    }
+
+    int card_extension::get_abs_coeff(bool_var v) const {
+        int coeff = get_coeff(v);
+        if (coeff < 0) coeff = -coeff;
+        return coeff;
+    }
+
+    void card_extension::reset_coeffs() {
+        for (unsigned i = 0; i < m_active_vars.size(); ++i) {
+            m_coeffs[m_active_vars[i]] = 0;
+        }
+        m_active_vars.reset();
+    }
+
+    bool card_extension::resolve_conflict(card& c, literal_vector const& conflict_clause) {
+
+        bool_var v;
+        m_conflict_lvl = 0;
+        for (unsigned i = 0; i < c.size(); ++i) {
+            literal lit = c[i];
+            SASSERT(s().value(lit) == l_false);
+            m_conflict_lvl = std::max(m_conflict_lvl, s().lvl(lit));
+        }
+        if (m_conflict_lvl < s().lvl(c.lit()) || m_conflict_lvl == 0) {
+            return false;
+        }
+
+        reset_coeffs();
+        m_num_marks = 0;
+        m_bound = c.k();
+        m_conflict.reset();
+        literal_vector const& lits = s().m_trail;
+        unsigned idx = lits.size()-1;
+        justification js;
+        literal consequent = ~conflict_clause[1];
+        process_card(c, 1);
+        literal alit;
+
+        while (m_num_marks > 0) {
+
+            v = consequent.var();
+
+            int offset = get_abs_coeff(v);
+
+            if (offset == 0) {
+                goto process_next_resolvent;            
+            }
+            if (offset > 1000) {
+                goto bail_out;
+            }
+
+            SASSERT(offset > 0);
+
+            js = s().m_justification[v];
+            
+            int bound = 1;            
+            switch(js.get_kind()) {
+            case justification::NONE:
+                break;
+            case justification::BINARY:
+                inc_coeff(consequent, offset);
+                process_antecedent(~(js.get_literal()), offset);
+                break;
+            case justification::TERNARY:
+                inc_coeff(consequent, offset);
+                process_antecedent(~(js.get_literal1()), offset);
+                process_antecedent(~(js.get_literal2()), offset);
+                break;
+            case justification::CLAUSE: {
+                inc_coeff(consequent, offset);
+                clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
+                unsigned i   = 0;
+                if (consequent != null_literal) {
+                    SASSERT(c[0] == consequent || c[1] == consequent);
+                    if (c[0] == consequent) {
+                        i = 1;
+                    }
+                    else {
+                        process_antecedent(~c[0], offset);
+                        i = 2;
+                    }
+                }
+                unsigned sz  = c.size();
+                for (; i < sz; i++)
+                    process_antecedent(~c[i], offset);
+                break;
+            }
+            case justification::EXT_JUSTIFICATION: {
+                unsigned index = js.get_ext_justification_idx();
+                card& c2 = *m_constraints[index];
+                process_card(c2, offset);
+                bound = c2.k();
+                break;
+            }
+            default:
+                UNREACHABLE();
+                break;
+            }
+            m_bound += offset * bound;
+
+            // cut();
+
+        process_next_resolvent:
+            
+            // find the next marked variable in the assignment stack
+            //
+            while (true) {
+                consequent = lits[idx];
+                v = consequent.var();
+                if (s().is_marked(v)) break;
+                SASSERT(idx > 0);
+                --idx;
+            }
+            
+            SASSERT(s().lvl(v) == m_conflict_lvl);
+            s().reset_mark(v);
+            --idx;
+            --m_num_marks;
+        }        
+        
+        SASSERT(validate_lemma());
+
+        normalize_active_coeffs();
+
+        if (m_bound > 0 && m_active_vars.empty()) {
+            return false;
+        }
+
+        int slack = -m_bound;
+        for (unsigned i = 0; i < m_active_vars.size(); ++i) { 
+            bool_var v = m_active_vars[i];
+            slack += get_abs_coeff(v);
+        }
+        
+        alit = get_asserting_literal(~consequent);
+        slack -= get_abs_coeff(alit.var());
+        m_conflict.push_back(alit);
+
+        for (unsigned i = lits.size(); 0 <= slack && i > 0; ) {
+            --i;
+            literal lit = lits[i];
+            bool_var v = lit.var();
+            if (m_active_var_set.contains(v) && v != alit.var()) {
+                int coeff = get_coeff(v);
+                if (coeff < 0 && !lit.sign()) {
+                    slack += coeff;
+                    m_conflict.push_back(~lit);
+                }
+                else if (coeff > 0 && lit.sign()) {
+                    slack -= coeff;
+                    m_conflict.push_back(~lit);
+                }
+            }
+        }
+        SASSERT(slack < 0);
+        SASSERT(validate_conflict(m_conflict));
+        
+        s().mk_clause_core(m_conflict.size(), m_conflict.c_ptr(), true);
+        return true;
+
+    bail_out:
+        while (m_num_marks > 0 && idx > 0) {
+            v = lits[idx].var();
+            if (s().is_marked(v)) {
+                s().reset_mark(v);
+            }
+            --idx;
+        }
+        return false;
+    }
+
+    void card_extension::process_card(card& c, int offset) {
+        SASSERT(c.k() <= c.size());
+        SASSERT(s().value(c.lit()) == l_true);
+        for (unsigned i = c.k(); i < c.size(); ++i) {
+            process_antecedent(c[i], offset);
+        }
+        for (unsigned i = 0; i < c.k(); ++i) {
+            inc_coeff(c[i], offset);                        
+        }
+        if (s().lvl(c.lit()) > 0) {
+            m_conflict.push_back(~c.lit());
+        }
+    }
+
+    void card_extension::process_antecedent(literal l, int offset) {
+        SASSERT(s().value(l) == l_false);
+        bool_var v = l.var();
+        unsigned lvl = s().lvl(v);
+
+        if (lvl > 0 && !s().is_marked(v) && lvl == m_conflict_lvl) {
+            s().mark(v);
+            ++m_num_marks;
+        }
+        inc_coeff(l, offset);                
+    }   
+
+    literal card_extension::get_asserting_literal(literal p) {
+        if (get_abs_coeff(p.var()) != 0) {
+            return p;
+        }
+        unsigned lvl = 0;        
+        for (unsigned i = 0; i < m_active_vars.size(); ++i) { 
+            bool_var v = m_active_vars[i];
+            literal lit(v, get_coeff(v) < 0);
+            if (s().value(lit) == l_false && s().lvl(lit) > lvl) {
+                p = lit;
+            }
+        }
+        return p;        
+    }
+
+    card_extension::card_extension(): m_solver(0) {}
+
+    card_extension::~card_extension() {
+        for (unsigned i = 0; i < m_var_infos.size(); ++i) {
+            m_var_infos[i].reset();
+        }
+        m_var_trail.reset();
+        m_var_lim.reset();
+        m_stats.reset();
+    }
+
+    void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
+        unsigned index = m_constraints.size();
+        card* c = alloc(card, index, literal(v, false), lits, k);
+        m_constraints.push_back(c);
+        init_watch(v);
+        m_var_infos[v].m_card = c;
+        m_var_trail.push_back(v);
+    }
+
+    void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
+        UNREACHABLE();
+    }
+
+    void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
+        card& c = *m_constraints[idx];
+
+        DEBUG_CODE(
+            bool found = false;
+            for (unsigned i = 0; !found && i < c.k(); ++i) {
+                found = c[i] == l;
+            }
+            SASSERT(found););
+
+        for (unsigned i = c.k(); i < c.size(); ++i) {
+            SASSERT(s().value(c[i]) == l_false);
+            r.push_back(c[i]);
+        }
+    }
+
+    lbool card_extension::add_assign(card& c, literal alit) {
+        // literal is assigned to false.        
+        unsigned sz = c.size();
+        unsigned bound = c.k();
+        TRACE("pb", tout << "assign: " << c.lit() << " " << ~alit << " " << bound << "\n";);
+
+        SASSERT(0 < bound && bound < sz);
+        SASSERT(s().value(alit) == l_false);
+        SASSERT(s().value(c.lit()) == l_true);
+        unsigned index = 0;
+        for (index = 0; index <= bound; ++index) {
+            if (c[index] == alit) {
+                break;
+            }
+        }
+        if (index == bound + 1) {
+            // literal is no longer watched.
+            return l_undef;
+        }
+        SASSERT(index <= bound);
+        SASSERT(c[index] == alit);
+        
+        // find a literal to swap with:
+        for (unsigned i = bound + 1; i < sz; ++i) {
+            literal lit2 = c[i];
+            if (s().value(lit2) != l_false) {
+                c.swap(index, i);
+                watch_literal(c, lit2);
+                return l_undef;
+            }
+        }
+
+        // conflict
+        if (bound != index && s().value(c[bound]) == l_false) {
+            TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
+            set_conflict(c, alit);
+            return l_false;
+        }
+
+        TRACE("pb", tout << "no swap " << index << " " << alit << "\n";);
+        // there are no literals to swap with,
+        // prepare for unit propagation by swapping the false literal into 
+        // position bound. Then literals in positions 0..bound-1 have to be
+        // assigned l_true.
+        if (index != bound) {
+            c.swap(index, bound);
+        }
+        SASSERT(validate_unit_propagation(c));
+        
+        for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
+            assign(c, c[i]);
+        }
+
+        return s().inconsistent() ? l_false : l_true;
+    }
+
+    void card_extension::asserted(literal l) {
+        bool_var v = l.var();
+        ptr_vector<card>* cards = m_var_infos[v].m_lit_watch[!l.sign()];
+        if (cards != 0  && !cards->empty() && !s().inconsistent())  {
+            ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
+            for (; it != end; ++it) {
+                card& c = *(*it);
+                if (s().value(c.lit()) != l_true) {
+                    continue;
+                }
+                switch (add_assign(c, l)) {
+                case l_false: // conflict
+                    for (; it != end; ++it, ++it2) {
+                        *it2 = *it;
+                    }
+                    SASSERT(s().inconsistent());
+                    cards->set_end(it2);
+                    return;
+                case l_undef: // watch literal was swapped
+                    break;
+                case l_true: // unit propagation, keep watching the literal
+                    if (it2 != it) {
+                        *it2 = *it;
+                    }
+                    ++it2;
+                    break;
+                }
+            }
+            cards->set_end(it2);
+        }
+
+        card* crd = m_var_infos[v].m_card;
+        if (crd != 0 && !s().inconsistent()) {
+            init_watch(*crd, !l.sign());
+        }
+    }
+
+    check_result card_extension::check() { return CR_DONE; }
+
+    void card_extension::push() {
+        m_var_lim.push_back(m_var_trail.size());
+    }
+
+    void card_extension::pop(unsigned n) {        
+        unsigned new_lim = m_var_lim.size() - n;
+        unsigned sz = m_var_lim[new_lim];
+        while (m_var_trail.size() > sz) {
+            bool_var v = m_var_trail.back();
+            m_var_trail.pop_back();
+            if (v != null_bool_var) {
+                card* c = m_var_infos[v].m_card;
+                clear_watch(*c);
+                m_var_infos[v].m_card = 0;
+                dealloc(c);
+            }
+        }
+        m_var_lim.resize(new_lim);
+    }
+
+    void card_extension::simplify() {}
+    void card_extension::clauses_modifed() {}
+    lbool card_extension::get_phase(bool_var v) { return l_undef; }
+
+    void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
+        watch const* w = m_var_infos[v].m_lit_watch[sign];
+        if (w) {
+            watch const& wl = *w;
+            out << "watch: " << literal(v, sign) << " |-> ";
+            for (unsigned i = 0; i < wl.size(); ++i) {
+                out << wl[i]->lit() << " ";
+            }
+            out << "\n";        
+        }
+    }
+
+    void card_extension::display(std::ostream& out, card& c, bool values) const {
+        out << c.lit();
+        if (c.lit() != null_literal) {
+            if (values) {
+                out << "@(" << s().value(c.lit());
+                if (s().value(c.lit()) != l_undef) {
+                    out << ":" << s().lvl(c.lit());
+                }
+                out << ")";
+            }
+            out << c.lit() << "\n";
+        }
+        else {
+            out << " ";
+        }
+        for (unsigned i = 0; i < c.size(); ++i) {
+            literal l = c[i];
+            out << l;
+            if (values) {
+                out << "@(" << s().value(l);
+                if (s().value(l) != l_undef) {
+                    out << ":" << s().lvl(l);
+                }
+                out << ") ";
+            }
+        }
+        out << " >= " << c.k()  << "\n";
+    }
+
+    std::ostream& card_extension::display(std::ostream& out) const {
+        for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
+            display_watch(out, vi, false);
+            display_watch(out, vi, true);
+        }
+        for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
+            card* c = m_var_infos[vi].m_card;
+            if (c) {
+                display(out, *c, true);
+            }
+        }
+        return out;
+    }
+
+    void card_extension::collect_statistics(statistics& st) const {
+        st.update("card propagations", m_stats.m_num_propagations);
+        st.update("card conflicts", m_stats.m_num_conflicts);
+    }
+
+    bool card_extension::validate_conflict(card& c) { 
+        if (!validate_unit_propagation(c)) return false;
+        for (unsigned i = 0; i < c.k(); ++i) {
+            if (s().value(c[i]) == l_false) return true;
+        }
+        return false;
+    }
+    bool card_extension::validate_unit_propagation(card const& c) { 
+        for (unsigned i = c.k(); i < c.size(); ++i) {
+            if (s().value(c[i]) != l_false) return false;
+        }
+        return true;
+    }
+    bool card_extension::validate_lemma() { 
+        int value = -m_bound;
+        normalize_active_coeffs();
+        for (unsigned i = 0; i < m_active_vars.size(); ++i) {
+            bool_var v = m_active_vars[i];
+            int coeff = get_coeff(v);
+            SASSERT(coeff != 0);
+            if (coeff < 0 && s().value(v) != l_true) {
+                value -= coeff;
+            }
+            else if (coeff > 0 && s().value(v) != l_false) {
+                value += coeff;
+            }
+        }
+        return value < 0;
+    }
+
+    bool card_extension::validate_assign(literal_vector const& lits, literal lit) { return true; }
+    bool card_extension::validate_conflict(literal_vector const& lits) { return true; }
+
+    
+};
+
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
new file mode 100644
index 000000000..db8e041c2
--- /dev/null
+++ b/src/sat/card_extension.h
@@ -0,0 +1,142 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    card_extension.h
+
+Abstract:
+
+    Cardinality extensions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-01-30
+
+Revision History:
+
+--*/
+#ifndef CARD_EXTENSION_H_
+#define CARD_EXTENSION_H_
+
+#include"sat_extension.h"
+#include"sat_solver.h"
+
+namespace sat {
+
+    class card_extension : public extension {
+        struct stats {
+            unsigned m_num_propagations;
+            unsigned m_num_conflicts;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        class card {
+            unsigned       m_index;
+            literal        m_lit;
+            unsigned       m_k;
+            unsigned       m_size;
+            literal_vector m_lits;
+        public:
+            card(unsigned index, literal lit, literal_vector const& lits, unsigned k);
+            unsigned index() const { return m_index; }
+            literal lit() const { return m_lit; }
+            literal operator[](unsigned i) const { return m_lits[i]; }
+            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();                       
+        };
+
+        typedef ptr_vector<card> watch;
+        struct var_info {
+            watch* m_lit_watch[2];
+            card*  m_card;
+            var_info(): m_card(0) {
+                m_lit_watch[0] = 0;
+                m_lit_watch[1] = 0;
+            }
+            void reset() {
+                dealloc(m_card);
+                dealloc(m_lit_watch[0]);
+                dealloc(m_lit_watch[1]);
+            }
+        };
+
+
+        solver*             m_solver;
+        stats               m_stats;        
+
+        ptr_vector<card>    m_constraints;
+
+        // watch literals
+        svector<var_info>   m_var_infos;
+        unsigned_vector     m_var_trail;
+        unsigned_vector     m_var_lim;       
+
+        // conflict resolution
+        unsigned          m_num_marks;
+        unsigned          m_conflict_lvl;
+        svector<int>      m_coeffs;
+        svector<bool_var> m_active_vars;
+        int               m_bound;
+        tracked_uint_set  m_active_var_set;
+        literal_vector    m_conflict;
+        literal_vector    m_literals;
+
+        solver& s() const { return *m_solver; }
+        void init_watch(card& c, bool is_true);
+        void init_watch(bool_var v);
+        void assign(card& c, literal lit);
+        lbool add_assign(card& c, literal lit);
+        void watch_literal(card& c, literal lit);
+        void set_conflict(card& c, literal lit);
+        void clear_watch(card& c);
+        void reset_coeffs();
+
+        void unwatch_literal(literal w, card* c);
+        void remove(ptr_vector<card>& cards, card* c);
+
+        void normalize_active_coeffs();
+        void inc_coeff(literal l, int offset);
+        int get_coeff(bool_var v) const;
+        int get_abs_coeff(bool_var v) const;       
+
+        literal_vector& get_literals() { m_literals.reset(); return m_literals; }
+        literal get_asserting_literal(literal conseq);
+        bool resolve_conflict(card& c, literal_vector const& conflict_clause);
+        void process_antecedent(literal l, int offset);
+        void process_card(card& c, int offset);
+        void cut();
+
+        // validation utilities
+        bool validate_conflict(card& c);
+        bool validate_assign(literal_vector const& lits, literal lit);
+        bool validate_lemma();
+        bool validate_unit_propagation(card const& c);
+        bool validate_conflict(literal_vector const& lits);
+
+        void display(std::ostream& out, card& c, bool values) const;
+        void display_watch(std::ostream& out, bool_var v, bool sign) const;
+    public:
+        card_extension();
+        virtual ~card_extension();
+        void    set_solver(solver* s) { m_solver = s; }
+        void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
+        virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
+        virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
+        virtual void asserted(literal l);
+        virtual check_result check();
+        virtual void push();
+        virtual void pop(unsigned n);
+        virtual void simplify();
+        virtual void clauses_modifed();
+        virtual lbool get_phase(bool_var v);
+        virtual std::ostream& display(std::ostream& out) const;
+        virtual void collect_statistics(statistics& st) const;
+    };
+
+};
+
+#endif
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index b0b1c5d96..f1a48c0a8 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -21,6 +21,7 @@ Revision History:
 
 #include"sat_types.h"
 #include"params.h"
+#include"statistics.h"
 
 namespace sat {
 
@@ -30,6 +31,7 @@ namespace sat {
 
     class extension {
     public:
+        virtual ~extension() {}
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
         virtual void asserted(literal l) = 0;
@@ -39,6 +41,8 @@ namespace sat {
         virtual void simplify() = 0;
         virtual void clauses_modifed() = 0;
         virtual lbool get_phase(bool_var v) = 0;
+        virtual std::ostream& display(std::ostream& out) const = 0;
+        virtual void collect_statistics(statistics& st) const = 0;
     };
 
 };
diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h
index 00da9f30e..8c5331d17 100644
--- a/src/sat/sat_justification.h
+++ b/src/sat/sat_justification.h
@@ -33,7 +33,7 @@ namespace sat {
         explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
         justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
         explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
-        justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
+        static justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
         
         kind get_kind() const { return static_cast<kind>(m_val2 & 7); }
         
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index bf3dc1988..647c5f9ed 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2752,6 +2752,7 @@ namespace sat {
         m_scc.collect_statistics(st);
         m_asymm_branch.collect_statistics(st);
         m_probing.collect_statistics(st);
+        if (m_ext) m_ext->collect_statistics(st);
     }
 
     void solver::reset_statistics() {
@@ -2856,6 +2857,9 @@ namespace sat {
         display_units(out);
         display_binary(out);
         out << m_clauses << m_learned;
+        if (m_ext) {
+            m_ext->display(out);
+        }
         out << ")\n";
     }
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 54b8a9bb2..b42acc680 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -145,6 +145,7 @@ namespace sat {
         friend class probing;
         friend class iff3_finder;
         friend class mus;
+        friend class card_extension;
         friend struct mk_stat;
     public:
         solver(params_ref const & p, reslimit& l, extension * ext);
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 56f3d1e76..90673768b 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -250,16 +250,6 @@ namespace smt {
         typedef map<arg_t, bool_var, arg_t::hash, arg_t::eq> arg_map;
 
 
-        struct row_info {
-            unsigned     m_slack;   // slack variable in simplex tableau
-            numeral      m_bound;   // bound
-            arg_t        m_rep;     // representative
-            row_info(theory_var slack, numeral const& b, arg_t const& r):
-                m_slack(slack), m_bound(b), m_rep(r) {}
-            row_info(): m_slack(0) {}
-        };
-
-
         struct var_info {
             ineq_watch*  m_lit_watch[2];
             ineq_watch*  m_var_watch;
@@ -290,7 +280,6 @@ namespace smt {
         theory_pb_params         m_params;        
 
         svector<var_info>        m_var_infos; 
-        unsynch_mpq_inf_manager  m_mpq_inf_mgr;    // Simplex: manage inf_mpq numerals
         mutable unsynch_mpz_manager      m_mpz_mgr;        // Simplex: manager mpz numerals
         unsigned_vector          m_ineqs_trail;
         unsigned_vector          m_ineqs_lim;