diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index c6b413dd4..eed5f7553 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1155,8 +1155,6 @@ extern "C" {
             case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO;
             case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL;
             case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL;
-            case OP_FPA_IS_PZERO: return Z3_OP_FPA_IS_PZERO;
-            case OP_FPA_IS_NZERO: return Z3_OP_FPA_IS_NZERO;
             case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE;
             case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE;
             case OP_FPA_FP: return Z3_OP_FPA_FP;
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index cbbd9e8a7..c7a987b83 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -143,9 +143,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
             case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
             case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
-            case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
-            case OP_FPA_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
-            case OP_FPA_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
+            case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;            
             case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
             case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
             case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 90bbd4901..52a1a95f7 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -294,8 +294,6 @@ func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_paramet
     symbol name;
     switch (k) {
     case OP_FPA_IS_ZERO: name = "fp.isZero";  break;
-    case OP_FPA_IS_NZERO: name = "fp.isNZero";   break;
-    case OP_FPA_IS_PZERO: name = "fp.isPZero";   break;        
     case OP_FPA_IS_NEGATIVE: name = "fp.isNegative";  break;
     case OP_FPA_IS_POSITIVE: name = "fp.isPositive";  break;
     case OP_FPA_IS_NAN: name = "fp.isNaN";  break;
@@ -717,8 +715,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_GE:
         return mk_bin_rel_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_IS_ZERO:
-    case OP_FPA_IS_NZERO:
-    case OP_FPA_IS_PZERO:
     case OP_FPA_IS_NEGATIVE: 
     case OP_FPA_IS_POSITIVE:
     case OP_FPA_IS_NAN:
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index b8d0c0c3e..44f0e62c4 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -71,8 +71,6 @@ enum fpa_op_kind {
     OP_FPA_IS_ZERO,
     OP_FPA_IS_NORMAL,
     OP_FPA_IS_SUBNORMAL,
-    OP_FPA_IS_PZERO,
-    OP_FPA_IS_NZERO,
     OP_FPA_IS_NEGATIVE,
     OP_FPA_IS_POSITIVE,
 
@@ -325,8 +323,6 @@ public:
     app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); }
     app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); }
     app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); }
-    app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NZERO, arg1); }
-    app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_PZERO, arg1); }
     app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); }
     app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); }
     app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); }
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 2977b7ab2..e7b8c7b34 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -57,8 +57,6 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_LE:        SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
     case OP_FPA_GE:        SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break;
     case OP_FPA_IS_ZERO:   SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
-    case OP_FPA_IS_NZERO:  SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
-    case OP_FPA_IS_PZERO:  SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
     case OP_FPA_IS_NAN:    SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break;
     case OP_FPA_IS_INF:    SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
     case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;