From 67fc369df0725c0f760ec9da122250ef0a867494 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Mar 2020 11:16:06 -0700 Subject: [PATCH] fix #3467 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index e180acd2c..6fc4117ed 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -533,7 +533,9 @@ struct purify_arith_proc { else { expr_ref s(u().mk_sin(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; } } @@ -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()); result = m().update_quantifier(q, new_body); if (m_produce_proofs) { - proof_ref_vector & cnstr_prs = r.cfg().m_new_cnstr_prs; - // cnstr_prs.push_back(result_pr); - // TODO: improve proof - 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())); + auto& cnstr_prs = r.cfg().m_new_cnstr_prs; + 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())); + r.cfg().push_cnstr_pr(result_pr); } } } @@ -771,7 +771,7 @@ struct purify_arith_proc { expr_ref new_curr(m()); proof_ref new_pr(m()); 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); r(curr, new_curr, new_pr); if (m_produce_proofs) {