diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index ed3a66515..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);
 }
 
@@ -3351,7 +3353,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {    
     #ifdef Z3DEBUG
-    // return;
+    return;
     // CMW: This works only for quantifier-free formulas.
     expr_ref new_e(m);
     new_e = m.mk_fresh_const(prefix, m.get_sort(e));
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index e559ee179..0b28c4277 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -289,7 +289,7 @@ func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_param
 
 func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 2)
+    if (arity < 2)
         m_manager->raise_exception("invalid number of arguments to floating point relation");
     if (domain[0] != domain[1] || !is_float_sort(domain[0]))
         m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
@@ -306,7 +306,7 @@ func_decl * fpa_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_parameter
     }
     func_decl_info finfo(m_family_id, k);
     finfo.set_chainable(true);
-    return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), finfo);
+    return m_manager->mk_func_decl(name, domain[0], domain[1], m_manager->mk_bool_sort(), finfo);
 }
 
 func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
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) {