From 5cecd986e2a4e70d3119c29442394f3db945df16 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Dec 2019 11:10:37 +0300
Subject: [PATCH] track empty clause during pop

If a theory solver creates the empty clause it gets dropped during pop.
By maintaining a variable m_empty_clause, the solver ensures that it retains the information that the search state is inconsistent.
---
 src/smt/smt_context.cpp      | 4 +++-
 src/smt/smt_context.h        | 5 ++++-
 src/smt/smt_internalizer.cpp | 1 +
 3 files changed, 8 insertions(+), 2 deletions(-)

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: