From b29c77dc87e42c2bb7584e595e4ea21ceaf74964 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 09:51:18 -0700 Subject: [PATCH] fix #3295 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index bf9ef9e65..9cfd172fa 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -757,7 +757,7 @@ struct purify_arith_proc { 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); + // 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()));