mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix #3461

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 14:46:24 -07:00
parent 9f1530fdc0
commit 61d9960420
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/th_rewriter.cpp
View file

@ -664,7 +664,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_ref & result, expr_ref & result,
proof_ref & result_pr) { proof_ref & result_pr) {
quantifier_ref q1(m()); quantifier_ref q1(m());
proof * p1 = nullptr; proof_ref p1(m());
if (is_quantifier(new_body) && if (is_quantifier(new_body) &&
to_quantifier(new_body)->get_kind() == old_q->get_kind() && to_quantifier(new_body)->get_kind() == old_q->get_kind() &&
to_quantifier(new_body)->get_kind() != lambda_k && to_quantifier(new_body)->get_kind() != lambda_k &&
@ -730,7 +730,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result_pr = nullptr; result_pr = nullptr;
if (m().proofs_enabled()) { if (m().proofs_enabled()) {
proof * p2 = nullptr; proof_ref p2(m());
if (q1.get() != result.get() && q1->get_kind() != lambda_k) if (q1.get() != result.get() && q1->get_kind() != lambda_k)
p2 = m().mk_elim_unused_vars(q1, result); p2 = m().mk_elim_unused_vars(q1, result);
result_pr = m().mk_transitivity(p1, p2); result_pr = m().mk_transitivity(p1, p2);