mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

#6320

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-05 13:44:16 -07:00
parent 9717dadd9f
commit 9732169b04
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/ast.cpp
View file

@ -3027,11 +3027,23 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
found_complement = true; found_complement = true;
} }
} }
// patch to deal with lambdas introduced during search.
// lambdas can occur in terms both internalized and in raw form.
if (!found_complement && !is_or(f1) && num_proofs == 2) {
args.push_back(proofs[0]);
args.push_back(proofs[1]);
args.push_back(mk_false());
found_complement = true;
}
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) for (unsigned i = 1; i < num_proofs; ++i)
tout << mk_pp(proofs[i], *this) << "\n"; tout << mk_pp(proofs[i], *this) << "\n";
tout << "facts\n";
for (unsigned i = 0; i < num_proofs; ++i)
tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
); );
SASSERT(is_or(f1)); SASSERT(is_or(f1));
ptr_buffer<expr> new_lits; ptr_buffer<expr> new_lits;