From cfbe16639f9fd1445ab6595fc68bbb895011dc69 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jul 2016 15:35:14 +0100 Subject: [PATCH] Bugfix for fpa2bv translation --- src/ast/fpa/fpa2bv_converter.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index e89664216..d3257ac55 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3641,11 +3641,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref // the maximum shift is `sbits', because after that the mantissa // would be zero anyways. So we can safely cut the shift variable down, // as long as we check the higher bits. - expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); - zero_s = m_bv_util.mk_numeral(0, sbits-1); + expr_ref zero_ems(m), sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); + zero_ems = m_bv_util.mk_numeral(0, ebits - sbits); sbits_s = m_bv_util.mk_numeral(sbits, sbits); sh = m_bv_util.mk_extract(ebits-1, sbits, shift); - m_simp.mk_eq(zero_s, sh, is_sh_zero); + m_simp.mk_eq(zero_ems, sh, is_sh_zero); short_shift = m_bv_util.mk_extract(sbits-1, 0, shift); m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);