diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index cb28f87f8..582bcc664 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -304,7 +304,7 @@ namespace smt {
             }
             m_instances.push_back(pr1);
         }
-        else if (m_context.on_clause_active()) {
+        else if (m_context.clause_proof_active()) {
             expr_ref_vector bindings_e(m), args(m);
             arith_util a(m);
             expr_ref gen(a.mk_int(generation), m);
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index ad3d3818c..096a0994f 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -18,7 +18,17 @@ Revision History:
 #include "ast/ast_ll_pp.h"
 
 namespace smt {
-    clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {}
+    
+    clause_proof::clause_proof(context& ctx):
+        ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) {
+        auto proof_log = ctx.get_fparams().m_proof_log;
+        m_enabled = ctx.get_fparams().m_clause_proof || proof_log.is_non_empty_string();
+        if (proof_log.is_non_empty_string()) {
+            m_pp_out = alloc(std::ofstream, proof_log.str());
+            if (!*m_pp_out)
+                throw default_exception(std::string("Could not open file ") + proof_log.str());
+        }
+    }
 
     clause_proof::status clause_proof::kind2st(clause_kind k) {
         switch (k) {
@@ -42,7 +52,7 @@ namespace smt {
             r = j->mk_proof(ctx.get_cr());
         if (r) 
             return r;
-        if (!m_on_clause_active)
+        if (!is_enabled())
             return nullptr;
         switch (st) {
         case status::assumption:
@@ -60,7 +70,7 @@ namespace smt {
     }
 
     void clause_proof::add(clause& c) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         justification* j = c.get_justification();
         auto st = kind2st(c.get_kind());
@@ -70,7 +80,7 @@ namespace smt {
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         auto st = kind2st(k);
         proof_ref pr(justification2proof(st, j), m);
@@ -83,7 +93,7 @@ namespace smt {
 
 
     void clause_proof::shrink(clause& c, unsigned new_size) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         m_lits.reset();
         for (unsigned i = 0; i < new_size; ++i) 
@@ -97,7 +107,7 @@ namespace smt {
     }
 
     void clause_proof::add(literal lit, clause_kind k, justification* j) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit));
@@ -107,7 +117,7 @@ namespace smt {
     }
 
     void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit1));
@@ -117,21 +127,75 @@ namespace smt {
         update(st, m_lits, pr);
     }
 
+    void clause_proof::propagate(literal lit, justification const& jst, literal_vector const& ante) {
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        for (literal l : ante)
+            m_lits.push_back(ctx.literal2expr(~l));
+        m_lits.push_back(ctx.literal2expr(lit));
+        proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
+        update(clause_proof::status::th_lemma, m_lits, pr);
+    }
 
     void clause_proof::del(clause& c) {
         update(c, status::deleted, justification2proof(status::deleted, nullptr));
     }
 
+    std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
+        for (expr* e : v)
+            if (m.is_not(e, e))                
+                m_pp.display_expr_def(out << " (not ", e) << ")";
+            else
+                m_pp.display_expr_def(out << " ", e);
+        return out;
+    }
+
+    std::ostream& clause_proof::display_hint(std::ostream& out, proof* p) {
+        if (p)
+            m_pp.display_expr_def(out << " ", p);
+        return out;
+    }
+
+    void clause_proof::declare(std::ostream& out, expr* e) {
+        m_pp.collect(e);
+        m_pp.display_decls(out);
+        m.is_not(e, e);
+        m_pp.define_expr(out, e);
+    }
+
     void clause_proof::update(status st, expr_ref_vector& v, proof* p) {
         TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";);
         if (ctx.get_fparams().m_clause_proof)
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
             m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data());        
+        if (m_pp_out) {
+            auto& out = *m_pp_out;
+            for (auto* e : v)
+                declare(out, e);
+            switch (st) {
+            case clause_proof::status::assumption:
+                display_literals(out << "(assume", v) << ")\n";
+                break;
+            case clause_proof::status::lemma:
+            case clause_proof::status::th_lemma:
+            case clause_proof::status::th_assumption:
+                if (p)
+                    declare(out, p);
+                display_hint(display_literals(out << "(infer", v), p) << ")\n";
+                break;
+            case clause_proof::status::deleted:
+                display_literals(out << "(del", v) << ")\n";
+                break;
+            default:
+                UNREACHABLE();
+            }
+        }
     }
 
     void clause_proof::update(clause& c, status st, proof* p) {
-        if (!ctx.get_fparams().m_clause_proof && !m_on_clause_active) 
+        if (!is_enabled())
             return;
         m_lits.reset();
         for (literal lit : c) 
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index f15d0ffe0..42f283f1d 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -26,8 +26,10 @@ Revision History:
 --*/
 #pragma once
 
+#include "ast/ast_pp_util.h"
 #include "smt/smt_theory.h"
 #include "smt/smt_clause.h"
+#include "smt/smt_justification.h"
 #include "tactic/user_propagator_base.h"
 
 namespace smt {
@@ -55,13 +57,20 @@ namespace smt {
         ast_manager&    m;
         expr_ref_vector m_lits;
         vector<info>    m_trail;
-        bool            m_on_clause_active = false;
+        bool            m_enabled = false;
         user_propagator::on_clause_eh_t m_on_clause_eh;
         void*                           m_on_clause_ctx = nullptr;
+        ast_pp_util                     m_pp;
+        scoped_ptr<std::ofstream>       m_pp_out;
+        
         void update(status st, expr_ref_vector& v, proof* p);
         void update(clause& c, status st, proof* p);
         status kind2st(clause_kind k);
         proof* justification2proof(status st, justification* j);
+        void log(status st, proof* p);
+        void declare(std::ostream& out, expr* e);
+        std::ostream& display_literals(std::ostream& out, expr_ref_vector const& v);
+        std::ostream& display_hint(std::ostream& out, proof* p);
     public:
         clause_proof(context& ctx);
         void shrink(clause& c, unsigned new_size);
@@ -69,13 +78,14 @@ namespace smt {
         void add(literal lit1, literal lit2, clause_kind k, justification* j);
         void add(clause& c);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
+        void propagate(literal lit, justification const& j, literal_vector const& ante);
         void del(clause& c);
         proof_ref get_proof(bool inconsistent);
-        bool on_clause_active() const { return m_on_clause_active; }
+        bool is_enabled() const { return m_enabled; }
         void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) {
             m_on_clause_eh = on_clause;
             m_on_clause_ctx = ctx;
-            m_on_clause_active = !!m_on_clause_eh;
+            m_enabled |= !!m_on_clause_eh;
         }
     };
 
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 45ff1900d..d075c0652 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -350,6 +350,7 @@ namespace smt {
         literal_vector & antecedents = m_tmp_literal_vector;
         antecedents.reset();
         justification2literals_core(js, antecedents);
+        m_ctx.get_clause_proof().propagate(consequent, *js, antecedents);
         for (literal l : antecedents)
             process_antecedent(l, num_marks);
         (void)consequent;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 84b4906ca..a8d2f268d 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -284,7 +284,7 @@ namespace smt {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
               display_literal_smt2(tout, l) << "\n";
               tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
-              /*display(tout, j);*/
+              display(tout, j);
               );
         TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
 
@@ -639,7 +639,6 @@ namespace smt {
                     if (val != l_true) {
                         if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE)
                             m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr());
-
                         assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
                     }
                     // It is not necessary to reinsert the equality to the congruence table
@@ -1347,6 +1346,7 @@ namespace smt {
                     TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v)););
                     if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
                         literal n_eq = literal(l.var(), true);
+                        IF_VERBOSE(0, verbose_stream() << "eq-conflict @" << m_scope_lvl << "\n");
                         set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq);
                     }
                 }
@@ -3732,6 +3732,7 @@ namespace smt {
         flet<bool> l(m_searching, true);
         TRACE("after_init_search", display(tout););
         IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);
+        log_stats();
         TRACE("search_lite", tout << "searching...\n";);
         lbool    status            = l_undef;
         unsigned curr_lvl          = m_scope_lvl;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 4a5f64926..2b3a343f7 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1706,7 +1706,9 @@ namespace smt {
 
         void get_units(expr_ref_vector& result);
 
-        bool on_clause_active() const { return m_clause_proof.on_clause_active(); }
+        bool clause_proof_active() const { return m_clause_proof.is_enabled(); }
+
+        clause_proof& get_clause_proof() { return m_clause_proof; }
 
         void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) {
             m_clause_proof.register_on_clause(ctx, on_clause);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 63848418f..26e23d92d 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1593,7 +1593,7 @@ namespace smt {
             TRACE("gate_clause", tout << mk_ll_pp(pr, m););
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
-        else if (m_clause_proof.on_clause_active()) {
+        else if (clause_proof_active()) {
             ptr_buffer<expr> new_lits;
             for (unsigned i = 0; i < num_lits; i++) {
                 literal l      = lits[i];
@@ -1638,7 +1638,7 @@ namespace smt {
             }
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
-        else if (pr && on_clause_active()) 
+        else if (pr && clause_proof_active()) 
             // support logging of quantifier instantiations and other more detailed information
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         else