mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Fixed reference counting in fpa2bv converter.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-23 14:22:02 +01:00
parent 04266fccc9
commit 2744d80642
2 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);

14
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -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<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
obj_map<func_decl, func_decl_triple>::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) {