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

Bugfix for fp.fma

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 18:36:19 +01:00
parent 3f32732ec9
commit 81218c0983
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1417,10 +1417,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
expr * res_or_args[2] = { m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky };
res_sig = m_bv_util.mk_bv_or(2, res_or_args);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
expr_ref is_zero_sig(m), nil_sbits4(m);
nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);