diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 89072a795..738422b89 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2952,11 +2952,16 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr * sgn, *sig, *exp;
     split_fp(e, sgn, exp, sig);
-    expr_ref zero(m);
+
+    expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
     zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
     m_simp.mk_eq(exp, zero, result);
+    m_simp.mk_eq(exp, zero, zexp);
+    mk_is_zero(e, is_zero);
+    m_simp.mk_not(is_zero, n_is_zero);
+    m_simp.mk_and(n_is_zero, zexp, result);
 }
 
 void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {    
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 4e452b1e8..d28395195 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1350,7 +1350,7 @@ bool mpf_manager::is_ninf(mpf const & x) {
 }
 
 bool mpf_manager::is_normal(mpf const & x) {
-    return !has_bot_exp(x) && !has_top_exp(x);
+    return !is_zero(x) && has_bot_exp(x);
 }
 
 bool mpf_manager::is_denormal(mpf const & x) {