mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix memory leak for scoped_numeral over trail objects

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-15 17:00:07 -08:00
parent 39dcc653df
commit ff54b3d92b
2 changed files with 27 additions and 2 deletions

27
src/opt/weighted_maxsat.cpp
View file

@ -184,6 +184,31 @@ namespace smt {
return !m_cost_save.empty();
}
// scoped_mpz leaks.
class numeral_trail : public trail<context> {
typedef scoped_mpz T;
T & m_value;
T* m_old_value;
// numeral_trail(numeral_trail const& nt);
public:
numeral_trail(T & value):
m_value(value),
m_old_value(alloc(T, value)) {
}
virtual ~numeral_trail() {
}
virtual void undo(context & ctx) {
m_value = *m_old_value;
dealloc(m_old_value);
m_old_value = 0;
}
};
virtual void assign_eh(bool_var v, bool is_true) {
TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";);
if (is_true) {
@ -192,7 +217,7 @@ namespace smt {
theory_var tv = m_bool2var[v];
if (m_assigned[tv]) return;
mpz const& w = m_zweights[tv];
ctx.push_trail(value_trail<context, scoped_mpz>(m_zcost));
ctx.push_trail(numeral_trail(m_zcost));
ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
m_zcost += w;

2
src/util/scoped_numeral.h
View file

@ -39,7 +39,7 @@ public:
numeral const & get() const { return m_num; }
numeral & get() { return m_num; }
_scoped_numeral & operator=(_scoped_numeral & n) {
_scoped_numeral & operator=(_scoped_numeral const & n) {
if (this == &n)
return *this;
m().set(m_num, n.m_num);