diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index df5bb1eed..b91018217 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -46,6 +46,8 @@ namespace sat {
         m_lit(lit),
         m_k(k),
         m_size(wlits.size()),
+        m_slack(0),
+        m_num_watch(0),
         m_max_sum(0) {
         for (unsigned i = 0; i < wlits.size(); ++i) {
             m_wlits[i] = wlits[i];
@@ -237,7 +239,6 @@ namespace sat {
             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();
 
@@ -280,6 +281,7 @@ namespace sat {
             p.set_slack(slack);
             p.set_num_watch(num_watch);
         }
+        TRACE("sat", display(tout << "init watch: ", p, true););
     }
 
     /*
@@ -296,7 +298,7 @@ namespace sat {
           Lw = Lw u {l_s}
           Lu = Lu \ {l_s}
       }
-      if (Sw < bound) conflict
+      if (Sw < k) conflict
       while (Sw < k + a_max) {
           assign (l_max)
           a_max = max { ai | li in Lw, li = undef }
@@ -308,7 +310,19 @@ namespace sat {
       
         
     */
+    void card_extension::add_index(pb& p, unsigned index, literal lit) {
+        if (value(lit) == l_undef) {
+            m_pb_undef.push_back(index);
+            if (p[index].first > m_a_max) {
+                m_a_max = p[index].first;
+            }
+        }
+    }
+
     lbool card_extension::add_assign(pb& p, literal alit) {
+
+        TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
+        SASSERT(!s().inconsistent());
         unsigned sz = p.size();
         unsigned bound = p.k();
         unsigned num_watch = p.num_watch();
@@ -316,63 +330,43 @@ namespace sat {
         SASSERT(value(alit) == l_false);
         SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
         SASSERT(num_watch <= sz);
+        SASSERT(num_watch > 0);
         unsigned index = 0;
-        unsigned a_max = 0;
-        unsigned max_index = 0;
+        m_a_max = 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;
-                }
-            }
+            add_index(p, index, lit);
         }
-    
-        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;
-            }
+        SASSERT(index < num_watch);
+
+        unsigned index1 = index + 1;
+        for (; m_a_max == 0 && index1 < num_watch; ++index1) {
+            add_index(p, index1, p[index1].second);
         }
 
         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) {
+        for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) {
+            literal lit = p[j].second;
+            if (value(lit) != 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;
-                }
+                add_index(p, num_watch, lit);
                 ++num_watch;
             }
         }
 
+        SASSERT(!s().inconsistent());
+        DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); });
+
         if (slack < bound) {
             // maintain watching the literal
             slack += val;
@@ -385,34 +379,30 @@ namespace sat {
         }
 
         // swap out the watched literal.
-        p.set_slack(slack);
         --num_watch;
         SASSERT(num_watch > 0);
+        p.set_slack(slack);
         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)) {
+        if (slack < bound + m_a_max) {
+            while (!s().inconsistent() && !m_pb_undef.empty()) {
+                index1 = m_pb_undef.back();
+                literal lit = p[index1].second;
+                if (slack >= bound + p[index1].first) {
+                    break;
+                }
                 m_pb_undef.pop_back();
+                if (value(lit) == l_undef) {
+                    assign(p, lit);
+                }
             }
-            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;  
+
+        TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
+
+        return l_undef;
     }
 
     void card_extension::watch_literal(pb& p, wliteral l) {
@@ -467,6 +457,7 @@ namespace sat {
             set_conflict(p, lit); 
             break;
         default:
+            SASSERT(validate_unit_propagation(p, lit));
             m_stats.m_num_pb_propagations++;
             m_num_propagations_since_pop++;
             if (s().m_config.m_drat) {
@@ -483,7 +474,7 @@ namespace sat {
     }
 
     void card_extension::display(std::ostream& out, pb const& p, bool values) const {
-        out << p.lit() << "[" << p.size() << "]";
+        out << p.lit() << "[ watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
         if (p.lit() != null_literal && values) {
             out << "@(" << value(p.lit());
             if (value(p.lit()) != l_undef) {
@@ -514,7 +505,7 @@ namespace sat {
     }
 
     void card_extension::asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p0) {
-        TRACE("sat", tout << l << " " << !is_tag_empty(pbs) << " " << (p0 != 0) << "\n";);
+        TRACE("sat", tout << "literal: " << l << " has pb: " << !is_tag_empty(pbs) << " p0 != 0: " << (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();
@@ -524,20 +515,28 @@ namespace sat {
                     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_false: // conflict.
+                    SASSERT(s().inconsistent());
+                    for (; it != end; ++it, ++it2) {
+                        *it2 = *it;
+                    }
+                    pbs->set_end(it2);
+                    return;                
                 case l_undef: // watch literal was swapped
+                    if (s().inconsistent()) {
+                        ++it;
+                        for (; it != end; ++it, ++it2) {
+                            *it2 = *it;
+                        }
+                        pbs->set_end(it2);
+                        return;
+                    }
                     break; 
                 }
             }
@@ -844,6 +843,7 @@ namespace sat {
         literal consequent = s().m_not_l;
         justification js = s().m_conflict;
         TRACE("sat", tout << consequent << " " << js << "\n";);
+        TRACE("sat", s().display(tout););
         m_conflict_lvl = s().get_max_lvl(consequent, js);
         if (consequent != null_literal) {
             consequent.neg();
@@ -942,7 +942,7 @@ namespace sat {
                     m_bound += offset;
                     inc_coeff(consequent, offset);
                     get_pb_antecedents(consequent, p, m_lemma);
-                    TRACE("sat", tout << m_lemma << "\n";);
+                    TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";);
                     for (unsigned i = 0; i < m_lemma.size(); ++i) {
                         process_antecedent(~m_lemma[i], offset);
                     }
@@ -989,6 +989,7 @@ namespace sat {
             SASSERT(lvl(v) == m_conflict_lvl);
             s().reset_mark(v);
             --idx;
+            TRACE("sat", tout << "Unmark: v" << v << "\n";);
             --m_num_marks;
             js = s().m_justification[v];
             offset = get_abs_coeff(v);
@@ -1153,6 +1154,7 @@ namespace sat {
 
         if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) {
             s().mark(v);
+            TRACE("sat", tout << "Mark: v" << v << "\n";);
             ++m_num_marks;
         }
         inc_coeff(l, offset);                
@@ -1347,20 +1349,12 @@ namespace sat {
     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;
+        TRACE("sat", display(tout, p, true););
+        for (unsigned i = p.num_watch(); i < p.size(); ++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(l_false == value(lit));
+            r.push_back(~lit);
         }
-        SASSERT(max_sum < k);
     }
 
     void card_extension::get_card_antecedents(literal l, card const& c, literal_vector& r) {
@@ -1776,6 +1770,31 @@ namespace sat {
         }
         return true;
     }
+    bool card_extension::validate_unit_propagation(pb const& p, literal alit) { 
+        if (p.lit() != null_literal && value(p.lit()) != l_true) return false;
+
+        unsigned k = p.k();
+        unsigned sum = 0;
+        unsigned a_min = 0;
+        TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
+        for (unsigned i = 0; i < p.size(); ++i) {
+            literal lit = p[i].second;
+            lbool val = value(lit);
+            if (val == l_false) {
+                // no-op
+            }
+            else if (lit == alit) {
+                a_min = p[i].first;
+                sum += p[i].first;
+            }
+            else {
+                sum += p[i].first;
+            }
+        }
+        return sum < k + a_min;
+        return true;
+    }
+
     bool card_extension::validate_lemma() { 
         int val = -m_bound;
         normalize_active_coeffs();
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index f7e54b843..41219fae5 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -232,10 +232,12 @@ namespace sat {
 
 
         // pb functionality
+        unsigned m_a_max;
         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 add_index(pb& p, unsigned index, literal lit);
         void watch_literal(pb& p, wliteral lit);
         void clear_watch(pb& p);
         void set_conflict(pb& p, literal lit);
@@ -280,6 +282,7 @@ namespace sat {
         bool validate_assign(literal_vector const& lits, literal lit);
         bool validate_lemma();
         bool validate_unit_propagation(card const& c);
+        bool validate_unit_propagation(pb const& p, literal lit);
         bool validate_conflict(literal_vector const& lits, ineq& p);
 
         ineq m_A, m_B, m_C;