diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 27a6011b5..d7bde6e23 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -75,6 +75,7 @@ namespace smt {
         m_phase_default(false),
         m_conflict(null_b_justification),
         m_not_l(null_literal),
+        m_empty_clause(false),
         m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
         m_unsat_proof(m),
         m_dyn_ack_manager(*this, p),
@@ -2395,9 +2396,10 @@ namespace smt {
                     m_unsat_proof = nullptr;
                 }
                 m_base_scopes.shrink(new_lvl);
+                m_empty_clause = false;
             }
             else {
-                m_conflict = null_b_justification;
+                m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
                 m_not_l = null_literal;
             }
             del_clauses(m_aux_clauses, s.m_aux_clauses_lim);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d3735f199..ace0eaed0 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -188,9 +188,12 @@ namespace smt {
 
         // 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
-        // justification for l, and the conflict is union of m_no_l and m_conflict;
+        // justification for l, and the conflict is union of m_not_l and m_conflict;
+        // m_empty_clause is set to ensure that an empty clause generated in deep scope 
+        // levels survives to the base level.
         b_justification             m_conflict;
         literal                     m_not_l;
+        bool                        m_empty_clause;
         scoped_ptr<conflict_resolution> m_conflict_resolution;
         proof_ref                   m_unsat_proof;
 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index efca6c042..b12bcc2ee 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1351,6 +1351,7 @@ namespace smt {
                 m_justifications.push_back(j);
             TRACE("mk_clause", tout << "empty clause... setting conflict\n";);
             set_conflict(j == nullptr ? b_justification::mk_axiom() : b_justification(j));
+            m_empty_clause = true;
             SASSERT(inconsistent());
             return nullptr;
         case 1: