diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt
index 41051fd40..6ffbb8c71 100644
--- a/contrib/cmake/src/sat/CMakeLists.txt
+++ b/contrib/cmake/src/sat/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(sat
     sat_clause_use_list.cpp
     sat_cleaner.cpp
     sat_config.cpp
+    sat_drat.cpp
     sat_elim_eqs.cpp
     sat_iff3_finder.cpp
     sat_integrity_checker.cpp
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index c4929d35b..6c8d5af3a 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -352,9 +352,9 @@ public:
         while (is_sat == l_false) {
             core.reset();
             s().get_unsat_core(core);
-            //expr_ref_vector core1(m);
-            //core1.append(core.size(), core.c_ptr());
-            //std::cout << core1 << "\n";
+            expr_ref_vector core1(m);
+            core1.append(core.size(), core.c_ptr());
+            std::cout << core1 << "\n";
             // verify_core(core);
             model_ref mdl;
             get_mus_model(mdl);
diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 712162e44..2bcccfb1a 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -94,7 +94,7 @@ namespace sat {
                     alit = c[j];
                 }
             }
-            set_conflict(c, alit);
+            set_conflict(c);
         }
         else if (j == bound) {
             for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
@@ -136,32 +136,40 @@ namespace sat {
     }
 
     void card_extension::assign(card& c, literal lit) {
-        if (value(lit) == l_true) {
-            return;
+        switch (value(lit)) {
+        case l_true: 
+            break;
+        case l_false: 
+            set_conflict(c); 
+            break;
+        default:
+            m_stats.m_num_propagations++;
+            //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
+            SASSERT(validate_unit_propagation(c));
+            s().assign(lit, justification::mk_ext_justification(c.index()));
+            break;
         }
-        m_stats.m_num_propagations++;
-        //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
-        SASSERT(validate_unit_propagation(c));
-        s().assign(lit, justification::mk_ext_justification(c.index()));
-        
     }
 
     void card_extension::watch_literal(card& c, literal lit) {
-        TRACE("sat", tout << "watch: " << lit << "\n";);
+        TRACE("sat_verbose", tout << "watch: " << lit << "\n";);
         init_watch(lit.var());
         ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
         if (cards == 0) {
             cards = alloc(ptr_vector<card>);
             m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
         }
-        TRACE("sat", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
+        TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
         cards->push_back(&c);
     }
 
-    void card_extension::set_conflict(card& c, literal lit) {
+    void card_extension::set_conflict(card& c) {
+        TRACE("sat", display(tout, c, true); );
         SASSERT(validate_conflict(c));
         m_stats.m_num_conflicts++;
-        if (!resolve_conflict(c, lit)) {            
+        literal lit = last_false_literal(c);
+        if (!resolve_conflict(c, lit)) {   
+            TRACE("sat", tout << "bail out conflict resolution\n";);
             m_conflict.reset();
             m_conflict.push_back(~c.lit()); 
             unsigned sz = c.size();
@@ -169,11 +177,40 @@ namespace sat {
                 m_conflict.push_back(c[i]);
             }
             m_conflict.push_back(lit);
-            SASSERT(validate_conflict(m_conflict));
+            // SASSERT(validate_conflict(m_conflict));
             s().assign(lit, justification::mk_ext_justification(0));
         }
         SASSERT(s().inconsistent());
     }
+
+    literal card_extension::last_false_literal(card& c) {
+        while (!m_active_var_set.empty()) m_active_var_set.erase();
+        reset_coeffs();
+        for (unsigned i = 0; i < c.size(); ++i) {
+            bool_var v = c[i].var();
+            m_active_var_set.insert(v);
+            m_active_vars.push_back(v);
+            m_coeffs.setx(v, c[i].sign() ? -1 : 1, 0); 
+        }
+        literal_vector const& lits = s().m_trail;
+        for (unsigned i = lits.size(); i > 0; ) {
+            --i;
+            literal lit = lits[i];
+            bool_var v = lit.var();
+            if (m_active_var_set.contains(v) && 
+                (m_coeffs[v] > 0 == lits[i].sign())) {
+                //std::cout << "last literal: " << lit << "\n";       
+                for (unsigned j = 0; j < c.size(); ++j) {
+                    if (~lit == c[j] && j != c.k()-1) {
+                        // std::cout << "POSITION " << j << " bound " << c.k() << "\n";
+                    }
+                }
+                return ~lit;
+            }
+        }
+        UNREACHABLE();
+        return null_literal;
+    }
     
     void card_extension::normalize_active_coeffs() {
         while (!m_active_var_set.empty()) m_active_var_set.erase();
@@ -244,7 +281,7 @@ namespace sat {
         if (m_conflict_lvl < lvl(c.lit()) || m_conflict_lvl == 0) {
             return false;
         }
-        std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n";
+        // std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n";
 
         reset_coeffs();
         m_num_marks = 0;
@@ -263,6 +300,8 @@ namespace sat {
             v = consequent.var();
             int offset = get_abs_coeff(v);
 
+            // TRACE("sat", display(tout, m_A););
+
             if (offset == 0) {
                 goto process_next_resolvent;            
             }
@@ -365,12 +404,14 @@ namespace sat {
             bool_var v = m_active_vars[i];
             slack += get_abs_coeff(v);
         }
+
+        TRACE("sat", display(tout, m_A););
         
         ++idx;
         alit = null_literal;
 #if 1
-        std::cout << c.size() << " >= " << c.k() << "\n";
-        std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n";
+        // std::cout << c.size() << " >= " << c.k() << "\n";
+        // std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n";
         while (0 <= slack) {            
             literal lit = lits[idx];
             bool_var v = lit.var();
@@ -432,7 +473,9 @@ namespace sat {
             return false;
         }
         SASSERT(slack < 0);
-        SASSERT(validate_conflict(m_conflict));
+        SASSERT(validate_conflict(m_conflict, m_A));
+
+        TRACE("sat", tout << m_conflict << "\n";);
 
         s().assign(alit, justification::mk_ext_justification(0));
         return true;
@@ -520,7 +563,7 @@ namespace sat {
 
     void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
         if (idx == 0) {
-            std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n";
+            // std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n";
             SASSERT(m_conflict.back() == l);
             for (unsigned i = 0; i + 1 < m_conflict.size(); ++i) {
                 SASSERT(value(m_conflict[i]) == l_false);
@@ -537,7 +580,7 @@ namespace sat {
                 }
                 SASSERT(found););
 
-            std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n";            
+            // std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n";            
             r.push_back(c.lit());
             SASSERT(value(c.lit()) == l_true);
             for (unsigned i = c.k(); i < c.size(); ++i) {
@@ -552,7 +595,7 @@ namespace sat {
         // literal is assigned to false.        
         unsigned sz = c.size();
         unsigned bound = c.k();
-        TRACE("sat", tout << "assign: " << c.lit() << " " << ~alit << " " << bound << "\n";);
+        TRACE("sat", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
 
         SASSERT(0 < bound && bound < sz);
         SASSERT(value(alit) == l_false);
@@ -583,11 +626,11 @@ namespace sat {
         // conflict
         if (bound != index && value(c[bound]) == l_false) {
             TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
-            set_conflict(c, alit);
+            set_conflict(c);
             return l_false;
         }
 
-        TRACE("sat", tout << "no swap " << index << " " << alit << "\n";);
+        // TRACE("sat", tout << "no swap " << index << " " << alit << "\n";);
         // there are no literals to swap with,
         // prepare for unit propagation by swapping the false literal into 
         // position bound. Then literals in positions 0..bound-1 have to be
@@ -609,8 +652,8 @@ namespace sat {
         if (v >= m_var_infos.size()) return;
         var_info& vinfo = m_var_infos[v];
         ptr_vector<card>* cards = vinfo.m_lit_watch[!l.sign()];
-        TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";);
-        TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";);
+        //TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";);
+        //TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";);
         if (cards != 0  && !cards->empty() && !s().inconsistent())  {
             ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
             for (; it != end; ++it) {
@@ -652,7 +695,7 @@ namespace sat {
     }
 
     void card_extension::pop(unsigned n) {        
-        TRACE("sat", tout << "pop:" << n << "\n";);
+        TRACE("sat_verbose", tout << "pop:" << n << "\n";);
         unsigned new_lim = m_var_lim.size() - n;
         unsigned sz = m_var_lim[new_lim];
         while (m_var_trail.size() > sz) {
@@ -690,9 +733,9 @@ namespace sat {
 
     void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
         watch const* w = m_var_infos[v].m_lit_watch[sign];
-        if (w) {
+        if (w && !w->empty()) {
             watch const& wl = *w;
-            out << "watch: " << literal(v, sign) << " |-> ";
+            out << literal(v, sign) << " |-> ";
             for (unsigned i = 0; i < wl.size(); ++i) {
                 out << wl[i]->lit() << " ";
             }
@@ -708,7 +751,7 @@ namespace sat {
     }
 
     void card_extension::display(std::ostream& out, card& c, bool values) const {
-        out << c.lit();
+        out << c.lit() << "[" << c.size() << "]";
         if (c.lit() != null_literal && values) {
             out << "@(" << value(c.lit());
             if (value(c.lit()) != l_undef) {
@@ -750,6 +793,21 @@ namespace sat {
         return out;
     }
 
+    std::ostream& card_extension::display_justification(std::ostream& out, ext_justification_idx idx) const {
+        if (idx == 0) {
+            out << "conflict: " << m_conflict;
+        }
+        else {
+            card& c = *m_constraints[idx];
+            out << "bound " << c.lit() << ": ";
+            for (unsigned i = c.k(); i < c.size(); ++i) {
+                out << c[i] << " ";
+            }
+            out << ">= " << c.k();
+        }
+        return out;
+    }
+
     void card_extension::collect_statistics(statistics& st) const {
         st.update("cardinality propagations", m_stats.m_num_propagations);
         st.update("cardinality conflicts", m_stats.m_num_conflicts);
@@ -842,7 +900,6 @@ namespace sat {
     // validate that m_A & m_B implies m_C
 
     bool card_extension::validate_resolvent() {
-        std::cout << "validate resolvent\n";
         u_map<unsigned> coeffs;
         unsigned k = m_A.m_k + m_B.m_k;
         for (unsigned i = 0; i < m_A.m_lits.size(); ++i) {
@@ -899,11 +956,18 @@ namespace sat {
         return true;
     }
 
-    bool card_extension::validate_conflict(literal_vector const& lits) { 
+    bool card_extension::validate_conflict(literal_vector const& lits, ineq& p) { 
         for (unsigned i = 0; i < lits.size(); ++i) {
             if (value(lits[i]) != l_false) return false;
         }
-        return true; 
+        unsigned value = 0;
+        for (unsigned i = 0; i < p.m_lits.size(); ++i) {
+            unsigned coeff = p.m_coeffs[i];
+            if (!lits.contains(p.m_lits[i])) {
+                value += coeff;
+            }
+        }
+        return value < p.m_k;
     }
 
     
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index 947f6e5d3..ac434ef5c 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -103,7 +103,8 @@ namespace sat {
         void assign(card& c, literal lit);
         lbool add_assign(card& c, literal lit);
         void watch_literal(card& c, literal lit);
-        void set_conflict(card& c, literal lit);
+        void set_conflict(card& c);
+        literal last_false_literal(card& c);
         void clear_watch(card& c);
         void reset_coeffs();
 
@@ -131,7 +132,7 @@ namespace sat {
         bool validate_assign(literal_vector const& lits, literal lit);
         bool validate_lemma();
         bool validate_unit_propagation(card const& c);
-        bool validate_conflict(literal_vector const& lits);
+        bool validate_conflict(literal_vector const& lits, ineq& p);
 
         ineq m_A, m_B, m_C;
         void active2pb(ineq& p);
@@ -156,6 +157,7 @@ namespace sat {
         virtual void clauses_modifed();
         virtual lbool get_phase(bool_var v);
         virtual std::ostream& display(std::ostream& out) const;
+        virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const;
         virtual void collect_statistics(statistics& st) const;
         virtual extension* copy(solver* s);
     };
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 9206ea8bc..3e132c738 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -113,6 +113,7 @@ namespace sat {
         m_minimize_lemmas = p.minimize_lemmas();
         m_core_minimize   = p.core_minimize();
         m_core_minimize_partial   = p.core_minimize_partial();
+        m_drat            = p.drat();
         m_dyn_sub_res     = p.dyn_sub_res();
     }
 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 405cbd092..34983f451 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -73,7 +73,7 @@ namespace sat {
         bool               m_dyn_sub_res;
         bool               m_core_minimize;
         bool               m_core_minimize_partial;
-
+        bool               m_drat;
 
         symbol             m_always_true;
         symbol             m_always_false;
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
new file mode 100644
index 000000000..7e30c18ff
--- /dev/null
+++ b/src/sat/sat_drat.cpp
@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_drat.cpp
+
+Abstract:
+   
+    Produce DRAT proofs.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-2-3
+
+Notes:
+
+--*/
+#include "sat_solver.h"
+#include "sat_drat.h"
+
+
+namespace sat {
+    drat::drat(solver& s):
+        s(s),
+        m_out(0)
+    {
+        if (s.m_config.m_drat) {
+            m_out = alloc(std::ofstream, "proof.drat");
+        }
+    }
+
+    drat::~drat() {
+        dealloc(m_out);
+    }
+    void drat::add_empty() {
+        (*m_out) << "0\n";
+    }
+    void drat::add_literal(literal l) {
+        (*m_out) << l << " 0\n";
+    }
+    void drat::add_binary(literal l1, literal l2) {
+        (*m_out) << l1 << " " << l2 << " 0\n";
+    }
+    void drat::add_ternary(literal l1, literal l2, literal l3) {
+        (*m_out) << l1 << " " << l2 << " " << l3 << " 0\n";
+    }
+    void drat::add_clause(clause& c) {
+        unsigned sz = c.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            (*m_out) << c[i] << " ";
+        }
+        (*m_out) << "0\n";
+    }
+    void drat::del_literal(literal l) {
+        (*m_out) << "d ";
+        add_literal(l);
+    }
+    void drat::del_binary(literal l1, literal l2) {
+        (*m_out) << "d ";
+        add_binary(l1, l2);
+    }
+    void drat::del_clause(clause& c) {
+        (*m_out) << "d ";
+        add_clause(c);
+    }
+}
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
new file mode 100644
index 000000000..9d34c57b4
--- /dev/null
+++ b/src/sat/sat_drat.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    sat_drat.h
+
+Abstract:
+   
+    Produce DRAT proofs.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-2-3
+
+Notes:
+
+--*/
+#ifndef SAT_DRAT_H_
+#define SAT_DRAT_H_
+
+namespace sat {
+    class drat {
+        solver& s;
+        std::ostream* m_out;
+    public:
+        drat(solver& s);
+        ~drat();  
+        void add_empty();
+        void add_literal(literal l);
+        void add_binary(literal l1, literal l2);
+        void add_ternary(literal l1, literal l2, literal l3);
+        void add_clause(clause& c);
+        void del_literal(literal l);
+        void del_binary(literal l1, literal l2);
+        void del_clause(clause& c);
+    };
+
+};
+
+#endif
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index c065e132e..e8d92d085 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -43,6 +43,7 @@ namespace sat {
         virtual void clauses_modifed() = 0;
         virtual lbool get_phase(bool_var v) = 0;
         virtual std::ostream& display(std::ostream& out) const = 0;
+        virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
         virtual void collect_statistics(statistics& st) const = 0;
         virtual extension* copy(solver* s) = 0;
     };
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 940fa8c45..feefe653f 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -24,4 +24,5 @@ def_module_params('sat',
                           ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('parallel_threads', UINT, 1, 'number of parallel threads to use'),
                           ('cardinality_solver', BOOL, False, 'enable cardinality based solver'),
-                          ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
+                          ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
+                          ('drat', BOOL, False, 'produce DRAT proofs'),))
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 6eafd8906..54122c019 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -42,6 +42,7 @@ namespace sat {
         m_asymm_branch(*this, p),
         m_probing(*this, p),
         m_mus(*this),
+        m_drat(*this),
         m_inconsistent(false),
         m_num_frozen(0),
         m_activity_inc(128),
@@ -199,7 +200,11 @@ namespace sat {
     }
 
     void solver::del_clause(clause& c) {
-        if (!c.is_learned()) m_stats.m_non_learned_generation++;
+        if (!c.is_learned()) {
+            m_stats.m_non_learned_generation++;
+        } else if (m_config.m_drat) {
+            m_drat.del_clause(c);
+        }
         m_cls_allocator.del_clause(&c);
         m_stats.m_del_clause++;
     }
@@ -214,9 +219,10 @@ namespace sat {
             }
             ++m_stats.m_non_learned_generation;
         }
-
+        
         switch (num_lits) {
         case 0:
+            if (m_config.m_drat) m_drat.add_empty();
             set_conflict(justification());
             return 0;
         case 1:
@@ -233,6 +239,8 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
+        if (learned && m_config.m_drat) 
+            m_drat.add_binary(l1, l2);
         if (propagate_bin_clause(l1, l2)) {
             if (at_base_lvl())
                 return;
@@ -266,6 +274,8 @@ namespace sat {
 
 
     clause * solver::mk_ter_clause(literal * lits, bool learned) {
+        if (learned && m_config.m_drat) 
+            m_drat.add_ternary(lits[0], lits[1], lits[2]);
         m_stats.m_mk_ter_clause++;
         clause * r = m_cls_allocator.mk_clause(3, lits, learned);
         bool reinit = attach_ter_clause(*r);
@@ -309,8 +319,10 @@ namespace sat {
         SASSERT(!learned || r->is_learned());
         bool reinit = attach_nary_clause(*r);
         if (reinit && !learned) push_reinit_stack(*r);
-        if (learned)
+        if (learned) {
             m_learned.push_back(r);
+            if (m_config.m_drat) m_drat.add_clause(*r);
+        }
         else
             m_clauses.push_back(r);
         return r;
@@ -516,8 +528,10 @@ namespace sat {
     void solver::assign_core(literal l, justification j) {
         SASSERT(value(l) == l_undef);
         TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
-        if (at_base_lvl())
+        if (at_base_lvl()) {
             j = justification(); // erase justification for level 0
+            if (m_config.m_drat) m_drat.add_literal(l);
+        }
         m_assignment[l.index()]    = l_true;
         m_assignment[(~l).index()] = l_false;
         bool_var v = l.var();
@@ -2058,6 +2072,10 @@ namespace sat {
             }
             consequent = ~m_not_l;
         }
+        std::cout << "CONFLICT: " << m_core << "\n";
+        display_status(std::cout);
+        ++count;
+        exit(0);
 
         justification js   = m_conflict;
 
@@ -2098,8 +2116,6 @@ namespace sat {
             IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
         }
 
-        ++count;
-        SASSERT(count == 1);
     }
 
 
@@ -2124,7 +2140,7 @@ namespace sat {
             for (; it != end; ++it)
                 r = std::max(r, lvl(*it));
             if (true || r != scope_lvl() || r != lvl(not_l)) {
-                std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n";
+                // std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n";
             }
             return r;
         }
@@ -2862,12 +2878,14 @@ namespace sat {
     }
 
     void solver::display_units(std::ostream & out) const {
-        unsigned end = init_trail_size();
+        unsigned end = m_trail.size(); // init_trail_size();
         for (unsigned i = 0; i < end; i++) {
             out << m_trail[i] << " ";
-        }
-        if (end != 0)
+            display_justification(out, m_justification[m_trail[i].var()]);
             out << "\n";
+        }
+        //if (end != 0)
+        //    out << "\n";
     }
 
     void solver::display(std::ostream & out) const {
@@ -2886,6 +2904,9 @@ namespace sat {
         if (js.is_clause()) {
             out << *(m_cls_allocator.get_clause(js.get_clause_offset()));
         }
+        else if (js.is_ext_justification() && m_ext) {
+            m_ext->display_justification(out << " ", js.get_ext_justification_idx());
+        }
     }
 
     unsigned solver::num_clauses() const {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 3702047d1..2ab9d5c50 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -33,6 +33,7 @@ Revision History:
 #include"sat_iff3_finder.h"
 #include"sat_probing.h"
 #include"sat_mus.h"
+#include"sat_drat.h"
 #include"sat_par.h"
 #include"params.h"
 #include"statistics.h"
@@ -87,6 +88,7 @@ namespace sat {
         asymm_branch            m_asymm_branch;
         probing                 m_probing;
         mus                     m_mus;           // MUS for minimal core extraction
+        drat                    m_drat;          // DRAT for generating proofs
         bool                    m_inconsistent;
         // A conflict is usually a single justification. That is, a justification
         // for false. If m_not_l is not null_literal, then m_conflict is a
@@ -146,6 +148,7 @@ namespace sat {
         friend class probing;
         friend class iff3_finder;
         friend class mus;
+        friend class drat;
         friend class card_extension;
         friend struct mk_stat;
     public:
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 69e624337..7715c4b5d 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -208,7 +208,7 @@ public:
     }
     virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr(expr * t) {
-        TRACE("sat", tout << mk_pp(t, m) << "\n";);
+        TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
     virtual void set_produce_models(bool f) {}
@@ -376,7 +376,7 @@ private:
         init_preprocess();
         SASSERT(g->models_enabled());
         SASSERT(!g->proofs_enabled());
-        TRACE("sat", g->display(tout););
+        TRACE("goal2sat", g->display(tout););
         try {
             (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
         }
@@ -393,7 +393,7 @@ private:
         }
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
-        TRACE("sat", g->display_with_dependencies(tout););
+        TRACE("goal2sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index eb90edd3d..923006da2 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -400,7 +400,7 @@ struct goal2sat::imp {
         sat::bool_var v = m_solver.mk_var(true);
         sat::literal lit(v, sign);
         m_ext->add_at_least(v, lits, k.get_unsigned());
-        TRACE("sat", tout << "root: " << root << " lit: " << lit << "\n";);
+        TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
         if (root) {
             m_result_stack.reset();
             mk_clause(lit);
@@ -616,7 +616,7 @@ struct goal2sat::imp {
                 }                
                 f = m.mk_or(fmls.size(), fmls.c_ptr());
             }
-            TRACE("sat", tout << mk_pp(f, m) << "\n";);
+            TRACE("goal2sat", tout << mk_pp(f, m) << "\n";);
             process(f);
         skip_dep:
             ;