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

fix #3467

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 11:16:06 -07:00
parent b6618892d8
commit 67fc369df0
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -533,7 +533,9 @@ struct purify_arith_proc {
else { else {
expr_ref s(u().mk_sin(theta), m()); expr_ref s(u().mk_sin(theta), m());
expr_ref c(u().mk_cos(theta), m()); expr_ref c(u().mk_cos(theta), m());
push_cnstr(EQ(mk_real_one(), u().mk_add(u().mk_mul(s, s), u().mk_mul(c, c)))); expr_ref axm(EQ(mk_real_one(), u().mk_add(u().mk_mul(s, s), u().mk_mul(c, c))), m());
push_cnstr(axm);
push_cnstr_pr(m().mk_asserted(axm));
return BR_FAILED; return BR_FAILED;
} }
} }
@ -756,11 +758,9 @@ struct purify_arith_proc {
new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight()); new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight());
result = m().update_quantifier(q, new_body); result = m().update_quantifier(q, new_body);
if (m_produce_proofs) { if (m_produce_proofs) {
proof_ref_vector & cnstr_prs = r.cfg().m_new_cnstr_prs; auto& cnstr_prs = r.cfg().m_new_cnstr_prs;
// cnstr_prs.push_back(result_pr); result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr()));
// TODO: improve proof r.cfg().push_cnstr_pr(result_pr);
result_pr = m().mk_quant_intro(q, to_quantifier(result.get()),
m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr()));
} }
} }
} }
@ -771,7 +771,7 @@ struct purify_arith_proc {
expr_ref new_curr(m()); expr_ref new_curr(m());
proof_ref new_pr(m()); proof_ref new_pr(m());
unsigned sz = m_goal.size(); unsigned sz = m_goal.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; !m_goal.inconsistent() && i < sz; i++) {
expr * curr = m_goal.form(i); expr * curr = m_goal.form(i);
r(curr, new_curr, new_pr); r(curr, new_curr, new_pr);
if (m_produce_proofs) { if (m_produce_proofs) {