mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-21 21:04:43 -07:00
parent 131dfc2101
commit 9da0b61d30
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/ast.cpp
View file

@ -3099,7 +3099,10 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
} }
if (!found_complement) { if (!found_complement) {
args.append(num_proofs, (expr**)proofs); args.append(num_proofs, (expr**)proofs);
CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n";); CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n";
for (unsigned i = 1; i < num_proofs; ++i)
tout << mk_pp(proofs[i], *this) << "\n";
);
SASSERT(is_or(f1)); SASSERT(is_or(f1));
ptr_buffer<expr> new_lits; ptr_buffer<expr> new_lits;
app const * cls = to_app(f1); app const * cls = to_app(f1);