From ec39d84f575e1f40172020e5ad1d3dd34b788213 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Dec 2019 20:19:59 -0800
Subject: [PATCH] remove empty clause feature

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp      | 5 +----
 src/smt/smt_context.h        | 1 -
 src/smt/smt_internalizer.cpp | 1 -
 3 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 3e3a5a910..27a6011b5 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -75,7 +75,6 @@ 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),
@@ -2396,11 +2395,9 @@ namespace smt {
                     m_unsat_proof = nullptr;
                 }
                 m_base_scopes.shrink(new_lvl);
-                m_empty_clause = false;
             }
             else {
-                m_conflict = m_empty_clause ? b_justification::mk_axiom() : null_b_justification;
-                // m_conflict = 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_context.h b/src/smt/smt_context.h
index ace0eaed0..0b78bc887 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -193,7 +193,6 @@ namespace smt {
         // 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 80dcb9f1d..efca6c042 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1351,7 +1351,6 @@ 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 = (j == nullptr);
             SASSERT(inconsistent());
             return nullptr;
         case 1: