diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index d9219fcb6..cf77877a2 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2950,7 +2950,7 @@ namespace smt {
     void context::assert_expr_core(expr * e, proof * pr) {
         if (get_cancel_flag()) return;
         SASSERT(is_well_sorted(m, e));
-        TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m) << "\n";);
+        TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
         TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
         pop_to_base_lvl();
         if (pr == nullptr)
@@ -3141,20 +3141,24 @@ namespace smt {
             m_asserted_formulas.commit();
         }
         if (m_asserted_formulas.inconsistent() && !inconsistent()) {
-            proof * pr = m_asserted_formulas.get_inconsistency_proof();
-            if (pr == nullptr) {
-                set_conflict(b_justification::mk_axiom());
-            }
-            else {
-                set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
-                m_unsat_proof = pr;
-            }
+            asserted_inconsistent();
         }
         TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
               tout << "inconsistent: " << inconsistent() << "\n";);
         TRACE("after_internalize_assertions", display(tout););
     }
 
+    void context::asserted_inconsistent() {
+        proof * pr = m_asserted_formulas.get_inconsistency_proof();
+        m_unsat_proof = pr;
+        if (!pr) {
+            set_conflict(b_justification::mk_axiom());
+        }
+        else {
+            set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
+        }
+    }
+
     /**
        \brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
     */
@@ -3626,8 +3630,10 @@ namespace smt {
 
 
     lbool context::search() {
-        if (m_asserted_formulas.inconsistent()) 
+        if (m_asserted_formulas.inconsistent()) {
+            asserted_inconsistent();
             return l_false;
+        }
         if (inconsistent()) {
             VERIFY(!resolve_conflict());
             return l_false;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index b52590c90..b790b6f9e 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1138,6 +1138,8 @@ namespace smt {
 
         void internalize_assertions();
 
+        void asserted_inconsistent();
+
         bool validate_assumptions(expr_ref_vector const& asms);
 
         void init_assumptions(expr_ref_vector const& asms);
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 855023f18..9b0f8d617 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -249,6 +249,7 @@ public:
                         lcore = m.mk_join(lcore, m.mk_leaf(d));
                     }
                 }
+                if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
                 in->assert_expr(m.mk_false(), pr, lcore);
                 result.push_back(in.get());
                 return;