From 4ed2b8a0f9d900547cfed92844418e7541ed1595 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 20 May 2016 20:15:08 +0100 Subject: [PATCH] Bugfix for unspecified FP model values. --- src/tactic/fpa/fpa2bv_model_converter.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index d8b826525..41650eda6 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -401,10 +401,19 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { func_decl * f = it->m_key; if (f->get_arity() == 0) { - array_model am = convert_array_func_interp(f, it->m_value, bv_mdl); - if (am.new_float_fd) float_mdl->register_decl(am.new_float_fd, am.new_float_fi); - if (am.result) float_mdl->register_decl(f, am.result); - if (am.bv_fd) seen.insert(am.bv_fd); + array_util au(m); + if (au.is_array(f->get_range())) { + array_model am = convert_array_func_interp(f, it->m_value, bv_mdl); + if (am.new_float_fd) float_mdl->register_decl(am.new_float_fd, am.new_float_fi); + if (am.result) float_mdl->register_decl(f, am.result); + if (am.bv_fd) seen.insert(am.bv_fd); + } + else { + // Just keep. + expr_ref val(m); + bv_mdl->eval(it->m_value, val); + float_mdl->register_decl(f, val); + } } else { func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl);