From 5d289a8da50fc790326d51efb565a6036ed42732 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 29 Nov 2015 10:49:52 +0000 Subject: [PATCH] fix leak in asserted_formulas::propagate_values() for proof generation mode continuation of issue #342 Signed-off-by: Nuno Lopes --- src/smt/asserted_formulas.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index a6072df0e..fa0ec62d4 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -606,8 +606,8 @@ void asserted_formulas::propagate_values() { proof_ref_vector new_prs2(m_manager); unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) { - expr_ref n(m_asserted_formulas.get(i), m_manager); - proof * pr = m_asserted_formula_prs.get(i, 0); + expr_ref n(m_asserted_formulas.get(i), m_manager); + proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager); TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";); if (m_manager.is_eq(n)) { expr * lhs = to_app(n)->get_arg(0);