diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 7d1c27abb..30206a441 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -45,9 +45,11 @@ namespace sat {
         m_index(index),
         m_lit(lit),
         m_k(k),
-        m_size(wlits.size()) {
+        m_size(wlits.size()),
+        m_max_sum(0) {
         for (unsigned i = 0; i < wlits.size(); ++i) {
             m_wlits[i] = wlits[i];
+            m_max_sum += wlits[i].first;
         }
     }
 
@@ -212,14 +214,355 @@ namespace sat {
     }
 
     // pb:
-    void card_extension::init_watch(pb& p, bool is_true) {
-        NOT_IMPLEMENTED_YET();
+
+    void card_extension::copy_pb(card_extension& result) {
+        for (unsigned i = 0; i < m_pbs.size(); ++i) {
+            svector<wliteral> wlits;
+            pb& p = *m_pbs[i];
+            for (unsigned i = 0; i < p.size(); ++i) {
+                wlits.push_back(p[i]);
+            }
+            bool_var v = p.lit() == null_literal ? null_bool_var : p.lit().var();
+            result.add_pb_ge(v, wlits, p.k());
+        }
     }
 
+    // watch a prefix of literals, such that the slack of these is >= k
+    void card_extension::init_watch(pb& p, bool is_true) {
+        clear_watch(p);
+        if (p.lit() != null_literal && p.lit().sign() == is_true) {
+            p.negate();
+        }
+        
+        TRACE("sat", display(tout << "init watch: ", p, true););
+        SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
+        unsigned sz = p.size(), bound = p.k();
 
+        // put the non-false literals into the head.
+        unsigned slack = 0, num_watch = 0, j = 0;
+        for (unsigned i = 0; i < sz; ++i) {
+            if (value(p[i].second) != l_false) {
+                if (j != i) {
+                    p.swap(i, j);
+                }
+                if (slack < bound) {
+                    slack += p[i].first;
+                    ++num_watch;
+                }
+                ++j;
+            }
+        }
+        DEBUG_CODE(
+            bool is_false = false;
+            for (unsigned k = 0; k < sz; ++k) {
+                SASSERT(!is_false || value(p[k].second) == l_false);
+                SASSERT(k < j == (value(p[k].second) != l_false));
+                is_false = value(p[k].second) == l_false;
+            });
 
+        if (slack < bound) {
+            literal lit = p[j].second;
+            SASSERT(value(p[j].second) == l_false);
+            for (unsigned i = j + 1; j < sz; ++i) {
+                if (lvl(lit) < lvl(p[i].second)) {
+                    lit = p[i].second;
+                }
+            }
+            set_conflict(p, lit);
+        }
+        else {            
+            for (unsigned i = 0; i < num_watch; ++i) {
+                watch_literal(p, p[i]);
+            }
+            p.set_slack(slack);
+            p.set_num_watch(num_watch);
+        }
+    }
+
+    /*
+      Chai Kuhlmann:
+      Lw - set of watched literals
+      Lu - set of unwatched literals that are not false
+      
+      Lw = Lw \ { alit }
+      Sw -= value
+      a_max = max { a | l in Lw u Lu, l = undef }
+      while (Sw < k + a_max & Lu != 0) {
+          a_s = max { a | l in Lu }
+          Sw += a_s
+          Lw = Lw u {l_s}
+          Lu = Lu \ {l_s}
+      }
+      if (Sw < bound) conflict
+      while (Sw < k + a_max) {
+          assign (l_max)
+          a_max = max { ai | li in Lw, li = undef }
+      }
+      ASSERT(Sw >= bound)
+      return no-conflict
+
+      a_max index: index of non-false literal with maximal weight.
+      
+        
+    */
+    lbool card_extension::add_assign(pb& p, literal alit) {
+        unsigned sz = p.size();
+        unsigned bound = p.k();
+        unsigned num_watch = p.num_watch();
+        unsigned slack = p.slack();
+        SASSERT(value(alit) == l_false);
+        SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
+        SASSERT(num_watch <= sz);
+        unsigned index = 0;
+        unsigned a_max = 0;
+        unsigned max_index = 0;
+        m_pb_undef.reset();
+        for (; index < num_watch; ++index) {
+            literal lit = p[index].second;
+            if (lit == alit) {
+                break;
+            }
+            if (value(lit) == l_undef) {
+                m_pb_undef.push_back(index);
+                if (p[index].first > a_max) {
+                    a_max = p[index].first;
+                    max_index = index;
+                }
+            }
+        }
+    
+        for (unsigned j = index + 1; a_max == 0 && j < num_watch; ++j) {
+            literal lit = p[j].second;
+            if (value(lit) == l_undef) {
+                m_pb_undef.push_back(j);
+                a_max = p[j].first;
+                max_index = j;
+            }
+        }
+        for (unsigned j = num_watch; a_max == 0 && j < sz; ++j) {
+            literal lit = p[j].second;
+            if (value(lit) == l_undef) {
+                p.swap(j, num_watch);
+                m_pb_undef.push_back(num_watch);
+                a_max = p[num_watch].first;
+                max_index = num_watch;
+            }
+        }
+
+        unsigned val = p[index].first;
+        SASSERT(num_watch > 0);
+        SASSERT(index < num_watch);
+        SASSERT(value(p[index].second) == l_false);
+        SASSERT(val <= slack);
+        slack -= val;
+        // find literals to swap with:            
+        for (unsigned j = num_watch; j < sz && slack < bound + a_max; ++j) {
+            if (value(p[j].second) != l_false) {
+                slack += p[j].first;
+                watch_literal(p, p[j]);
+                p.swap(num_watch, j);
+                if (value(p[num_watch].second) == l_undef && a_max < p[num_watch].first) {
+                    m_pb_undef.push_back(num_watch);
+                    a_max = p[num_watch].first;
+                    max_index = num_watch;
+                }
+                ++num_watch;
+            }
+        }
+
+        if (slack < bound) {
+            // maintain watching the literal
+            slack += val;
+            p.set_slack(slack);
+            p.set_num_watch(num_watch);
+            SASSERT(bound <= slack);
+            TRACE("sat", tout << "conflict " << alit << "\n";);
+            set_conflict(p, alit);
+            return l_false;
+        }
+
+        // swap out the watched literal.
+        p.set_slack(slack);
+        --num_watch;
+        SASSERT(num_watch > 0);
+        p.set_num_watch(num_watch);
+        p.swap(num_watch, index);
+        if (num_watch == max_index) {
+            max_index = index;
+        }
+
+        SASSERT(max_index < sz);
+        while (slack < bound + a_max && !s().inconsistent()) {
+            // variable at max-index must be assigned to true.
+            assign(p, p[max_index].second);         
+
+            a_max = 0;
+            // find the next a_max among m_pb_undef
+            while (!m_pb_undef.empty() && l_undef != value(p[m_pb_undef.back()].second)) {
+                m_pb_undef.pop_back();
+            }
+            if (m_pb_undef.empty()) {
+                break;
+            }
+            max_index = m_pb_undef.back();
+            a_max = p[max_index].first;
+            m_pb_undef.pop_back();
+        }
+
+        return s().inconsistent() ? l_false : l_true;  
+    }
+
+    void card_extension::watch_literal(pb& p, wliteral l) {
+        literal lit = l.second;
+        init_watch(lit.var());
+        ptr_vector<pb>* pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
+        if (pbs == 0) {
+            pbs = alloc(ptr_vector<pb>);
+            m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;
+        }
+        else if (is_tag_empty(pbs)) {
+            pbs = set_tag_non_empty(pbs);
+            m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;            
+        }
+        TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
+        pbs->push_back(&p);
+    }
+
+    void card_extension::clear_watch(pb& p) {
+        unsigned sz = p.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            unwatch_literal(p[i].second, &p);            
+        }
+    }
+    
+    void card_extension::unwatch_literal(literal lit, pb* p) {
+        if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
+            return;
+        }
+        pb_watch*& pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
+        if (!is_tag_empty(pbs)) {
+            if (remove(*pbs, p)) {
+                pbs = set_tag_empty(pbs);
+            }        
+        }
+    }
+
+    void card_extension::set_conflict(pb& p, literal lit) {
+        m_stats.m_num_pb_conflicts++;
+        TRACE("sat", display(tout, p, true); );
+        // SASSERT(validate_conflict(p));
+        SASSERT(value(lit) == l_false);
+        s().set_conflict(justification::mk_ext_justification(p.index()), ~lit);
+        SASSERT(s().inconsistent());
+    }
+
+    void card_extension::assign(pb& p, literal lit) {
+        switch (value(lit)) {
+        case l_true: 
+            break;
+        case l_false: 
+            set_conflict(p, lit); 
+            break;
+        default:
+            m_stats.m_num_pb_propagations++;
+            m_num_propagations_since_pop++;
+            if (s().m_config.m_drat) {
+                svector<drat::premise> ps;
+                literal_vector lits;
+                get_pb_antecedents(lit, p, lits);
+                lits.push_back(lit);
+                ps.push_back(drat::premise(drat::s_ext(), p.lit()));
+                s().m_drat.add(lits, ps);
+            }
+            s().assign(lit, justification::mk_ext_justification(p.index()));
+            break;
+        }
+    }
+
+    void card_extension::display(std::ostream& out, pb& p, bool values) const {
+        out << p.lit() << "[" << p.size() << "]";
+        if (p.lit() != null_literal && values) {
+            out << "@(" << value(p.lit());
+            if (value(p.lit()) != l_undef) {
+                out << ":" << lvl(p.lit());
+            }
+            out << "): ";
+        }
+        else {
+            out << ": ";
+        }
+        for (unsigned i = 0; i < p.size(); ++i) {
+            literal l = p[i].second;
+            unsigned w = p[i].first;
+            if (w > 1) out << w << " * ";
+            out << l;
+            if (values) {
+                out << "@(" << value(l);
+                if (value(l) != l_undef) {
+                    out << ":" << lvl(l);
+                }
+                out << ") ";
+            }
+            else {
+                out << " ";
+            }
+        }
+        out << ">= " << p.k()  << "\n";
+    }
+
+    void card_extension::asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p0) {
+        TRACE("sat", tout << l << " " << !is_tag_empty(pbs) << " " << (p0 != 0) << "\n";);
+        if (!is_tag_empty(pbs)) {
+            ptr_vector<pb>::iterator begin = pbs->begin();
+            ptr_vector<pb>::iterator it = begin, it2 = it, end = pbs->end();
+            for (; it != end; ++it) {
+                pb& p = *(*it);
+                if (p.lit() != null_literal && value(p.lit()) != l_true) {
+                    continue;
+                }
+                switch (add_assign(p, ~l)) {
+                case l_false: // conflict
+                    for (; it != end; ++it, ++it2) {
+                        *it2 = *it;
+                    }
+                    SASSERT(s().inconsistent());
+                    pbs->set_end(it2);
+                    return;
+                case l_true: // unit propagation, keep watching the literal
+                    if (it2 != it) {
+                        *it2 = *it;
+                    }
+                    ++it2;
+                    break;
+                case l_undef: // watch literal was swapped
+                    break; 
+                }
+            }
+            pbs->set_end(it2);
+            if (pbs->empty()) {
+                m_var_infos[l.var()].m_pb_watch[!l.sign()] = set_tag_empty(pbs);
+            }
+        }
+
+        if (p0 != 0 && !s().inconsistent()) {
+            init_watch(*p0, !l.sign());
+        }        
+    }
 
     // xor:
+
+    void card_extension::copy_xor(card_extension& result) {
+        for (unsigned i = 0; i < m_xors.size(); ++i) {
+            literal_vector lits;
+            xor& x = *m_xors[i];
+            for (unsigned i = 0; i < x.size(); ++i) {
+                lits.push_back(x[i]);
+            }
+            bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
+            result.add_xor(v, lits);
+        }
+    }
+
     void card_extension::clear_watch(xor& x) {
         unwatch_literal(x[0], &x);
         unwatch_literal(x[1], &x);         
@@ -229,7 +572,7 @@ namespace sat {
         if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
             return;
         }
-        xor_watch* xors = m_var_infos[lit.var()].m_xor_watch;
+        xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch;
         if (!is_tag_empty(xors)) {
             if (remove(*xors, c)) {
                 xors = set_tag_empty(xors);
@@ -384,6 +727,45 @@ namespace sat {
         return s().inconsistent() ? l_false : l_true;  
     }
 
+    void card_extension::asserted_xor(literal l, ptr_vector<xor>* xors, xor* x) {
+        TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";);
+        if (!is_tag_empty(xors)) {
+            ptr_vector<xor>::iterator begin = xors->begin();
+            ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
+            for (; it != end; ++it) {
+                xor& c = *(*it);
+                if (c.lit() != null_literal && 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());
+                    xors->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;
+                }
+            }
+            xors->set_end(it2);
+            if (xors->empty()) {
+                m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors);
+            }
+        }
+
+        if (x != 0 && !s().inconsistent()) {
+            init_watch(*x, !l.sign());
+        }
+    }
+
     
     void card_extension::normalize_active_coeffs() {
         while (!m_active_var_set.empty()) m_active_var_set.erase();
@@ -551,7 +933,15 @@ namespace sat {
                     ++m_stats.m_num_xor_resolves;
                 }
                 else if (is_pb_index(index)) {
-                    NOT_IMPLEMENTED_YET();
+                    pb& p = index2pb(index);
+                    m_lemma.reset();
+                    m_bound += offset;
+                    inc_coeff(consequent, offset);
+                    get_pb_antecedents(consequent, p, m_lemma);
+                    for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                        process_antecedent(~m_lemma[i], offset);
+                    }
+                    ++m_stats.m_num_pb_resolves;
                 }
                 else {
                     UNREACHABLE();
@@ -810,10 +1200,10 @@ namespace sat {
     }
 
     void card_extension::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
-        unsigned index = 4*m_pb.size() + 0x11;
+        unsigned index = 4*m_pbs.size() + 0x11;
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
         pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
-        m_pb.push_back(p);
+        m_pbs.push_back(p);
         if (v == null_bool_var) {
             init_watch(*p, true);
             m_pb_axioms.push_back(p);
@@ -946,6 +1336,25 @@ namespace sat {
         TRACE("sat", tout << r << "\n";);
     }
 
+    void card_extension::get_pb_antecedents(literal l, pb const& p, literal_vector& r) {
+        if (p.lit() != null_literal) r.push_back(p.lit());
+        SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
+        unsigned k = p.k();
+        unsigned max_sum = p.max_sum();
+        for (unsigned i = p.size(); i > 0 && max_sum >= k; ) {
+            --i;
+            literal lit = p[i].second;
+            if (lit == l) {
+                max_sum -= p[i].first;
+            }
+            else if (value(lit) == l_false) {
+                r.push_back(~p[i].second);
+                max_sum -= p[i].first;
+            }
+        }
+        SASSERT(max_sum < k);
+    }
+
     void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
         if (is_card_index(idx)) {
             card& c = index2card(idx);
@@ -984,7 +1393,8 @@ namespace sat {
             }
         }
         else if (is_pb_index(idx)) {
-            NOT_IMPLEMENTED_YET();
+            pb const& p = index2pb(idx);
+            get_pb_antecedents(l, p, r);
         }
         else {
             UNREACHABLE();
@@ -1054,9 +1464,11 @@ namespace sat {
         if (v >= m_var_infos.size()) return;
         var_info& vinfo = m_var_infos[v];
         ptr_vector<card>* cards = vinfo.m_card_watch[!l.sign()];
+        ptr_vector<xor>* xors = vinfo.m_xor_watch;
+        ptr_vector<pb>* pbs = vinfo.m_pb_watch[!l.sign()];
+        pb* p = vinfo.m_pb;
         card* crd = vinfo.m_card;
         xor* x = vinfo.m_xor;
-        ptr_vector<xor>* xors = vinfo.m_xor_watch;
 
         if (!is_tag_empty(cards)) {
             ptr_vector<card>::iterator begin = cards->begin();
@@ -1093,51 +1505,17 @@ namespace sat {
         if (crd != 0 && !s().inconsistent()) {
             init_watch(*crd, !l.sign());
         }
+        
+        if ((!is_tag_empty(pbs) || p) && !s().inconsistent()) {
+            asserted_pb(l, pbs, p);
+        }
+
         if (m_has_xor && !s().inconsistent()) {
             asserted_xor(l, xors, x);
         }
     }
 
 
-    void card_extension::asserted_xor(literal l, ptr_vector<xor>* xors, xor* x) {
-        TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";);
-        if (!is_tag_empty(xors)) {
-            ptr_vector<xor>::iterator begin = xors->begin();
-            ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
-            for (; it != end; ++it) {
-                xor& c = *(*it);
-                if (c.lit() != null_literal && 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());
-                    xors->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;
-                }
-            }
-            xors->set_end(it2);
-            if (xors->empty()) {
-                m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors);
-            }
-        }
-
-        if (x != 0 && !s().inconsistent()) {
-            init_watch(*x, !l.sign());
-        }
-    }
-
     check_result card_extension::check() { return CR_DONE; }
 
     void card_extension::push() {
@@ -1153,13 +1531,17 @@ namespace sat {
             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);
+                if (c) {
+                    clear_watch(*c);
+                    m_var_infos[v].m_card = 0;
+                    dealloc(c);
+                }
                 xor* x = m_var_infos[v].m_xor;
-                clear_watch(*x);
-                m_var_infos[v].m_xor = 0;
-                dealloc(x);
+                if (x) {
+                    clear_watch(*x);
+                    m_var_infos[v].m_xor = 0;
+                    dealloc(x);
+                }
             }
         }
         m_var_lim.resize(new_lim);
@@ -1182,15 +1564,8 @@ namespace sat {
             bool_var v = c.lit() == null_literal ? null_bool_var : c.lit().var();
             result->add_at_least(v, lits, c.k());
         }
-        for (unsigned i = 0; i < m_xors.size(); ++i) {
-            literal_vector lits;
-            xor& x = *m_xors[i];
-            for (unsigned i = 0; i < x.size(); ++i) {
-                lits.push_back(x[i]);
-            }
-            bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
-            result->add_xor(v, lits);
-        }
+        copy_xor(*result);
+        copy_pb(*result);
         return result;
     }
 
@@ -1347,7 +1722,15 @@ namespace sat {
             }            
         }
         else if (is_pb_index(idx)) {
-            NOT_IMPLEMENTED_YET();
+            pb& p = index2pb(idx);
+            out << "pb " << p.lit() << ": ";
+            for (unsigned i = 0; i < p.size(); ++i) {
+                if (p[i].first != 1) {
+                    out << p[i].first << " ";
+                }
+                out << p[i].second << " ";
+            }
+            out << ">= " << p.k();
         }
         else {
             UNREACHABLE();
@@ -1362,6 +1745,9 @@ namespace sat {
         st.update("xor propagations", m_stats.m_num_xor_propagations);
         st.update("xor conflicts", m_stats.m_num_xor_conflicts);
         st.update("xor resolves", m_stats.m_num_xor_resolves);
+        st.update("pb propagations", m_stats.m_num_pb_propagations);
+        st.update("pb conflicts", m_stats.m_num_pb_conflicts);
+        st.update("pb resolves", m_stats.m_num_pb_resolves);
     }
 
     bool card_extension::validate_conflict(card& c) { 
@@ -1457,7 +1843,12 @@ namespace sat {
                 if (lxor != null_literal) p.push(~lxor, offset);
             }
             else if (is_pb_index(index)) {
-                NOT_IMPLEMENTED_YET();
+                pb& pb = index2pb(index);
+                p.reset(pb.k());
+                for (unsigned i = 0; i < pb.size(); ++i) {
+                    p.push(pb[i].second, pb[i].first);
+                }
+                if (pb.lit() != null_literal) p.push(~pb.lit(), pb.k());
             }
             else {
                 UNREACHABLE();
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index 6f8b6d120..0e229a056 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -36,6 +36,9 @@ namespace sat {
             unsigned m_num_xor_propagations;
             unsigned m_num_xor_conflicts;
             unsigned m_num_xor_resolves;
+            unsigned m_num_pb_propagations;
+            unsigned m_num_pb_conflicts;
+            unsigned m_num_pb_resolves;
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
@@ -66,6 +69,9 @@ namespace sat {
             literal        m_lit;
             unsigned       m_k;
             unsigned       m_size;
+            unsigned       m_slack;
+            unsigned       m_num_watch;
+            unsigned       m_max_sum;
             wliteral       m_wlits[0];
         public:
             static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(wliteral); }
@@ -75,6 +81,11 @@ namespace sat {
             wliteral operator[](unsigned i) const { return m_wlits[i]; }
             unsigned k() const { return m_k; }
             unsigned size() const { return m_size; }
+            unsigned slack() const { return m_slack; }
+            void set_slack(unsigned s) { m_slack = s; }
+            unsigned num_watch() const { return m_num_watch; }
+            unsigned max_sum() const { return m_max_sum; }
+            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();                       
         };
@@ -153,7 +164,7 @@ namespace sat {
 
         ptr_vector<card>    m_cards;
         ptr_vector<xor>     m_xors;
-        ptr_vector<pb>      m_pb;
+        ptr_vector<pb>      m_pbs;
 
         scoped_ptr_vector<card> m_card_axioms;
         scoped_ptr_vector<pb>   m_pb_axioms;
@@ -175,6 +186,9 @@ namespace sat {
         bool              m_has_xor;
         unsigned_vector   m_parity_marks;
         literal_vector    m_parity_trail;
+
+        unsigned_vector   m_pb_undef;
+
         void     ensure_parity_size(bool_var v);
         unsigned get_parity(bool_var v);
         void     inc_parity(bool_var v);
@@ -193,6 +207,7 @@ namespace sat {
         void unwatch_literal(literal w, card* c);
 
         // xor specific functionality
+        void copy_xor(card_extension& result);
         void clear_watch(xor& x);
         void watch_literal(xor& x, literal lit);
         void unwatch_literal(literal w, xor* x);
@@ -202,17 +217,28 @@ namespace sat {
         bool parity(xor const& x, unsigned offset) const;
         lbool add_assign(xor& x, literal alit);
         void asserted_xor(literal l, ptr_vector<xor>* xors, xor* x);
+        void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
+
 
         bool is_card_index(unsigned idx) const { return 0x00 == (idx & 0x11); }
         bool is_xor_index(unsigned idx) const { return 0x01 == (idx & 0x11); }
         bool is_pb_index(unsigned idx) const { return 0x11 == (idx & 0x11); }
         card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 2]; }
         xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 2]; }
-        pb&  index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pb[idx >> 2]; }
+        pb&  index2pb(unsigned idx) const { SASSERT(is_pb_index(idx)); return *m_pbs[idx >> 2]; }
 
-        void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r);
 
+        // pb functionality
+        void copy_pb(card_extension& result);
+        void asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p);
         void init_watch(pb& p, bool is_true);
+        lbool add_assign(pb& p, literal alit);
+        void watch_literal(pb& p, wliteral lit);
+        void clear_watch(pb& p);
+        void set_conflict(pb& p, literal lit);
+        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);
 
 
         template<typename T>
@@ -260,6 +286,7 @@ namespace sat {
 
         void display(std::ostream& out, ineq& p) const;
         void display(std::ostream& out, card& c, bool values) const;
+        void display(std::ostream& out, pb& p, bool values) const;
         void display(std::ostream& out, xor& c, bool values) const;
         void display_watch(std::ostream& out, bool_var v) const;
         void display_watch(std::ostream& out, bool_var v, bool sign) const;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 407475280..2687c59e5 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -191,7 +191,7 @@ namespace sat {
         m_elim_counter = m_res_limit;
         m_old_num_elim_vars = m_num_elim_vars;
 
-        scoped_finalize _scoped_finalize(*this);
+        // scoped_finalize _scoped_finalize(*this);
 
         do {
             if (m_subsumption)