From ea261c930d6f335f22acc6a8489b7e2f799afd2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Mar 2014 20:34:34 -0700 Subject: [PATCH] fix memory leak in scoped_numeral_vector Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 9 ++++++--- src/util/scoped_numeral_vector.h | 4 ++++ 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 5d42bb63a..597bfa6b0 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -79,7 +79,9 @@ namespace smt { m_normalize(false) {} - virtual ~theory_weighted_maxsat() { } + virtual ~theory_weighted_maxsat() { + m_old_values.reset(); + } /** \brief return the complement of variables that are currently assigned. @@ -208,7 +210,7 @@ namespace smt { virtual void undo(context & ctx) { m_value = m_old_values.back(); - m_old_values.pop_back(); + m_old_values.shrink(m_old_values.size() - 1); } }; @@ -219,7 +221,8 @@ namespace smt { context& ctx = get_context(); theory_var tv = m_bool2var[v]; if (m_assigned[tv]) return; - mpz const& w = m_zweights[tv]; + scoped_mpz w(m_mpz); + w = m_zweights[tv]; ctx.push_trail(numeral_trail(m_zcost, m_old_values)); ctx.push_trail(push_back_vector >(m_costs)); ctx.push_trail(value_trail(m_assigned[tv])); diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index 4375babb3..585bfa895 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -46,6 +46,10 @@ public: m_manager.set(this->back(), v); } + void pop_back() { + shrink(size()-1); + } + void shrink(unsigned sz) { unsigned old_sz = this->size(); if (old_sz == sz)