From a9df4a208faa40bb4f500d2a42cc378d699f1ffd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Mar 2016 14:58:55 +0000 Subject: [PATCH] More bugfixes for fp.to_ieee_bv for unspecified input/output. Relates to #507 --- src/ast/fpa/fpa2bv_converter.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ff1d84171..9ecac1ec9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2939,8 +2939,17 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * x = args[0]; split_fp(x, sgn, e, s); mk_is_nan(x, x_is_nan); - result = m.mk_ite(x_is_nan, mk_to_ieee_bv_unspecified(m_bv_util.get_bv_size(x)), - m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); + + sort * fp_srt = m.get_sort(x); + unsigned ebits = m_util.get_ebits(fp_srt); + unsigned sbits = m_util.get_sbits(fp_srt); + + expr_ref sig_unspec(s, m); + if (sbits > 2) + sig_unspec = m_bv_util.mk_concat(mk_to_ieee_bv_unspecified(sbits - 2), + m_bv_util.mk_numeral(1, 1)); + + result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s)); } void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {