From ed94bc2f6b31b68f41ce417b83e463bc6540f90e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 23 Oct 2015 14:58:29 +0100 Subject: [PATCH] Bugfix for fpa2bv converter. --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index c3feeb10a..c289d5804 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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() { diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 6ead927e0..53dc071ff 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -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::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; }