From db3f439e88c5696011da8beb3f7c363b686182aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 May 2018 20:55:30 -0700 Subject: [PATCH 1/2] fix memory leak from Arie Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 605c447bd..c00fb93b1 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -500,6 +500,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) { void asserted_formulas::update_substitution(expr* n, proof* pr) { expr* lhs, *rhs, *n1; + proof_ref pr1(m); if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { compute_depth(lhs); compute_depth(rhs); @@ -510,12 +511,12 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { } if (is_gt(rhs, lhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); - m_scoped_substitution.insert(rhs, lhs, m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr); + pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr; + m_scoped_substitution.insert(rhs, lhs, pr1); return; } TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } - proof_ref pr1(m); if (m.is_not(n, n1)) { pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr; m_scoped_substitution.insert(n1, m.mk_false(), pr1); From 0d668e14289c0728b65bbcc214749ac865297507 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 May 2018 03:18:22 -0700 Subject: [PATCH 2/2] fix #1661 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index e4a34fc93..3862aecae 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -357,8 +357,8 @@ struct pb2bv_rewriter::imp { /** \brief MiniSat+ based encoding of PB constraints. - The procedure is described in "Translating Pseudo-Boolean Constraints into SAT " -         Niklas Een, Niklas Sörensson, JSAT 2006. + Translating Pseudo-Boolean Constraints into SAT, + Niklas Een, Niklas Soerensson, JSAT 2006. */