diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp
index f8979edce..9bab8e624 100644
--- a/src/opt/inc_sat_solver.cpp
+++ b/src/opt/inc_sat_solver.cpp
@@ -93,11 +93,12 @@ public:
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(num_assumptions, assumptions, dep2asm);
-        extract_assumptions(dep2asm, m_asms);
         if (r != l_true) return r;
+        extract_assumptions(dep2asm, m_asms);
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         switch (r) {
         case l_true:
+            check_assumptions(dep2asm);
             break;
         case l_false:
             // TBD: expr_dependency core is not accounted for.
@@ -271,6 +272,23 @@ private:
 
     }
 
+    void check_assumptions(dep2asm_t& dep2asm) {
+        sat::model const & ll_m = m_solver.get_model();
+        dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
+        for (; it != end; ++it) {
+            sat::literal lit = it->m_value;
+            lbool polarity = lit.sign()?l_false:l_true;
+            lbool value = sat::value_at(lit.var(), ll_m); 
+            if (value != polarity) {
+                std::cout << mk_pp(it->m_key, m) << " evaluates to " << value << "\n";
+                std::cout << m_asms << "\n";
+                m_solver.display_assignment(std::cout);
+                // m_solver.display(std::cout);
+                throw default_exception("bad state");
+            }
+        }
+    }
+
     // TBD: this is super-expensive because of the
     // bit-blasting model converter.
 
@@ -286,6 +304,7 @@ private:
                 continue;
             }
             sat::bool_var v = it->m_value;
+            // std::cout << mk_pp(n, m) << " -> " << sat::value_at(v, ll_m) << "\n";
             switch (sat::value_at(v, ll_m)) {
             case l_true: 
                 md->register_decl(to_app(n)->get_decl(), m.mk_true()); 
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 5e7dac0f7..f879ff99a 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -59,6 +59,8 @@ Notes:
 #include "ast_pp.h"
 #include "mus.h"
 #include "mss.h"
+#include "inc_sat_solver.h"
+
 
 using namespace opt;
 
@@ -117,7 +119,7 @@ public:
         else {
             asum = mk_fresh_bool("soft");
             fml = m.mk_iff(asum, e);
-            m_s->assert_expr(fml);
+            s().assert_expr(fml);
         }
         new_assumption(asum, w);
         m_upper += w;
@@ -138,17 +140,17 @@ public:
         while (true) {
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
-                  m_s->display(tout);
+                  s().display(tout);
                   tout << "\n";
                   display(tout);
                   );
-            lbool is_sat = m_s->check_sat(m_asms.size(), m_asms.c_ptr());
+            lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
             if (m_cancel) {
                 return l_undef;
             }
             switch (is_sat) {
             case l_true: {
-                m_s->get_model(m_model);
+                s().get_model(m_model);
                 expr_ref tmp(m);
                 DEBUG_CODE(
                     for (unsigned i = 0; i < m_asms.size(); ++i) {
@@ -157,6 +159,7 @@ public:
                     });
                 for (unsigned i = 0; i < m_soft.size(); ++i) {
                     VERIFY(m_model->eval(m_soft[i].get(), tmp));
+                    std::cout << mk_pp(m_soft[i].get(), m) << " -> " << tmp << "\n";
                     m_assignment[i] = m.is_true(tmp);
                 }
                 m_upper = m_lower;
@@ -186,7 +189,7 @@ public:
         while (m_lower < m_upper) {            
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
-                  m_s->display(tout);
+                  s().display(tout);
                   tout << "\n";
                   display(tout);
                   );
@@ -203,11 +206,10 @@ public:
                 return l_true;
             case l_true:
                 SASSERT(cores.empty() || mcs.empty());
-                SASSERT(!cores.empty() || !mcs.empty());
                 for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
                     is_sat = process_unsat(cores[i]);
                 }
-                if (is_sat == l_true && !mcs.empty()) {
+                if (is_sat == l_true && cores.empty()) {
                     is_sat = process_sat(mcs);
                 }
                 if (is_sat != l_true) {
@@ -216,7 +218,7 @@ public:
                 break;
             }
         }
-        m_lower = m_lower;        
+        m_lower = m_upper;
         return l_true;
     }
 
@@ -247,7 +249,7 @@ public:
         ptr_vector<expr> core;
         while (is_sat == l_false) {
             core.reset();
-            m_s->get_unsat_core(core);
+            s().get_unsat_core(core);
             is_sat = minimize_core(core);
             if (is_sat != l_true) {
                 break;
@@ -261,7 +263,7 @@ public:
             TRACE("opt",
                   display_vec(tout << "core: ", core.size(), core.c_ptr());
                   display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr()););
-            is_sat = m_s->check_sat(asms.size(), asms.c_ptr());            
+            is_sat = s().check_sat(asms.size(), asms.c_ptr());            
         }
         TRACE("opt", 
               tout << "num cores: " << cores.size() << "\n";
@@ -280,9 +282,8 @@ public:
     lbool process_sat(ptr_vector<expr>& corr_set) {
         expr_ref fml(m), tmp(m);
         TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
-        SASSERT(!corr_set.empty()); // we should somehow stop if all soft are satisfied.
         if (corr_set.empty()) {
-            return l_false;
+            return l_true;
         }
         
         remove_core(corr_set);
@@ -314,7 +315,7 @@ public:
         TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
         max_resolve(core, w);
         fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
-        m_s->assert_expr(fml);
+        s().assert_expr(fml);
         m_lower += w;
         IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
         return l_true;
@@ -407,9 +408,9 @@ public:
             if (i > 2) {
                 dd = mk_fresh_bool("d");
                 fml = m.mk_implies(dd, d);
-                m_s->assert_expr(fml);
+                s().assert_expr(fml);
                 fml = m.mk_implies(dd, b_i);
-                m_s->assert_expr(fml);
+                s().assert_expr(fml);
                 d = dd;
             }
             else {
@@ -419,7 +420,7 @@ public:
             cls = m.mk_or(b_i1, d);
             fml = m.mk_implies(asum, cls);
             new_assumption(asum, w);
-            m_s->assert_expr(fml);
+            s().assert_expr(fml);
         }
     }
 
@@ -449,20 +450,20 @@ public:
             if (i > 2) {
                 d = mk_fresh_bool("d");
                 fml = m.mk_implies(d, cls);
-                m_s->assert_expr(fml);
+                s().assert_expr(fml);
             }
             else {
                 d = cls;
             }
             asum = mk_fresh_bool("a");
             fml = m.mk_implies(asum, b_i1);
-            m_s->assert_expr(fml);
+            s().assert_expr(fml);
             fml = m.mk_implies(asum, cls);
-            m_s->assert_expr(fml);
+            s().assert_expr(fml);
             new_assumption(asum, w);
         }
         fml = m.mk_or(m_B.size(), m_B.c_ptr());
-        m_s->assert_expr(fml);
+        s().assert_expr(fml);
     }
 
     lbool try_improve_bound(vector<ptr_vector<expr> >& cores, ptr_vector<expr>& mcs) {
@@ -473,25 +474,29 @@ public:
         while (true) {
             rational upper = m_max_upper;
             unsigned sz = 0;
-            for (unsigned i = 0; m_upper <= upper && i < asms.size(); ++i, ++sz) {
+            for (unsigned i = 0; m_upper <= rational(2)*upper && i < asms.size(); ++i, ++sz) {
                 upper -= get_weight(asms[i].get());
             }
-            lbool is_sat = m_s->check_sat(sz, asms.c_ptr());
+            lbool is_sat = s().check_sat(sz, asms.c_ptr());
             switch (is_sat) {
             case l_true: {
-                ptr_vector<expr> lits;
-                lits.append(asms.size(), asms.c_ptr());
+                s().get_model(m_model); // last model is best way to reduce search space.
+                update_assignment();
+                ptr_vector<expr> mss;
+                mss.append(asms.size(), asms.c_ptr());
                 set_mus(false);
-                is_sat = m_mss(cores, lits);
+                is_sat = m_mss(cores, mss, mcs);
                 set_mus(true);
                 if (is_sat != l_true) {
                     return is_sat;
                 }
                 m_mss.get_model(m_model); // last model is best way to reduce search space.
                 update_assignment();
-                if (cores.empty() || asms.size() < cores.back().size()) {
+                if (!cores.empty() && mcs.size() > cores.back().size()) {
+                    mcs.reset();
+                }
+                else {
                     cores.reset();
-                    mcs.append(asms.size(), asms.c_ptr());                    
                 }
                 return l_true;
             }
@@ -499,7 +504,7 @@ public:
                 return l_undef;
             case l_false:
                 core.reset();
-                m_s->get_unsat_core(core);
+                s().get_unsat_core(core);
                 is_sat = minimize_core(core);
                 if (is_sat != l_true) {
                     break;
@@ -531,23 +536,29 @@ public:
 
     void update_assignment() {
         rational upper(0);
+        expr_ref tmp(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            expr_ref tmp(m);
             expr* n = m_soft[i].get();
             VERIFY(m_model->eval(n, tmp));
-            CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), 
-                   tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
-
-            m_assignment[i] = m.is_true(tmp);
-            if (!m_assignment[i]) {
+            if (!m.is_true(tmp)) {
                 upper += m_weights[i];
             }
+            CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), 
+                   tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
+        }
+        if (upper >= m_upper) {
+            return;
+        }
+
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            expr* n = m_soft[i].get();
+            VERIFY(m_model->eval(n, tmp));
+            m_assignment[i] = m.is_true(tmp);
         }
-        SASSERT(upper <= m_upper);
         m_upper = upper;
+        // verify_assignment();
         IF_VERBOSE(1, verbose_stream() << 
                    "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
-
     }
 
     void remove_soft(ptr_vector<expr> const& core, expr_ref_vector& asms) {
@@ -579,6 +590,26 @@ public:
         m_max_upper = m_upper;
     }
 
+    void verify_assignment() {
+        IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);        
+        ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);        
+        for (unsigned i = 0; i < m_assertions.size(); ++i) {
+            sat_solver->assert_expr(m_assertions[i].get());
+        }
+        expr_ref n(m);
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            n = m_soft[i].get();
+            if (!m_assignment[i]) {
+                n = m.mk_not(n);
+            }
+            sat_solver->assert_expr(n);
+        }
+        lbool is_sat = sat_solver->check_sat(0, 0);
+        if (is_sat == l_false) {
+            IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
+        }
+    }
+
 };
 
 opt::maxsmt_solver_base* opt::mk_maxres(ast_manager& m, opt_solver* s, params_ref& p, 
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index eb0a65ce9..572c6e66c 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -134,6 +134,7 @@ namespace opt {
         unsigned sz = s().get_num_assertions();
         for (unsigned i = 0; i < sz; ++i) {
             sat_solver->assert_expr(s().get_assertion(i));
+            m_assertions.push_back(s().get_assertion(i));
         }   
         m_s = sat_solver;
     }
@@ -232,16 +233,24 @@ namespace opt {
                    });
 
         DEBUG_CODE(if (is_sat == l_true) {
-                m_s->push();
-                commit_assignment();
-                VERIFY(l_true == m_s->check_sat(0,0));
-                m_s->pop(1);
-                // TBD: check that all extensions are unsat too
+                       verify_assignment();
+                   });
 
-            });
+        // TBD: check that all extensions are unsat too
+        
         return is_sat;
     }
 
+    void maxsmt::verify_assignment() {
+        m_s->push();
+        commit_assignment();
+        if (l_true != m_s->check_sat(0,0)) {
+            IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
+            UNREACHABLE();
+        }
+        m_s->pop(1);
+    }
+
     bool maxsmt::get_assignment(unsigned idx) const {
         if (m_msolver) {
             return m_msolver->get_assignment(idx);
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index df03499c9..a36269447 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -48,6 +48,7 @@ namespace opt {
         ast_manager&     m;
         volatile bool    m_cancel;
         expr_ref_vector  m_soft;
+        expr_ref_vector  m_assertions;
         vector<rational> m_weights;
         rational         m_lower;
         rational         m_upper;
@@ -65,6 +66,7 @@ namespace opt {
         maxsmt_solver_base(opt_solver* s, ast_manager& m, params_ref& p,
                            vector<rational> const& ws, expr_ref_vector const& soft): 
             m_s(s), m(m), m_cancel(false), m_soft(m),
+            m_assertions(m),
             m_enable_sls(false), m_enable_sat(false),
             m_sls_enabled(false), m_sat_enabled(false) {
             m_s->get_model(m_model);
@@ -148,6 +150,8 @@ namespace opt {
     private:
 
         bool is_maxsat_problem(vector<rational> const& ws) const;        
+        
+        void verify_assignment();
 
     };
 
diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index 73c35bd79..d796a2b92 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -144,7 +144,7 @@ namespace opt {
         m_todo.resize(j);
     }       
     
-    lbool mss::operator()(vector<exprs> const& _cores, exprs& literals) {
+    lbool mss::operator()(vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
         m_mss.reset();
         m_todo.reset();
         m_s->get_model(m_model);
@@ -171,6 +171,11 @@ namespace opt {
             TRACE("opt", display(tout););
             literals.reset();
             literals.append(m_mss);
+            mcs.reset();
+            expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
+            for (; it != end; ++it) {
+                mcs.push_back(*it);
+            }
             SASSERT(check_result());
         }
         m_mcs.reset();
@@ -203,12 +208,12 @@ namespace opt {
         unsigned sz_save = m_mss.size();
         m_mss.append(sz, core.c_ptr());
         lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
+        IF_VERBOSE(1, display_vec(verbose_stream(), sz, core.c_ptr()););
         m_mss.resize(sz_save);
         switch (is_sat) {
         case l_true:
             m_s->get_model(m_model);
-            update_mss();
-            // sz entries from core should now be in mss.
+            update_mss();           
             DEBUG_CODE(
                 for (unsigned i = 0; i < sz; ++i) {
                     SASSERT(m_mss_set.contains(core[i]));
diff --git a/src/opt/mss.h b/src/opt/mss.h
index 34767beb6..9f14f66c3 100644
--- a/src/opt/mss.h
+++ b/src/opt/mss.h
@@ -35,7 +35,7 @@ namespace opt {
         mss(ref<solver>& s, ast_manager& m);
         ~mss();
         
-        lbool operator()(vector<exprs> const& cores, exprs& literals);
+        lbool operator()(vector<exprs> const& cores, exprs& literals, exprs& mcs);
                 
         void set_cancel(bool f) { m_cancel = f; }
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 969a6c37a..76d3a1730 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -917,6 +917,9 @@ namespace sat {
 
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
+            if (s.is_external(l.var()) || s.was_eliminated(l.var())) {
+                return;
+            }
             model_converter::entry * new_entry = 0;
             {
                 m_to_remove.reset();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 91dada236..870544d92 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -880,7 +880,9 @@ namespace sat {
         TRACE("sat", 
               for (unsigned i = 0; i < num_lits; ++i) 
                   tout << lits[i] << " ";
-              tout << "\n";);
+              tout << "\n";
+              m_mc.display(tout);
+              );
 #define _INSERT_LIT(_l_)                     \
         SASSERT(is_external((_l_).var()));   \
         m_assumption_set.insert(_l_);        \
@@ -950,7 +952,7 @@ namespace sat {
         m_simplifier(false);
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
-
+        
         if (!m_learned.empty()) {
             m_simplifier(true);
             CASSERT("sat_missed_prop", check_missed_propagation());
@@ -1000,6 +1002,7 @@ namespace sat {
         IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";);
         if (!check_model(m_model))
             throw solver_exception("check model failed");
+
         if (m_clone) {
             IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
             if (!m_clone->check_model(m_model))
@@ -1018,7 +1021,12 @@ namespace sat {
             for (; it != end; ++it) {
                 clause const & c = *(*it);
                 if (!c.satisfied_by(m)) {
-                    TRACE("sat_model_bug", tout << "failed: " << c << "\n";);
+                    TRACE("sat", tout << "failed: " << c << "\n";
+                          tout << "assumptions: " << m_assumptions << "\n";
+                          tout << "trail: " << m_trail << "\n";
+                          tout << "model: " << m << "\n";      
+                          m_mc.display(tout);
+                          );
                     ok = false;
                 }
             }
@@ -1036,15 +1044,28 @@ namespace sat {
                         continue;
                     literal l2 = it2->get_literal();
                     if (value_at(l2, m) != l_true) {
-                        TRACE("sat_model_bug", tout << "failed binary: " << l << " " << l2 << " learned: " << it2->is_learned() << "\n";);
+                        TRACE("sat", tout << "failed binary: " << l << " " << l2 << " learned: " << it2->is_learned() << "\n";
+                          m_mc.display(tout););
                         ok = false;
                     }
                 }
             }
         }
-        if (!m_mc.check_model(m))
+        for (unsigned i = 0; i < m_assumptions.size(); ++i) {
+            if (value_at(m_assumptions[i], m) != l_true) {
+                TRACE("sat", 
+                      tout << m_assumptions[i] << " does not model check\n";
+                      tout << "trail: " << m_trail << "\n";
+                      tout << "model: " << m << "\n";      
+                      m_mc.display(tout);
+                      );
+                ok = false;
+            }
+        }
+        if (ok && !m_mc.check_model(m)) {
             ok = false;
-        TRACE("sat", tout << "check: " << ok << "\n" << m << "\n";);
+            TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout););
+        }
         return ok;
     }
 
@@ -1532,73 +1553,99 @@ namespace sat {
         }        
     }
 
-    void solver::resolve_conflict_for_unsat_core() {
-        TRACE("sat", display(tout););
+    void solver::process_consequent_for_unsat_core(literal consequent, justification const& js) {
+        TRACE("sat", tout << "processing consequent: " << consequent << "\n";
+              display_justification(tout << "js kind: ", js);
+              tout << "\n";);
+        switch (js.get_kind()) {
+        case justification::NONE:
+            break;
+        case justification::BINARY:
+            process_antecedent_for_unsat_core(~(js.get_literal()));
+            break;
+        case justification::TERNARY:
+            process_antecedent_for_unsat_core(~(js.get_literal1()));
+            process_antecedent_for_unsat_core(~(js.get_literal2()));
+            break;
+        case justification::CLAUSE: {
+            clause & c = *(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_for_unsat_core(~c[0]);
+                    i = 2;
+                }
+            }
+            unsigned sz  = c.size();
+            for (; i < sz; i++)
+                process_antecedent_for_unsat_core(~c[i]);
+            break;
+        }
+        case justification::EXT_JUSTIFICATION: {
+            fill_ext_antecedents(consequent, js);
+            literal_vector::iterator it  = m_ext_antecedents.begin();
+            literal_vector::iterator end = m_ext_antecedents.end();
+            for (; it != end; ++it)
+                process_antecedent_for_unsat_core(*it);
+            break;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
 
+    void solver::resolve_conflict_for_unsat_core() {
+        TRACE("sat", display(tout);
+              unsigned level = 0;
+              for (unsigned i = 0; i < m_trail.size(); ++i) {
+                  literal l = m_trail[i];
+                  if (level != m_level[l.var()]) {
+                      level = m_level[l.var()];
+                      tout << level << ": ";
+                  }
+                  tout << l;
+                  if (m_mark[l.var()]) {
+                      tout << "*";
+                  }
+                  tout << " ";
+              }
+              tout << "\n";
+              );
+
+        m_core.reset();
         if (m_conflict_lvl == 0) {
             return;
         }
 
         unsigned old_size = m_unmark.size();        
-        m_core.reset();
         int idx = skip_literals_above_conflict_level();
 
         if (m_not_l != null_literal) {
-            TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
+            justification js = m_justification[m_not_l.var()];
+            TRACE("sat", tout << "not_l: " << m_not_l << "\n";
+                  display_justification(tout, js);
+                  tout << "\n";);
+
             process_antecedent_for_unsat_core(m_not_l);
             if (is_assumption(~m_not_l)) {
                 m_core.push_back(~m_not_l);
             }
+            else {
+                process_consequent_for_unsat_core(m_not_l, js);
+            }
         }
-        
-            
+                    
         literal consequent = m_not_l;
         justification js   = m_conflict;
 
-        do {
-            TRACE("sat", tout << "processing consequent: " << consequent << "\n";
-                  tout << "js kind: " << js << "\n";);
-            switch (js.get_kind()) {
-            case justification::NONE:
-                break;
-            case justification::BINARY:
-                process_antecedent_for_unsat_core(~(js.get_literal()));
-                break;
-            case justification::TERNARY:
-                process_antecedent_for_unsat_core(~(js.get_literal1()));
-                process_antecedent_for_unsat_core(~(js.get_literal2()));
-                break;
-            case justification::CLAUSE: {
-                clause & c = *(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_for_unsat_core(~c[0]);
-                        i = 2;
-                    }
-                }
-                unsigned sz  = c.size();
-                for (; i < sz; i++)
-                    process_antecedent_for_unsat_core(~c[i]);
-                break;
-            }
-            case justification::EXT_JUSTIFICATION: {
-                fill_ext_antecedents(consequent, js);
-                literal_vector::iterator it  = m_ext_antecedents.begin();
-                literal_vector::iterator end = m_ext_antecedents.end();
-                for (; it != end; ++it)
-                    process_antecedent_for_unsat_core(*it);
-                break;
-            }
-            default:
-                UNREACHABLE();
-                break;
-            }
-
+        while (true) {
+            process_consequent_for_unsat_core(consequent, js);
+            idx--;
             while (idx >= 0) {
                 literal l = m_trail[idx];
                 if (is_marked(l.var()))
@@ -1611,17 +1658,16 @@ namespace sat {
             }
             consequent     = m_trail[idx];
             if (lvl(consequent) < m_conflict_lvl) {
+                TRACE("sat", tout << consequent << " at level " << lvl(consequent) << "\n";);
                 break;
             }
             bool_var c_var = consequent.var();
             SASSERT(lvl(consequent) == m_conflict_lvl);
             js             = m_justification[c_var];
-            idx--;
         }        
-        while (idx > 0);
         reset_unmark(old_size);
         if (m_config.m_minimize_core) {
-            m_mus(); //ignore return value on cancelation.
+            m_mus(); // ignore return value on cancelation.
         }
     }
 
@@ -2362,6 +2408,13 @@ namespace sat {
         out << ")\n";
     }
 
+    void solver::display_justification(std::ostream & out, justification const& js) const {
+        out << js;
+        if (js.is_clause()) {
+            out << *(m_cls_allocator.get_clause(js.get_clause_offset()));
+        }
+    }
+
     unsigned solver::num_clauses() const {
         unsigned num_cls = 0;
         num_cls += m_trail.size(); // units;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 056567bf9..e0b386c24 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -328,6 +328,7 @@ namespace sat {
         unsigned get_max_lvl(literal consequent, justification js);
         void process_antecedent(literal antecedent, unsigned & num_marks);
         void process_antecedent_for_unsat_core(literal antecedent);
+        void process_consequent_for_unsat_core(literal consequent, justification const& js);
         void fill_ext_antecedents(literal consequent, justification js);
         unsigned skip_literals_above_conflict_level();
         void forget_phase_of_vars(unsigned from_lvl);
@@ -425,11 +426,12 @@ namespace sat {
         void display(std::ostream & out) const;
         void display_watches(std::ostream & out) const;
         void display_dimacs(std::ostream & out) const;
+        void display_assignment(std::ostream & out) const;
+        void display_justification(std::ostream & out, justification const& j) const;
 
     protected:
         void display_binary(std::ostream & out) const;
         void display_units(std::ostream & out) const;
-        void display_assignment(std::ostream & out) const;
         unsigned num_clauses() const;
         bool is_unit(clause const & c) const;
         bool is_empty(clause const & c) const;