From fcb4962016bab1064dd98ff094a5227346fe6951 Mon Sep 17 00:00:00 2001 From: nikolajbjorner Date: Mon, 23 Feb 2015 11:18:24 -0800 Subject: [PATCH 1/2] add patch suggested by Arie Gurfinkel Signed-off-by: nikolajbjorner --- src/muz/base/proof_utils.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp index 87ecf9985..d4a8ab22b 100644 --- a/src/muz/base/proof_utils.cpp +++ b/src/muz/base/proof_utils.cpp @@ -156,12 +156,22 @@ public: SASSERT(m.get_num_parents(p) == 1); tmp = m.get_parent(p, 0); elim(tmp); - get_literals(m.get_fact(p)); expr_set* hyps = m_hypmap.find(tmp); expr_set* new_hyps = 0; if (hyps) { new_hyps = alloc(expr_set, *hyps); } + expr* fact = m.get_fact(p); + // when hypothesis is a single literal of the form + // (or A B), and the fact of p is (or A B). + if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) { + m_literals.reset(); + m_literals.push_back(fact); + } + else { + get_literals(fact); + } + for (unsigned i = 0; i < m_literals.size(); ++i) { expr* e = m_literals[i]; if (!in_hypotheses(e, hyps)) { From fbf8289394f4e4d78ef9c360e4b4b47d9bd961b4 Mon Sep 17 00:00:00 2001 From: nikolajbjorner Date: Tue, 24 Feb 2015 14:02:23 -0800 Subject: [PATCH 2/2] probe also hard constraints before enabling SAT solver. Bug reported by Zvonimir Pavlinovic Signed-off-by: nikolajbjorner --- src/opt/opt_context.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index f22ce479e..b98343013 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -533,6 +533,9 @@ namespace opt { for (unsigned i = 0; i < sz; i++) { quick_for_each_expr(proc, visited, get_solver().get_assertion(i)); } + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + quick_for_each_expr(proc, visited, m_hard_constraints[i].get()); + } } catch (is_bv::found) { return false;