mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

fix #3275

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-13 13:55:12 -07:00
parent 59755dd72e
commit 31c3ac016a
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/ast.cpp
View file

@ -3107,6 +3107,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
#ifdef Z3DEBUG #ifdef Z3DEBUG
svector<bool> found; svector<bool> found;
#endif #endif
ast_mark mark;
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
bool found_complement = false; bool found_complement = false;
expr * lit = cls->get_arg(i); expr * lit = cls->get_arg(i);
@ -3118,8 +3119,12 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
break; break;
} }
} }
if (!found_complement) if (!found_complement) {
new_lits.push_back(lit); if (!mark.is_marked(lit)) {
new_lits.push_back(lit);
mark.mark(lit, true);
}
}
} }
DEBUG_CODE({ DEBUG_CODE({
for (unsigned i = 1; proofs_enabled() && i < num_proofs; i++) { for (unsigned i = 1; proofs_enabled() && i < num_proofs; i++) {
@ -3168,7 +3173,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
SASSERT(is_or(f1)); SASSERT(is_or(f1));
app * cls = to_app(f1); app * cls = to_app(f1);
unsigned cls_sz = cls->get_num_args(); unsigned cls_sz = cls->get_num_args();
CTRACE("cunit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))), CTRACE("unit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))),
for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n"; for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
tout << "===>\n"; tout << "===>\n";
tout << mk_pp(new_fact, *this) << "\n";); tout << mk_pp(new_fact, *this) << "\n";);
@ -3187,7 +3192,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
} }
} }
if (j == num_proofs) { if (j == num_proofs) {
CTRACE("unit_bug1", new_fact != lit, tout << mk_ll_pp(new_fact, *this) << "\n" << mk_ll_pp(lit, *this) << "\n";); CTRACE("unit_bug", new_fact != lit, tout << mk_pp(f1, *this) << "\n" << mk_ll_pp(new_fact, *this) << "\n" << mk_ll_pp(lit, *this) << "\n";);
SASSERT(new_fact == lit); SASSERT(new_fact == lit);
++num_occ; ++num_occ;
} }