From 51040d3e19dae7046225405c27a6ef977167d4f5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 20 May 2015 18:32:40 +0100 Subject: [PATCH] Bugfix for fp.isNormal --- src/ast/fpa/fpa2bv_converter.cpp | 4 +++- src/util/mpf.cpp | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6d07092ea..83ba843ac 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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); } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 683140129..1dab7b995 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1428,7 +1428,7 @@ bool mpf_manager::is_ninf(mpf const & x) { } bool mpf_manager::is_normal(mpf const & x) { - return !(has_top_exp(x) || is_denormal(x)); + return !(has_top_exp(x) || is_denormal(x) || is_zero(x)); } bool mpf_manager::is_denormal(mpf const & x) {