mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix memory leak in scoped_numeral_vector

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-22 20:34:34 -07:00
parent 92145f2bfa
commit ea261c930d
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/opt/weighted_maxsat.cpp
View file

@ -79,7 +79,9 @@ namespace smt {
m_normalize(false) 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. \brief return the complement of variables that are currently assigned.
@ -208,7 +210,7 @@ namespace smt {
virtual void undo(context & ctx) { virtual void undo(context & ctx) {
m_value = m_old_values.back(); 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(); context& ctx = get_context();
theory_var tv = m_bool2var[v]; theory_var tv = m_bool2var[v];
if (m_assigned[tv]) return; 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(numeral_trail(m_zcost, m_old_values));
ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs)); ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<context, bool>(m_assigned[tv])); ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));

4
src/util/scoped_numeral_vector.h
View file

@ -46,6 +46,10 @@ public:
m_manager.set(this->back(), v); m_manager.set(this->back(), v);
} }
void pop_back() {
shrink(size()-1);
}
void shrink(unsigned sz) { void shrink(unsigned sz) {
unsigned old_sz = this->size(); unsigned old_sz = this->size();
if (old_sz == sz) if (old_sz == sz)