From 92b6a3e1348484c8354365380e8ece24f870b929 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 7 Feb 2016 17:33:33 +0000 Subject: [PATCH] Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). Fixes #439. --- src/ast/fpa/fpa2bv_converter.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1d66b793d..40bb7efe8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -419,11 +419,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_exp_delta", exp_delta); - // cap the delta - expr_ref cap(m), cap_le_delta(m); - cap = m_bv_util.mk_numeral(sbits+2, ebits); - cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); - m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); + if (log2(sbits + 2) < ebits + 2) + { + // cap the delta + expr_ref cap(m), cap_le_delta(m); + cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); + cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); + m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); + dbg_decouple("fpa2bv_add_exp_cap", cap); + } dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);