mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Fix for mk_to_fp_float; pertains to #4841

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2021-09-15 12:33:49 +00:00
parent 00e8ea7962
commit c24f438e51
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2561,9 +2561,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
res_sig = sig;
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
(void) sig_sz;
SASSERT(sig_sz == to_sbits + 4);
SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 4);
expr_ref exponent_overflow(m), exponent_underflow(m);
exponent_overflow = m.mk_false();
@ -2577,7 +2575,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz);
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
}
else if (from_ebits > (to_ebits + 2)) {
else if (from_ebits >= (to_ebits + 2)) {
unsigned ebits_diff = from_ebits - (to_ebits + 2);
// subtract lz for subnormal numbers.
@ -2617,9 +2615,6 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
res_exp = m.mk_ite(ovf_cond, max_exp, res_exp);
res_exp = m.mk_ite(udf_cond, min_exp, res_exp);
}
else { // from_ebits == (to_ebits + 2)
res_exp = m_bv_util.mk_bv_sub(exp, lz);
}
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2);
SASSERT(is_well_sorted(m, res_exp));