From 2744d806421c771052a60bdd503f4332eeb47922 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Sep 2015 14:22:02 +0100 Subject: [PATCH] Fixed reference counting in fpa2bv converter. --- src/ast/fpa/fpa2bv_converter.cpp | 6 ++++-- src/tactic/fpa/fpa2bv_model_converter.h | 14 ++++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 20c4822d2..8d012ca9b 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -253,8 +253,10 @@ void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, ex new_domain.push_back(f->get_domain()[i]); if (!is_float(f->get_range())) - { - func_decl * fbv = m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range(), *f->get_info()); + { + func_decl_ref fbv(m); + fbv = (f->get_info()) ? m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range(), *f->get_info()) : + m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range()); TRACE("fpa2bv_dbg", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl; ); m_uf2bvuf.insert(f, fbv); m.inc_ref(f); diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index ef8ea91f5..f36e8e068 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -66,12 +66,26 @@ public: { m_uf23bvuf.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); + m.inc_ref(it->m_value.f_sgn); + m.inc_ref(it->m_value.f_sig); + m.inc_ref(it->m_value.f_exp); } } virtual ~fpa2bv_model_converter() { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); + dec_ref_map_key_values(m, m_uf2bvuf); + + obj_map::iterator it = m_uf23bvuf.begin(); + obj_map::iterator end = m_uf23bvuf.end(); + for (; it != end; ++it) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.f_sgn); + m.dec_ref(it->m_value.f_sig); + m.dec_ref(it->m_value.f_exp); + } + m_uf23bvuf.reset(); } virtual void operator()(model_ref & md, unsigned goal_idx) {