mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

bugfix for sign computation in floating-point FMA

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-02-13 19:33:51 +00:00
parent f45ad4bdc0
commit e860c65567
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -1368,12 +1368,12 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
not_f_sgn = m_bv_util.mk_bv_not(f_sgn);
not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv);
res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv);
res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs);
sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);