mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Bugfix for fpa2bv converter.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-23 14:58:29 +01:00
parent 9b5abcd55a
commit ed94bc2f6b
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -51,7 +51,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl());
m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl());
m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl());
}
fpa2bv_converter::~fpa2bv_converter() {

7
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -79,6 +79,13 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_hashtable<func_decl>::iterator it = m_decls_to_hide.begin();
it != m_decls_to_hide.end();
it++) {
func_decl * k = translator(*it);
res->m_decls_to_hide.insert(*it);
translator.to().inc_ref(*it);
}
return res;
}