From 3c8c80bbaccfdc7ecc17a128abe63896cb2fa0df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Sep 2022 12:33:28 -0700 Subject: [PATCH] fix #6336 --- src/ast/fpa/fpa2bv_converter.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8c1ff40cd..18baba57c 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3431,8 +3431,14 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args } else { expr_ref ll(m); - ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); - ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz-1))); + ll = bv1; + if (bv_sz > 1) + ll = m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz - 1)); + ll = m_bv_util.mk_sign_extend(3, ll); + if (bv_sz > 1) + ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz - 1))); + else + ul = m_bv_util.mk_numeral(0, 4); ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz + 3)))); pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); in_range = m.mk_and(m.mk_not(ovfl),