diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp
index d283feab8..1019465cd 100644
--- a/src/opt/core_maxsat.cpp
+++ b/src/opt/core_maxsat.cpp
@@ -50,13 +50,13 @@ namespace opt {
             case l_undef: 
                 return l_undef;
             case l_true: {
-                model_ref model;
+                model_ref mdl;
                 expr_ref_vector ans(m);
-                s.get_model(model);
+                s.get_model(mdl);
                 
                 for (unsigned i = 0; i < aux.size(); ++i) {
                     expr_ref val(m);
-                    VERIFY(model->eval(m_soft[i].get(), val));
+                    VERIFY(mdl->eval(m_soft[i].get(), val));
                     if (m.is_true(val)) {
                         ans.push_back(m_soft[i].get());
                     }
@@ -69,6 +69,7 @@ namespace opt {
                 if (ans.size() > m_answer.size()) {
                     m_answer.reset();
                     m_answer.append(ans);
+                    m_model = mdl.get();
                 }
                 if (m_answer.size() == m_upper) {
                     return l_true;
@@ -150,6 +151,9 @@ namespace opt {
     void core_maxsat::collect_statistics(statistics& st) const {
         // nothing specific
     }
+    void core_maxsat::get_model(model_ref& mdl) {
+        mdl = m_model.get();
+    }
 
     
 };
diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h
index 63f92cf4a..cf4ce8d48 100644
--- a/src/opt/core_maxsat.h
+++ b/src/opt/core_maxsat.h
@@ -31,6 +31,7 @@ namespace opt {
         expr_ref_vector m_soft;
         expr_ref_vector m_answer;
         unsigned        m_upper;
+        model_ref       m_model;
     public:
         core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
         virtual ~core_maxsat();
@@ -41,7 +42,7 @@ namespace opt {
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
-
+        virtual void get_model(model_ref& mdl);
     private:
         void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
         expr_ref mk_at_most(expr_set const& set, unsigned k);
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index a83419cb6..13dc6e46d 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -48,6 +48,7 @@ namespace opt {
         expr_ref_vector m_aux;
         expr_ref_vector m_assignment;
         unsigned        m_upper_size;
+        model_ref       m_model;
 
         ref<solver>     m_s;
         solver &        m_original_solver;
@@ -300,13 +301,12 @@ namespace opt {
                 
                 if (is_sat == l_true) {
                     // Get a list of satisfying m_soft
-                    model_ref model;
-                    s().get_model(model);
+                    s().get_model(m_model);
 
                     m_assignment.reset();                    
                     for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
                         expr_ref val(m);
-                        VERIFY(model->eval(m_orig_soft[i].get(), val));
+                        VERIFY(m_model->eval(m_orig_soft[i].get(), val));
                         if (m.is_true(val)) {
                             m_assignment.push_back(m_orig_soft[i].get());
                         }
@@ -318,6 +318,10 @@ namespace opt {
             return is_sat;            
         }
 
+        void get_model(model_ref& mdl) {
+            mdl = m_model.get();
+        }
+
     };
 
     fu_malik::fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) {
@@ -348,6 +352,10 @@ namespace opt {
     void fu_malik::collect_statistics(statistics& st) const {
         m_imp->collect_statistics(st);
     }
+    void fu_malik::get_model(model_ref& m) {
+        m_imp->get_model(m);
+    }
+
 
 
 
diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h
index 980db707b..2cd4e146d 100644
--- a/src/opt/fu_malik.h
+++ b/src/opt/fu_malik.h
@@ -42,6 +42,7 @@ namespace opt {
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
+        virtual void get_model(model_ref& m);
     };
     
 };
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 8232e169e..1d1a65e5c 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -52,6 +52,9 @@ namespace opt {
         if (m_msolver) {
             is_sat = (*m_msolver)();
             m_answer.append(m_msolver->get_assignment());
+            if (is_sat == l_true) {
+                m_msolver->get_model(m_model);
+            }
         }
 
         // Infrastructure for displaying and storing solution is TBD.
@@ -105,6 +108,10 @@ namespace opt {
         if (m_lower > r)  m_lower = r;
     }
 
+    void maxsmt::get_model(model_ref& mdl) {
+        mdl = m_model.get();
+    }
+
     void maxsmt::commit_assignment() {
         SASSERT(m_s);
         for (unsigned i = 0; i < m_answer.size(); ++i) {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index d4eff4334..92744baaf 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -35,6 +35,7 @@ namespace opt {
         virtual expr_ref_vector get_assignment() const = 0;
         virtual void set_cancel(bool f) = 0;
         virtual void collect_statistics(statistics& st) const = 0;
+        virtual void get_model(model_ref& mdl) = 0;
     };
     /**
        Takes solver with hard constraints added.
@@ -52,6 +53,7 @@ namespace opt {
         rational         m_upper;
         scoped_ptr<maxsmt_solver> m_msolver;
         symbol           m_maxsat_engine;
+        model_ref        m_model;
     public:
         maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
 
@@ -78,15 +80,11 @@ namespace opt {
         rational get_lower() const;
         rational get_upper() const;
         void update_lower(rational const& r);
-
-
+        void get_model(model_ref& mdl);
         expr_ref_vector get_assignment() const;
-
-        void display_answer(std::ostream& out) const;
-        
+        void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;
 
-
     private:
 
         bool is_maxsat_problem(vector<rational> const& ws) const;        
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2142ffae3..6501ef51b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -108,12 +108,16 @@ namespace opt {
 
     void context::get_model(model_ref& mdl) {
         mdl = m_model;
+        if (m_model_converter) {
+            (*m_model_converter)(mdl, 0);
+        }
     }
 
     lbool context::execute_min_max(unsigned index, bool committed, bool is_max) {
         // HACK: reuse m_optsmt without regard for box reuse and not considering
         // use-case of lex.
         lbool result = m_optsmt(get_solver());
+        if (result == l_true) m_optsmt.get_model(m_model);
         if (committed) m_optsmt.commit_assignment(index);
         return result;
     }
@@ -122,6 +126,7 @@ namespace opt {
     lbool context::execute_maxsat(symbol const& id, bool committed) {
         maxsmt& ms = *m_maxsmts.find(id);
         lbool result = ms(get_solver());
+        if (result == l_true) ms.get_model(m_model);
         if (committed) ms.commit_assignment();
         return result;
     }
@@ -177,11 +182,10 @@ namespace opt {
         tactic_ref tac1 = mk_elim01_tactic(m);
         tactic_ref tac2 = mk_lia2card_tactic(m);
         tactic_ref tac  = and_then(tac1.get(), tac2.get());
-        model_converter_ref mc;  // TBD: expose model converter upwards and apply to returned model.
         proof_converter_ref pc;
         expr_dependency_ref core(m);
         goal_ref_buffer result;
-        (*tac)(g, result, mc, pc, core);   // TBD: have this an attribute so we can cancel.
+        (*tac)(g, result, m_model_converter, pc, core);  // TBD: have this an attribute so we can cancel.
         SASSERT(result.size() == 1);
         goal* r = result[0];
         fmls.reset();
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 2e19c3cb3..bc13795eb 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -29,6 +29,7 @@ Notes:
 #include "opt_solver.h"
 #include "optsmt.h"
 #include "maxsmt.h"
+#include "model_converter.h"
 
 namespace opt {
 
@@ -83,6 +84,7 @@ namespace opt {
         map_id              m_indices;
         vector<objective>   m_objectives;
         model_ref           m_model;
+        model_converter_ref m_model_converter;
         obj_map<func_decl, unsigned> m_objective_fns;
     public:
         context(ast_manager& m);
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 2f4a35459..fdf86c534 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -121,6 +121,7 @@ namespace opt {
         inf_eps v(r);
         if (m_lower[idx] < v) {
             m_lower[idx] = v;
+            s->get_model(m_model);
         }
     }
 
@@ -261,6 +262,10 @@ namespace opt {
         return m_is_max[i]?m_upper[i]:-m_lower[i];
     }
 
+    void optsmt::get_model(model_ref& mdl) {
+        mdl = m_model.get();
+    }
+
     // force lower_bound(i) <= objective_value(i)    
     void optsmt::commit_assignment(unsigned i) {
         inf_eps mid(0);
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index c8be7a730..3379ee310 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -37,6 +37,7 @@ namespace opt {
         svector<bool>    m_is_max;
         svector<smt::theory_var> m_vars;
         symbol           m_engine;
+        model_ref        m_model;
     public:
         optsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
 
@@ -56,6 +57,7 @@ namespace opt {
         inf_eps get_value(unsigned index) const;
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
+        void    get_model(model_ref& mdl);
 
         void update_lower(unsigned idx, rational const& r);
         
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 48c25e4d5..b03b8005a 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -35,6 +35,7 @@ namespace smt {
         rational                 m_min_cost;   // current maximal cost assignment.
         u_map<theory_var>        m_bool2var;   // bool_var -> theory_var
         svector<bool_var>        m_var2bool;   // theory_var -> bool_var
+        model_ref                m_model;
     public:
         theory_weighted_maxsat(ast_manager& m):
             theory(m.mk_family_id("weighted_maxsat")),
@@ -186,6 +187,7 @@ namespace smt {
             m_bool2var.reset();
             m_var2bool.reset();
             m_min_cost_atom = 0;
+            m_model = 0;
         }
 
         virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_weighted_maxsat, new_ctx->get_manager()); }
@@ -194,6 +196,9 @@ namespace smt {
         virtual void new_eq_eh(theory_var v1, theory_var v2) { }
         virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
 
+        void get_model(model_ref& mdl) {
+            mdl = m_model.get();
+        }
 
     private:
        
@@ -239,9 +244,11 @@ namespace smt {
                 m_min_cost = weight;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);
+                ctx.get_model(m_model);
             }
             return false;
         }                
+
     };
 
 }
@@ -284,6 +291,7 @@ namespace opt {
         expr_ref_vector  m_assignment;
         vector<rational> m_weights;
         rational         m_upper;
+        model_ref        m_model;
 
         imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
             m(m), s(s), m_soft(soft_constraints), m_assignment(m), m_weights(weights)
@@ -337,6 +345,7 @@ namespace opt {
                 }
             }
             m_upper = wth.get_min_cost();
+            wth.get_model(m_model);
             TRACE("opt", tout << "min cost: " << m_upper << "\n";);
             wth.reset();
             return result;            
@@ -349,6 +358,11 @@ namespace opt {
         rational get_upper() const {
             return m_upper;
         }
+
+        void get_model(model_ref& mdl) {
+            mdl = m_model.get();
+        }
+
     };
 
     wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
@@ -380,6 +394,9 @@ namespace opt {
     void wmaxsmt::collect_statistics(statistics& st) const {
         // no-op
     }
+    void wmaxsmt::get_model(model_ref& mdl) {
+        m_imp->get_model(mdl);
+    }
 
 
     
diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h
index 3b00e1690..01793b949 100644
--- a/src/opt/weighted_maxsat.h
+++ b/src/opt/weighted_maxsat.h
@@ -40,6 +40,7 @@ namespace opt {
         virtual expr_ref_vector get_assignment() const;
         virtual void set_cancel(bool f);
         virtual void collect_statistics(statistics& st) const;
+        virtual void get_model(model_ref& mdl);
     };
 };
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index c6d86bdf8..944414267 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -348,13 +348,24 @@ namespace smt {
         context & ctx   = get_context();
         simplifier & s  = ctx.get_simplifier();
         expr_ref s_ante(m), s_conseq(m);
+        expr* s_conseq_n, * s_ante_n;
+        bool negated;
         proof_ref pr(m);
+
         s(ante, s_ante, pr);
+        negated = m.is_not(s_ante, s_ante_n);
+        if (negated) s_ante = s_ante_n;
         ctx.internalize(s_ante, false);
         literal l_ante = ctx.get_literal(s_ante);
+        if (negated) l_ante.neg();
+
         s(conseq, s_conseq, pr);
+        negated = m.is_not(s_conseq, s_conseq_n);
+        if (negated) s_conseq = s_conseq_n;
         ctx.internalize(s_conseq, false);
         literal l_conseq = ctx.get_literal(s_conseq);
+        if (negated) l_conseq.neg();
+
         literal lits[2] = {l_ante, l_conseq};
         ctx.mk_th_axiom(get_id(), 2, lits);
         if (ctx.relevancy()) {
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index e2ec2c48a..33cc4105e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -38,9 +38,9 @@ namespace smt {
     }
 
     void theory_pb::ineq::reset() {
-        m_max_coeff.reset();
+        m_max_watch.reset();
         m_watch_sz = 0;
-        m_max_sum.reset();
+        m_watch_sum.reset();
         m_num_propagations = 0;
         m_compilation_threshold = UINT_MAX;
         m_compiled = l_false;
@@ -341,10 +341,10 @@ namespace smt {
         // TBD: special cases: args.size() == 1
         
         // maximal coefficient:
-        numeral& max_coeff = c->m_max_coeff;
-        max_coeff = numeral::zero();
+        numeral& max_watch = c->m_max_watch;
+        max_watch = numeral::zero();
         for (unsigned i = 0; i < args.size(); ++i) {
-            max_coeff = std::max(max_coeff, args[i].second);
+            max_watch = std::max(max_watch, args[i].second);
         }
 
 
@@ -448,13 +448,13 @@ namespace smt {
             std::swap(c.m_args[ineq_index], c.m_args[c.watch_size()-1]);
         }
         --c.m_watch_sz;
-        c.m_max_sum  -= coeff;
-        if (c.max_coeff() == coeff) {
+        c.m_watch_sum  -= coeff;
+        if (c.max_watch() == coeff) {
             coeff = c.coeff(0);
-            for (unsigned i = 1; coeff != c.max_coeff() && i < c.m_watch_sz; ++i) {
+            for (unsigned i = 1; coeff != c.max_watch() && i < c.watch_size(); ++i) {
                 if (coeff < c.coeff(i)) coeff = c.coeff(i);
             }
-            c.set_max_coeff(coeff);
+            c.set_max_watch(coeff);
         }
 
         // current index of unwatched literal is c.watch_size().
@@ -463,12 +463,18 @@ namespace smt {
     void theory_pb::add_watch(ineq& c, unsigned i) {
         literal lit = c.lit(i);
         bool_var v = lit.var();
-        c.m_max_sum += c.coeff(i);
+        numeral coeff = c.coeff(i);
+        c.m_watch_sum += coeff;
         SASSERT(i >= c.watch_size());
+        
         if (i > c.watch_size()) {
             std::swap(c.m_args[i], c.m_args[c.watch_size()]);
         }
         ++c.m_watch_sz;
+        if (coeff > c.max_watch()) {
+            c.set_max_watch(coeff);
+        }
+
         ptr_vector<ineq>* ineqs;
         if (!m_watch.find(lit.index(), ineqs)) {
             ineqs = alloc(ptr_vector<ineq>);
@@ -515,43 +521,6 @@ namespace smt {
         return FC_DONE;
     }
 
-    void theory_pb::validate_final_check() {
-        u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
-        for (; itc != endc; ++itc) {
-            validate_final_check(*itc->m_value);                
-        }
-    }
-
-    void theory_pb::validate_final_check(ineq& c) {
-        context& ctx = get_context();
-
-        if (ctx.get_assignment(c.lit()) == l_undef) {
-            return;
-        }
-        if (!ctx.is_relevant(c.lit())) {
-            return;
-        }
-        numeral sum = numeral::zero(), maxsum = numeral::zero();
-        for (unsigned i = 0; i < c.size(); ++i) {
-            switch(ctx.get_assignment(c.lit(i))) {
-            case l_true:
-                sum += c.coeff(i);
-            case l_undef:
-                maxsum += c.coeff(i);
-                break;
-            }
-        }
-        TRACE("pb", display(tout << "validate: ", c, true);
-              tout << "sum: " << sum << " " << maxsum << " ";
-              tout << ctx.get_assignment(c.lit()) << "\n";
-              );
-
-        SASSERT(sum <= maxsum);
-        SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
-        SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));
-    }
-
-
     void theory_pb::assign_eh(bool_var v, bool is_true) {
         context& ctx = get_context();
         ptr_vector<ineq>* ineqs = 0;
@@ -636,15 +605,17 @@ namespace smt {
             add_clause(c, lits);
         }
         else {
-            c.m_max_sum = numeral::zero();
+            c.m_watch_sum = numeral::zero();
             c.m_watch_sz = 0;
-            for (unsigned i = 0; c.max_sum() < c.k() + c.max_coeff() && i < c.size(); ++i) {
+            c.m_max_watch = numeral::zero();
+            for (unsigned i = 0; c.watch_sum() < c.k() + c.max_watch() && i < c.size(); ++i) {
                 if (ctx.get_assignment(c.lit(i)) != l_false) {
                     add_watch(c, i);
                 }       
             }
-            SASSERT(c.max_sum() >= c.k());
+            SASSERT(c.watch_sum() >= c.k());
             m_assign_ineqs_trail.push_back(&c);
+            DEBUG_CODE(validate_watch(c););
         }
 
         // perform unit propagation
@@ -653,7 +624,7 @@ namespace smt {
             lits.push_back(c.lit());
             for (unsigned i = 0; i < c.size(); ++i) {
                 if (ctx.get_assignment(c.lit(i)) == l_undef) {
-                    SASSERT(validate_assign(c, lits, c.lit(i)));
+                    DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
                     add_assign(c, lits, c.lit(i));
                 }                
             }
@@ -677,20 +648,20 @@ namespace smt {
         SASSERT(is_true == c.lit(w).sign());
 
         //
-        // max_sum is decreased.
+        // watch_sum is decreased.
         // Adjust set of watched literals.
         //
         
         numeral k = c.k();
         numeral coeff = c.coeff(w);
         
-        for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) {
+        for (unsigned i = c.watch_size(); c.watch_sum() - coeff < k + c.max_watch() && i < c.size(); ++i) {
             if (ctx.get_assignment(c.lit(i)) != l_false) {
                 add_watch(c, i);
             }
         }        
         
-        if (c.max_sum() - coeff < k) {
+        if (c.watch_sum() - coeff < k) {
             //
             // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0
             // create clause x1 or x2 or ~L
@@ -702,12 +673,13 @@ namespace smt {
         else {
             del_watch(watch, watch_index, c, w);
             removed = true;
-            if (c.max_sum() < k + c.max_coeff()) {
+            SASSERT(c.watch_sum() >= k);
+            if (c.watch_sum() < k + c.max_watch()) {
                 
                 //
                 // opportunities for unit propagation for unassigned 
                 // literals whose coefficients satisfy
-                // c.max_sum() < k
+                // c.watch_sum() < k
                 //
                 // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0
                 // Create clauses x1 or ~L or x2 
@@ -717,18 +689,14 @@ namespace smt {
                 literal_vector& lits = get_unhelpful_literals(c, true);
                 lits.push_back(c.lit());
                 for (unsigned i = 0; i < c.size(); ++i) {
-                    if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
-                        SASSERT(validate_assign(c, lits, c.lit(i)));
+                    if (c.watch_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
+                        DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
                         add_assign(c, lits, c.lit(i));                            
                     }
                 }
             }
             //
-            // else: c.max_sum() >= k + c.max_coeff()
-            // we might miss opportunities for unit propagation if 
-            // max_coeff is not the maximal coefficient
-            // of the current unassigned literal, but we can
-            // rely on eventually learning this from propagations.
+            // else: c.watch_sum() >= k + c.max_watch()
             //
         }
 
@@ -875,12 +843,10 @@ namespace smt {
 
     void theory_pb::inc_propagations(ineq& c) {
         ++c.m_num_propagations;
-#if 1
         if (c.m_compiled == l_false && c.m_num_propagations > c.m_compilation_threshold) {
             c.m_compiled = l_undef;
             m_to_compile.push_back(&c);
         }
-#endif
     }
 
     void theory_pb::restart_eh() {
@@ -970,69 +936,6 @@ namespace smt {
         m_ineqs_lim.resize(new_lim);
     }
 
-    void theory_pb::display(std::ostream& out) const {
-        u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
-        for (; it != end; ++it) {
-            out << "watch: " << to_literal(it->m_key) << " |-> ";
-            watch_list const& wl = *it->m_value;
-            for (unsigned i = 0; i < wl.size(); ++i) {
-                out << wl[i]->lit() << " ";
-            }
-            out << "\n";
-        }
-        u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
-        for (; itc != endc; ++itc) {
-            ineq& c = *itc->m_value;
-            display(out, c);
-        }
-    }
-
-    std::ostream& theory_pb::display(std::ostream& out, ineq const& c, bool values) const {
-        ast_manager& m = get_manager();
-        context& ctx = get_context();
-        out << c.lit();
-        if (c.lit() != null_literal) {
-            if (values) {
-                out << "@(" << ctx.get_assignment(c.lit());
-                if (ctx.get_assignment(c.lit()) != l_undef) {
-                    out << ":" << ctx.get_assign_level(c.lit());
-                }
-                out << ")";
-            }
-            expr_ref tmp(m);
-            ctx.literal2expr(c.lit(), tmp);
-            out << " " << tmp << "\n";
-        }
-        else {
-            out << " ";
-        }
-        for (unsigned i = 0; i < c.size(); ++i) {
-            literal l(c.lit(i));
-            if (!c.coeff(i).is_one()) {
-                out << c.coeff(i) << "*";
-            }
-            out << l;
-            if (values) {
-                out << "@(" << ctx.get_assignment(l);
-                if (ctx.get_assignment(l) != l_undef) {
-                    out << ":" << ctx.get_assign_level(l);
-                }
-                out << ")";
-            }
-            if (i + 1 < c.size()) {
-                out << " + ";
-            }
-        }
-        out << " >= " << c.m_k  << "\n";
-        if (c.m_num_propagations)    out << "propagations: " << c.m_num_propagations << " ";
-        if (c.max_coeff().is_pos())  out << "max_coeff: "   << c.max_coeff() << " ";
-        if (c.watch_size())          out << "watch size: "  << c.watch_size() << " ";
-        if (c.max_sum().is_pos())    out << "max-sum: "     << c.max_sum() << " ";
-        if (c.m_num_propagations || c.max_coeff().is_pos() || c.watch_size() || c.max_sum().is_pos()) out << "\n";
-        return out;
-    }
-
-
     literal_vector& theory_pb::get_lits() {
         m_literals.reset();
         return m_literals;
@@ -1087,34 +990,6 @@ namespace smt {
                    verbose_stream() << "\n";);
     }
 
-    bool theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
-        uint_set nlits;
-        context& ctx = get_context();
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            SASSERT(ctx.get_assignment(lits[i]) == l_false);
-            nlits.insert((~lits[i]).index());
-        }
-        SASSERT(ctx.get_assignment(l) == l_undef);
-        SASSERT(ctx.get_assignment(c.lit()) == l_true);
-        nlits.insert(l.index());
-        numeral sum = numeral::zero();
-        for (unsigned i = 0; i < c.size(); ++i) {
-            literal lit = c.lit(i);
-            if (!nlits.contains(lit.index())) {
-                sum += c.coeff(i);
-            }
-        }
-        if (sum >= c.k()) {
-            IF_VERBOSE(0, 
-                       display(verbose_stream(), c, true);
-                       for (unsigned i = 0; i < lits.size(); ++i) {
-                           verbose_stream() << lits[i] << " ";
-                       }
-                       verbose_stream() << " => " << l << "\n";);
-        }
-        SASSERT(sum < c.k());
-        return true;
-    }
 
     void theory_pb::set_mark(bool_var v, unsigned idx) {
         SASSERT(v != null_bool_var);
@@ -1149,7 +1024,12 @@ namespace smt {
         }
         else if (lvl > ctx.get_base_level()) {
             if (is_marked(v)) {
-                m_lemma.m_args[m_conseq_index[v]].second += coeff;
+                numeral& lcoeff = m_lemma.m_args[m_conseq_index[v]].second;
+                lcoeff += coeff;
+                if (lcoeff.is_zero()) {
+                    IF_VERBOSE(1, display(verbose_stream() << "remove 0 consequence", m_lemma, true););
+                    remove_from_lemma(m_lemma, m_conseq_index[v]);
+                }                
             }
             else {                
                 if (lvl == m_conflict_lvl) {
@@ -1243,10 +1123,9 @@ namespace smt {
    
         while (m_num_marks > 0) {
 
-            m_lemma.normalize();
             lbool is_sat = m_lemma.normalize();
             if (is_sat != l_undef) {
-                IF_VERBOSE(0, display(verbose_stream() << "created non-tautology lemma: ", m_lemma, true););
+                IF_VERBOSE(0, display(verbose_stream() << "lemma already evaluated ", m_lemma, true););
                 return false;
             }
             TRACE("pb", display(tout, m_lemma, true););
@@ -1261,11 +1140,22 @@ namespace smt {
                 --idx;
             }
             while (!is_marked(v) && idx > 0);
-            if (idx == 0) {
-                IF_VERBOSE(1, verbose_stream() << "BUG?!\n";);
+            if (idx == 0 && !is_marked(v)) {
+                //
+                // Yes, this can (currently) happen because
+                // the decisions for performing unit propagation
+                // are made asynchronously.
+                // In other words, PB unit propagation does not follow the
+                // same order as the assignment stack.
+                // It is not a correctness bug but causes to miss lemmas.
+                //
+                IF_VERBOSE(1, display_resolved_lemma(verbose_stream()););
+                for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                    unset_mark(m_lemma.lit(i));
+                }
                 return false;
             }
-
+            
             unsigned conseq_index = m_conseq_index[v];
             numeral conseq_coeff = m_lemma.coeff(conseq_index);
 
@@ -1274,16 +1164,8 @@ namespace smt {
 
             SASSERT(~conseq == m_lemma.lit(conseq_index));
 
-            // Remove conseq from lemma:
-            unsigned last = m_lemma.size()-1;
-            if (conseq_index != last) {
-                m_lemma.m_args[conseq_index] = m_lemma.m_args[last];
-                m_conseq_index[m_lemma.lit(conseq_index).var()] = conseq_index;
-            }
-            m_lemma.m_args.pop_back();
-            unset_mark(conseq);
+            remove_from_lemma(m_lemma, conseq_index);
 
-            --m_num_marks;
             b_justification js = ctx.get_justification(v);
 
             //
@@ -1359,14 +1241,19 @@ namespace smt {
 
         lbool is_true = m_lemma.normalize();
 
-        IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
+        IF_VERBOSE(2, display(verbose_stream() << "lemma: ", m_lemma););
         switch(is_true) {
         case l_true:
             UNREACHABLE();
             return false;
-        case l_false:
-            //add_assign(c, m_ineq_literals, false_literal);
-            //break;
+        case l_false: 
+            inc_propagations(c);
+            m_stats.m_num_conflicts++;
+            for (unsigned i = 0; i < m_ineq_literals.size(); ++i) {
+                m_ineq_literals[i].neg();
+            }
+            ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), 0, CLS_AUX_LEMMA, 0);
+            break;
         default: {
             app_ref tmp = m_lemma.to_expr(ctx, get_manager());
             internalize_atom(tmp, false);
@@ -1389,4 +1276,204 @@ namespace smt {
             }
         }
     }
+
+    void theory_pb::remove_from_lemma(ineq& c, unsigned idx) {
+        // Remove conseq from lemma:
+        literal lit = c.lit(idx);
+        unsigned last = c.size()-1;
+        if (idx != last) {
+            c.m_args[idx] = c.m_args[last];
+            m_conseq_index[c.lit(idx).var()] = idx;
+        }
+        c.m_args.pop_back();
+        unset_mark(lit);
+        --m_num_marks;
+    }
+
+
+    // debug methods
+
+    void theory_pb::validate_watch(ineq const& c) const {
+        context& ctx = get_context();
+        numeral sum = numeral::zero();
+        numeral max = numeral::zero();
+        for (unsigned i = 0; i < c.watch_size(); ++i) {
+            sum += c.coeff(i);
+            if (c.coeff(i) > max) {
+                max = c.coeff(i);
+            }
+        }
+        SASSERT(c.watch_sum() == sum);
+        SASSERT(sum >= c.k());
+        SASSERT(max == c.max_watch());
+    }
+
+    void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
+        uint_set nlits;
+        context& ctx = get_context();
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            SASSERT(ctx.get_assignment(lits[i]) == l_true);
+            nlits.insert((~lits[i]).index());
+        }
+        SASSERT(ctx.get_assignment(l) == l_undef);
+        SASSERT(ctx.get_assignment(c.lit()) == l_true);
+        nlits.insert(l.index());
+        numeral sum = numeral::zero();
+        for (unsigned i = 0; i < c.size(); ++i) {
+            literal lit = c.lit(i);
+            if (!nlits.contains(lit.index())) {
+                sum += c.coeff(i);
+            }
+        }
+        if (sum >= c.k()) {
+            IF_VERBOSE(0, 
+                       display(verbose_stream(), c, true);
+                       for (unsigned i = 0; i < lits.size(); ++i) {
+                           verbose_stream() << lits[i] << " ";
+                       }
+                       verbose_stream() << " => " << l << "\n";);
+        }
+        SASSERT(sum < c.k());
+    }
+
+    void theory_pb::validate_final_check() {
+        u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
+        for (; itc != endc; ++itc) {
+            validate_final_check(*itc->m_value);                
+        }
+    }
+
+    void theory_pb::validate_final_check(ineq& c) {
+        context& ctx = get_context();
+
+        if (ctx.get_assignment(c.lit()) == l_undef) {
+            return;
+        }
+        if (!ctx.is_relevant(c.lit())) {
+            return;
+        }
+        numeral sum = numeral::zero(), maxsum = numeral::zero();
+        for (unsigned i = 0; i < c.size(); ++i) {
+            switch(ctx.get_assignment(c.lit(i))) {
+            case l_true:
+                sum += c.coeff(i);
+            case l_undef:
+                maxsum += c.coeff(i);
+                break;
+            }
+        }
+        TRACE("pb", display(tout << "validate: ", c, true);
+              tout << "sum: " << sum << " " << maxsum << " ";
+              tout << ctx.get_assignment(c.lit()) << "\n";
+              );
+
+        SASSERT(sum <= maxsum);
+        SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
+        SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));
+    }
+
+    // display methods
+
+    void theory_pb::display_resolved_lemma(std::ostream& out) const {
+        context& ctx = get_context();
+        literal_vector const& lits = ctx.assigned_literals();                
+        bool_var v;
+        unsigned lvl;
+        out << "num marks: " << m_num_marks << "\n";
+        out << "conflict level: " << m_conflict_lvl << "\n";
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            v = lits[i].var();
+            lvl = ctx.get_assign_level(v);
+            out << lits[i]
+                << "@ " << lvl 
+                << " " << (is_marked(v)?"m":"u") 
+                << "\n";
+            
+            if (lvl == m_conflict_lvl && is_marked(v)) {
+                out << "skipped: " << lits[i] << ":"<< i << "\n";
+            }
+        }
+        display(out, m_lemma, true); 
+
+        unsigned nc = 0;
+        for (unsigned i = 0; i < m_lemma.size(); ++i) {
+            v = m_lemma.lit(i).var();
+            lvl = ctx.get_assign_level(v);
+            if (lvl == m_conflict_lvl) ++nc;
+            out << m_lemma.lit(i) 
+                << "@" << lvl 
+                << " " << (is_marked(v)?"m":"u") 
+                << " " << ctx.get_assignment(m_lemma.lit(i))
+                << "\n";
+        }
+        out << "num conflicts: " << nc << "\n";
+    }
+
+
+    std::ostream& theory_pb::display(std::ostream& out, ineq const& c, bool values) const {
+        ast_manager& m = get_manager();
+        context& ctx = get_context();
+        out << c.lit();
+        if (c.lit() != null_literal) {
+            if (values) {
+                out << "@(" << ctx.get_assignment(c.lit());
+                if (ctx.get_assignment(c.lit()) != l_undef) {
+                    out << ":" << ctx.get_assign_level(c.lit());
+                }
+                out << ")";
+            }
+            expr_ref tmp(m);
+            ctx.literal2expr(c.lit(), tmp);
+            out << " " << tmp << "\n";
+        }
+        else {
+            out << " ";
+        }
+        for (unsigned i = 0; i < c.size(); ++i) {
+            literal l(c.lit(i));
+            if (!c.coeff(i).is_one()) {
+                out << c.coeff(i) << "*";
+            }
+            out << l;
+            if (values) {
+                out << "@(" << ctx.get_assignment(l);
+                if (ctx.get_assignment(l) != l_undef) {
+                    out << ":" << ctx.get_assign_level(l);
+                }
+                out << ")";
+            }
+            if (i + 1 == c.watch_size()) {
+                out << " .w ";
+            }
+            if (i + 1 < c.size()) {
+                out << " + ";
+            }
+        }
+        out << " >= " << c.m_k  << "\n";
+        if (c.m_num_propagations)    out << "propagations: " << c.m_num_propagations << " ";
+        if (c.max_watch().is_pos())  out << "max_watch: "    << c.max_watch() << " ";
+        if (c.watch_size())          out << "watch size: "   << c.watch_size() << " ";
+        if (c.watch_sum().is_pos())  out << "watch-sum: "    << c.watch_sum() << " ";
+        if (c.m_num_propagations || c.max_watch().is_pos() || c.watch_size() || c.watch_sum().is_pos()) out << "\n";
+        return out;
+    }
+
+    void theory_pb::display(std::ostream& out) const {
+        u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
+        for (; it != end; ++it) {
+            out << "watch: " << to_literal(it->m_key) << " |-> ";
+            watch_list const& wl = *it->m_value;
+            for (unsigned i = 0; i < wl.size(); ++i) {
+                out << wl[i]->lit() << " ";
+            }
+            out << "\n";
+        }
+        u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
+        for (; itc != endc; ++itc) {
+            ineq& c = *itc->m_value;
+            display(out, c);
+        }
+    }
+
+
 }
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index fc1a61186..34cd479a1 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -48,11 +48,11 @@ namespace smt {
             numeral         m_k;        // invariants: m_k > 0, coeffs[i] > 0
             
             // Watch the first few positions until the sum satisfies:
-            // sum coeffs[i] >= m_lower + max_coeff
+            // sum coeffs[i] >= m_lower + max_watch
             
-            numeral         m_max_coeff;    // maximal coefficient.
+            numeral         m_max_watch;    // maximal coefficient.
             unsigned        m_watch_sz;     // number of literals being watched.
-            numeral         m_max_sum;      // maximal sum of watch literals.
+            numeral         m_watch_sum;      // maximal sum of watch literals.
             unsigned        m_num_propagations;
             unsigned        m_compilation_threshold;
             lbool           m_compiled;
@@ -69,9 +69,9 @@ namespace smt {
 
             unsigned size() const { return m_args.size(); }
 
-            numeral const& max_sum() const { return m_max_sum; }
-            numeral const& max_coeff() const { return m_max_coeff; }
-            void set_max_coeff(numeral const& n) { m_max_coeff = n; }
+            numeral const& watch_sum() const { return m_watch_sum; }
+            numeral const& max_watch() const { return m_max_watch; }
+            void set_max_watch(numeral const& n) { m_max_watch = n; }
             
             unsigned watch_size() const { return m_watch_sz; }
 
@@ -118,6 +118,7 @@ namespace smt {
 
         std::ostream& display(std::ostream& out, ineq const& c, bool values = false) const;
         virtual void display(std::ostream& out) const;
+        void display_resolved_lemma(std::ostream& out) const;
 
         void add_clause(ineq& c, literal_vector const& lits);
         void add_assign(ineq& c, literal_vector const& lits, literal l);
@@ -152,12 +153,14 @@ namespace smt {
         bool resolve_conflict(ineq& c);
         void process_antecedent(literal l, numeral coeff);
         void process_ineq(ineq& c, literal conseq, numeral coeff);
+        void remove_from_lemma(ineq& c, unsigned idx);
 
         void hoist_maximal_values();
 
         void validate_final_check();
         void validate_final_check(ineq& c);
-        bool validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
+        void validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
+        void validate_watch(ineq const& c) const;
     public:
         theory_pb(ast_manager& m);