From 4f988595c7800dafd63e81015cbce1e0cd32ec3b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 27 Jan 2019 19:45:19 -0800
Subject: [PATCH] fix #2107
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c8b8d27de..9d4c9f852 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3244,8 +3244,13 @@ namespace smt {
proof * pr = m_manager.mk_asserted(curr_assumption);
internalize_assertion(curr_assumption, pr, 0);
literal l = get_literal(curr_assumption);
+ if (l == true_literal)
+ continue;
+ if (l == false_literal) {
+ set_conflict(b_justification::mk_axiom());
+ break;
+ }
m_literal2assumption.insert(l.index(), orig_assumption);
- // mark_as_relevant(l); <<< not needed
// internalize_assertion marked l as relevant.
SASSERT(is_relevant(l));
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);