diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 259f8e730..444274270 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -3353,7 +3353,6 @@ proof * ast_manager::mk_redundant_del(expr* e) {
 proof * ast_manager::mk_clause_trail(unsigned n, proof* const* ps) {    
     ptr_buffer<expr> args;
     args.append(n, (expr**) ps);
-    args.push_back(mk_false());
     return mk_app(m_basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.c_ptr());
 }
 
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 7dc4d1310..188cf5528 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -114,7 +114,7 @@ namespace smt {
         }
     }
 
-    proof_ref clause_proof::get_proof() {
+    proof_ref clause_proof::get_proof(bool inconsistent) {
         TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";);
         if (!ctx.get_fparams().m_clause_proof) {
             return proof_ref(m);
@@ -141,8 +141,8 @@ namespace smt {
                 break;
             }
         }
-        proof_ref result(m.mk_clause_trail(ps.size(), ps.c_ptr()), m);
-        return result;
+        ps.push_back(m.mk_bool_val(!inconsistent));
+        return proof_ref(m.mk_clause_trail(ps.size(), ps.c_ptr()), m);
     }
 
     std::ostream& operator<<(std::ostream& out, clause_proof::status st) {
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index 972b19bd0..289d4d1fe 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -67,7 +67,7 @@ namespace smt {
         void add(clause& c);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
         void del(clause& c);
-        proof_ref get_proof();
+        proof_ref get_proof(bool inconsistent);
     };
 
     std::ostream& operator<<(std::ostream& out, clause_proof::status st);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ebf5da767..40c993248 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4173,7 +4173,7 @@ namespace smt {
             return true;
         }
         else if (m_fparams.m_clause_proof && !m.proofs_enabled()) {
-            m_unsat_proof = m_clause_proof.get_proof();
+            m_unsat_proof = m_clause_proof.get_proof(inconsistent());
         }
         else if (m.proofs_enabled()) {
             m_unsat_proof = m_conflict_resolution->get_lemma_proof();
@@ -4500,7 +4500,7 @@ namespace smt {
 
     proof * context::get_proof() {        
         if (!m_unsat_proof) {
-            m_unsat_proof = m_clause_proof.get_proof();
+            m_unsat_proof = m_clause_proof.get_proof(inconsistent());
         }
         TRACE("context", tout << m_unsat_proof << "\n";);
         return m_unsat_proof;
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 116e1f793..855023f18 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -208,7 +208,7 @@ public:
             }
             SASSERT(m_ctx);
             m_ctx->collect_statistics(m_stats);
-            proof * pr = m_ctx->get_proof();
+            proof_ref pr(m_ctx->get_proof(), m);
             TRACE("smt_tactic", tout << r << " " << pr << "\n";);
             switch (r) {
             case l_true: {
@@ -267,7 +267,7 @@ public:
                 result.push_back(in.get());
                 if (pr) {
                     in->reset();
-                    in->assert_expr(m.mk_const(symbol("trail"), m.mk_bool_sort()), pr, nullptr);
+                    in->assert_expr(m.get_fact(pr), pr, nullptr);
                 }
                 if (m_candidate_models) {
                     switch (m_ctx->last_failure()) {