From 31c3ac016a23d3e827de5f314ceb6a3aaa9579aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2020 13:55:12 -0700 Subject: [PATCH] fix #3275 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b6cdaca9f..204c76287 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3107,6 +3107,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro #ifdef Z3DEBUG svector found; #endif + ast_mark mark; for (unsigned i = 0; i < num_args; i++) { bool found_complement = false; expr * lit = cls->get_arg(i); @@ -3118,8 +3119,12 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro break; } } - if (!found_complement) - new_lits.push_back(lit); + if (!found_complement) { + if (!mark.is_marked(lit)) { + new_lits.push_back(lit); + mark.mark(lit, true); + } + } } DEBUG_CODE({ 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)); app * cls = to_app(f1); 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"; tout << "===>\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) { - 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); ++num_occ; }