From 21d9875239a3bad48be41dd0e6973a2b960f2ba2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 9 Dec 2019 10:48:59 -1000 Subject: [PATCH] integrating changes of Nikolaj with m_empty_clause etc. Signed-off-by: Lev Nachmanson --- src/smt/smt_internalizer.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index efca6c042..56eecbd15 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1346,13 +1346,15 @@ namespace smt { bool lemma = is_lemma(k); m_stats.m_num_mk_lits += num_lits; switch (num_lits) { - case 0: + case 0: { if (j && !j->in_region()) 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: if (j && !j->in_region()) m_justifications.push_back(j);