mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Fix bug in fp.round_to_integral (#7060)

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2023-12-15 16:34:27 +00:00 committed by GitHub
parent e90a844508
commit 2e83352d42
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2189,7 +2189,13 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref &
renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
SASSERT(m_bv_util.get_bv_size(renorm_delta) == ebits + 2);
res_exp = m_bv_util.mk_bv_sub(res_exp, renorm_delta);
res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
if (sbits >= ebits+2)
res_sig = m_bv_util.mk_bv_shl(res_sig, m_bv_util.mk_zero_extend(sbits-ebits-2, renorm_delta));
else {
// should not overflow because renorm_delta is logarithmic to the size of the leading zero bits
res_sig = m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(ebits+2-sbits, res_sig), renorm_delta);
res_sig = m_bv_util.mk_extract(sbits-1, 0, res_sig);
}
dbg_decouple("fpa2bv_r2i_renorm_delta", renorm_delta);
dbg_decouple("fpa2bv_r2i_sig_lz", sig_lz);
dbg_decouple("fpa2bv_r2i_sig_lz_capped", sig_lz_capped);