mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits).

Browse source 
Fixes #439.
This commit is contained in:
Christoph M. Wintersteiger 2016-02-07 17:33:33 +00:00
parent e9d94e53f6
commit 92b6a3e134
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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