diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c98c26485..3e3a5a910 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2399,8 +2399,8 @@ namespace smt {
                 m_empty_clause = false;
             }
             else {
-                // m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
-                m_conflict = null_b_justification;
+                m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
+                // m_conflict = null_b_justification;
                 m_not_l = null_literal;
             }
             del_clauses(m_aux_clauses, s.m_aux_clauses_lim);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index b12bcc2ee..80dcb9f1d 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1351,7 +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;
+            m_empty_clause = (j == nullptr);
             SASSERT(inconsistent());
             return nullptr;
         case 1: