mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 12:35:59 +00:00
Code Activity

add patch suggested by Arie Gurfinkel

Browse source 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
This commit is contained in:
nikolajbjorner 2015-02-23 11:18:24 -08:00
parent c3232693f0
commit fcb4962016
1 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz/base/proof_utils.cpp
View file

@ -156,12 +156,22 @@ public:
SASSERT(m.get_num_parents(p) == 1); SASSERT(m.get_num_parents(p) == 1);
tmp = m.get_parent(p, 0); tmp = m.get_parent(p, 0);
elim(tmp); elim(tmp);
get_literals(m.get_fact(p));
expr_set* hyps = m_hypmap.find(tmp); expr_set* hyps = m_hypmap.find(tmp);
expr_set* new_hyps = 0; expr_set* new_hyps = 0;
if (hyps) { if (hyps) {
new_hyps = alloc(expr_set, *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) { for (unsigned i = 0; i < m_literals.size(); ++i) {
expr* e = m_literals[i]; expr* e = m_literals[i];
if (!in_hypotheses(e, hyps)) { if (!in_hypotheses(e, hyps)) {