mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Bugfix for fpa2bv translation

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-07-13 15:35:14 +01:00
parent f96cfeae9e
commit cfbe16639f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);