diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index f5ce6c73a..6b59bd61f 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -15,6 +15,7 @@ Revision History:
 #include "smt/smt_clause_proof.h"
 #include "smt/smt_context.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 
 namespace smt {
     clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {}
@@ -42,18 +43,19 @@ namespace smt {
     void clause_proof::add(clause& c) {
         if (ctx.get_fparams().m_clause_proof) {  
             justification* j = c.get_justification();
-            proof* pr = justification2proof(j);
+            proof_ref pr(justification2proof(j), m);
+            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
             update(c, kind2st(c.get_kind()), pr);
         }
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
-        if (ctx.get_fparams().m_clause_proof) {  
-            proof* pr = justification2proof(j);
+        if (ctx.get_fparams().m_clause_proof) {              
+            proof_ref pr(justification2proof(j), m);
+            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
             m_lits.reset();
             for (unsigned i = 0; i < n; ++i) {
-                literal lit = lits[i];
-                m_lits.push_back(ctx.literal2expr(lit));
+                m_lits.push_back(ctx.literal2expr(lits[i]));
             }
             update(kind2st(k), m_lits, pr);
         }
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 6723d26a8..8d2279824 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1043,7 +1043,7 @@ namespace smt {
     */
     proof * conflict_resolution::get_proof(justification * js) {
         proof * pr;
-        if (m_js2proof.find(js, pr)) {
+        if (false && m_js2proof.find(js, pr)) {
             TRACE("proof_gen_bug", tout << "js2pr_cached: #" << js << "\n";);
             return pr;
         }
@@ -1313,10 +1313,9 @@ namespace smt {
         }
         else {
             proof * prs[2] = { nullptr, nullptr};
-            m_lit2proof.find(not_l, prs[0]);
-            SASSERT(prs[0]);
-            prs[1]         = get_proof(consequent, conflict);
-            SASSERT(prs[1]);
+            prs[0] = m_lit2proof.find(not_l);
+            prs[1] = get_proof(consequent, conflict);
+            SASSERT(prs[0] && prs[1]);
             pr = m_manager.mk_unit_resolution(2, prs);
         }
         expr_ref_buffer lits(m_manager);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index cf77877a2..d2a06361e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3135,6 +3135,7 @@ namespace smt {
                 }
                 expr * f   = m_asserted_formulas.get_formula(qhead);
                 proof * pr = m_asserted_formulas.get_formula_proof(qhead);
+                SASSERT(!pr || f == m.get_fact(pr));
                 internalize_assertion(f, pr, 0);
                 qhead++;
             }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 9536c7f40..ffa900062 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1079,6 +1079,7 @@ namespace smt {
        clauses because they are deleted during backtracking.
     */
     bool context::simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits) {
+        TRACE("simplify_aux_clause_literals", display_literals(tout, num_lits, lits); tout << "\n";);
         std::sort(lits, lits + num_lits);
         literal prev = null_literal;
         unsigned j = 0;
@@ -1087,7 +1088,7 @@ namespace smt {
             lbool   val  = get_assignment(curr);
             switch(val) {
             case l_false:
-                TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; );
+                TRACE("simplify_aux_clause_literals", display_literal_verbose(tout << get_assign_level(curr) << " " << get_scope_level() << " " << curr << ":", curr); tout << "\n"; );
                 simp_lits.push_back(~curr);
                 break; // ignore literal                
                 // fall through
@@ -1131,9 +1132,9 @@ namespace smt {
        kind of simplification.
     */
     bool context::simplify_aux_lemma_literals(unsigned & num_lits, literal * lits) {
-        TRACE("simplify_aux_lemma_literals", tout << "1) "; display_literals(tout, num_lits, lits); tout << "\n";);
+        TRACE("simplify_aux_lemma_literals", display_literals(tout << "1) ", num_lits, lits) << "\n";);
         std::sort(lits, lits + num_lits);
-        TRACE("simplify_aux_lemma_literals", tout << "2) "; display_literals(tout, num_lits, lits); tout << "\n";);
+        TRACE("simplify_aux_lemma_literals", display_literals(tout << "2) ", num_lits, lits) << "\n";);
         literal prev = null_literal;
         unsigned i = 0;
         unsigned j = 0;
@@ -1155,7 +1156,7 @@ namespace smt {
             }
         }
         num_lits = j;
-        TRACE("simplify_aux_lemma_literals", tout << "3) "; display_literals(tout, num_lits, lits); tout << "\n";);
+        TRACE("simplify_aux_lemma_literals", display_literals(tout << "3) ", num_lits, lits) << "\n";);
         return true;
     }
     
@@ -1338,7 +1339,7 @@ namespace smt {
             }
             break;
         }
-        case CLS_TH_LEMMA: {
+        case CLS_TH_LEMMA: 
             if (!simplify_aux_lemma_literals(num_lits, lits)) {
                 if (j && !j->in_region()) {
                     j->del_eh(m);
@@ -1348,16 +1349,13 @@ namespace smt {
             }
             // simplify_aux_lemma_literals does not delete literals assigned to false, so
             // it is not necessary to create a unit_resolution_justification
-            break;
-        }
+            break;        
         default:
             break;
         }
-        TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
+        TRACE("mk_clause", display_literals_verbose(tout << "after simplification:\n", num_lits, lits) << "\n";);
 
-        unsigned activity = 0;
-        if (activity == 0)
-            activity = 1;
+        unsigned activity = 1;
         bool  lemma = is_lemma(k);
         m_stats.m_num_mk_lits += num_lits;
         switch (num_lits) {
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index 65f4c4a12..6d1d93879 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -32,6 +32,7 @@ namespace smt {
 
     void justification_proof_wrapper::del_eh(ast_manager & m) {
         m.dec_ref(m_proof);
+        m_proof = nullptr;
     }
     
     proof * justification_proof_wrapper::mk_proof(conflict_resolution & cr) {
@@ -47,11 +48,7 @@ namespace smt {
         SASSERT(!js || js->in_region());
         m_literals = new (r) literal[num_lits];
         memcpy(m_literals, lits, sizeof(literal) * num_lits);
-        TRACE("unit_resolution_justification_bug",
-              for (unsigned i = 0; i < num_lits; i++) {
-                  tout << lits[i] << " ";
-              }
-              tout << "\n";);
+        TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
         SASSERT(m_num_literals > 0);
     }
 
@@ -64,11 +61,7 @@ namespace smt {
         SASSERT(!js || !js->in_region());
         m_literals = alloc_vect<literal>(num_lits);
         memcpy(m_literals, lits, sizeof(literal) * num_lits);
-        TRACE("unit_resolution_justification_bug",
-              for (unsigned i = 0; i < num_lits; i++) {
-                  tout << lits[i] << " ";
-              }
-              tout << "\n";);
+        TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
         SASSERT(num_lits != 0);
     }
 
@@ -88,29 +81,23 @@ namespace smt {
 
     proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) {
         SASSERT(m_antecedent);
-        ptr_buffer<proof> prs;
-        proof * pr   = cr.get_proof(m_antecedent);
-        bool visited = pr != nullptr;
+        ast_manager& m = cr.get_manager();
+        proof_ref_vector prs(m);
+        cr.init_mk_proof();
+        proof * pr = cr.get_proof(m_antecedent);
+        if (!pr)
+            return pr;
         prs.push_back(pr);
         for (unsigned i = 0; i < m_num_literals; i++) {
             proof * pr = cr.get_proof(m_literals[i]);
-            if (pr == nullptr)
-                visited = false;
+            if (!pr)
+                return pr;
             else
                 prs.push_back(pr);
         }
-        if (!visited)
-            return nullptr;
-        ast_manager & m = cr.get_manager();
         TRACE("unit_resolution_justification_bug",
-              tout << "in mk_proof\n";
-              for (unsigned i = 0; i < m_num_literals; i++) {
-                  tout << m_literals[i] << " ";
-              }
-              tout << "\n";
-              for (unsigned i = 0; i < prs.size(); i++) {
-                  tout << mk_ll_pp(m.get_fact(prs[i]), m);
-              });
+            tout << "in mk_proof\n" << literal_vector(m_num_literals, m_literals) << "\n";
+            for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m););
         return m.mk_unit_resolution(prs.size(), prs.c_ptr());
     }