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 fp.isNormal

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-20 18:32:40 +01:00
parent 1e3952406c
commit 51040d3e19
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3132,14 +3132,16 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp;
split_fp(e, sgn, exp, sig);
expr_ref is_special(m), is_denormal(m), p(m);
expr_ref is_special(m), is_denormal(m), p(m), is_zero(m);
mk_is_denormal(e, is_denormal);
mk_is_zero(e, is_zero);
unsigned ebits = m_bv_util.get_bv_size(exp);
p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits);
m_simp.mk_eq(exp, p, is_special);
expr_ref or_ex(m);
m_simp.mk_or(is_special, is_denormal, or_ex);
m_simp.mk_or(is_zero, or_ex, or_ex);
m_simp.mk_not(or_ex, result);
}