From 724f86d43e23a7230277dcb53a4d27d9db66c473 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 5 Apr 2018 19:55:04 +0100 Subject: [PATCH] Bugfix for unspecified semantics of some fp.* operators. --- src/ast/fpa/bv2fpa_converter.cpp | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 86a5b80c9..2bacae12a 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -311,8 +311,6 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * result->set_else(ft_els); } } - else - result->set_else(m.get_some_value(f->get_range())); return result; } @@ -467,20 +465,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode else { if (it->get_key().get_family_id() == m_fpa_util.get_fid()) { // it->m_value contains the model for the unspecified cases of it->m_key. - - func_interp * fmv = convert_func_interp(mc, f, it->m_value); - SASSERT(fmv); -#if 0 - // Upon request, add this 'recursive' definition? - unsigned n = fmv->get_arity(); - expr_ref_vector args(m); - for (unsigned i = 0; i < n; i++) - args.push_back(m.mk_var(i, f->get_domain()[i])); - fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); -#else - fmv->set_else(0); // Make sure it's not left open. -#endif - target_model->register_decl(f, fmv); + target_model->register_decl(f, convert_func_interp(mc, f, it->m_value)); } } }