From 04df77e89d1f2a62c8f23b6d6ab4cf5fb4732942 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Dec 2019 02:40:38 -0800 Subject: [PATCH] revert empty clause handling Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d7bde6e23..c98c26485 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2399,7 +2399,8 @@ namespace smt { m_empty_clause = false; } else { - m_conflict = m_empty_clause ? b_justification::mk_axiom() : 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);