From 3a2ed691f896ac244b4010d451797e74e45cffb5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jan 2021 00:49:28 -0800 Subject: [PATCH] fix #4952 Signed-off-by: Nikolaj Bjorner --- src/smt/dyn_ack.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index b70c39c6e..fcd26ed53 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -73,11 +73,11 @@ namespace smt { ast_manager & m = cr.get_manager(); context & ctx = cr.get_context(); unsigned num_args = m_app1->get_num_args(); - ptr_buffer prs; - ptr_buffer lits; + proof_ref_vector prs(m); + expr_ref_vector lits(m); for (unsigned i = 0; i < num_args; i++) { - expr * arg1 = m_app1->get_arg(i); - expr * arg2 = m_app2->get_arg(i); + expr * arg1 = m_app1->get_arg(i); + expr * arg2 = m_app2->get_arg(i); if (arg1 != arg2) { app * eq = m.mk_eq(arg1, arg2); app_ref neq(m.mk_not(eq), m); @@ -87,16 +87,16 @@ namespace smt { } } } - proof * antecedents[2]; - antecedents[0] = m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr()); - app * eq = m.mk_eq(m_app1, m_app2); - antecedents[1] = mk_hypothesis(m, eq, true, m_app1, m_app2); - proof * false_pr = m.mk_unit_resolution(2, antecedents); + app_ref eq(m.mk_eq(m_app1, m_app2), m); + proof_ref a1(m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr()), m); + proof_ref a2(mk_hypothesis(m, eq, true, m_app1, m_app2), m); + proof * antecedents[2] = { a1.get(), a2.get() }; + proof_ref false_pr(m.mk_unit_resolution(2, antecedents), m); lits.push_back(eq); SASSERT(lits.size() >= 2); - app * lemma = m.mk_or(lits.size(), lits.c_ptr()); - TRACE("dyn_ack", tout << mk_pp(lemma, m) << "\n";); - TRACE("dyn_ack", tout << mk_pp(false_pr, m) << "\n";); + app_ref lemma(m.mk_or(lits), m); + TRACE("dyn_ack", tout << lemma << "\n";); + TRACE("dyn_ack", tout << false_pr << "\n";); return m.mk_lemma(false_pr, lemma); }