mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Fixed memory leak in theory_fpa. Relates to #436

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-08 17:17:49 +00:00
parent 7e2783c6a2
commit a2f376f9d6
1 changed files with 11 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_fpa.cpp
View file

@ -26,17 +26,17 @@ namespace smt {
class fpa2bv_conversion_trail_elem : public trail<theory_fpa> { class fpa2bv_conversion_trail_elem : public trail<theory_fpa> {
ast_manager & m; ast_manager & m;
obj_map<expr, expr*> & m_conversions; obj_map<expr, expr*> & m_map;
expr * m_e; expr_ref key;
public: public:
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) : fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & map, expr * e) :
m(m), m_conversions(c), m_e(e) { m.inc_ref(e); } m(m), m_map(map), key(e, m) { }
virtual ~fpa2bv_conversion_trail_elem() { } virtual ~fpa2bv_conversion_trail_elem() { }
virtual void undo(theory_fpa & th) { virtual void undo(theory_fpa & th) {
expr * v = m_conversions.find(m_e); expr * val = m_map.find(key);
m_conversions.remove(m_e); m_map.remove(key);
m.dec_ref(v); m.dec_ref(val);
m.dec_ref(m_e); key = 0;
} }
}; };
@ -153,6 +153,8 @@ namespace smt {
theory_fpa::~theory_fpa() theory_fpa::~theory_fpa()
{ {
m_trail_stack.reset();
if (m_is_initialized) { if (m_is_initialized) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
dec_ref_map_values(m, m_conversions); dec_ref_map_values(m, m_conversions);