From a09ed766f56faea184002a90bcad0b6fcd2046df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 11:41:41 -0700 Subject: [PATCH] fix #3226 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 719d82b41..b6cdaca9f 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3176,7 +3176,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro // typically: num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact)) // but formula could have repeated literals that are merged in the clausal representation. // - unsigned num_matches = 0; + unsigned num_matches = 0, num_occ = 0; for (unsigned i = 0; i < cls_sz; i++) { expr * lit = cls->get_arg(i); unsigned j = 1; @@ -3189,9 +3189,10 @@ 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";); SASSERT(new_fact == lit); + ++num_occ; } } - SASSERT(num_matches == cls_sz || num_matches == cls_sz - 1); + SASSERT(num_matches == cls_sz || num_matches == cls_sz - num_occ); SASSERT(num_matches != cls_sz || is_false(new_fact)); } #endif