diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 3ae660434..ff1d84171 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2925,11 +2925,22 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
     mk_ite(c1, v1, v2, result);
 }
 
+expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned width) {
+    if (m_hi_fp_unspecified)
+        return expr_ref(m_bv_util.mk_numeral(0, width), m);
+    else
+        return expr_ref(m_util.mk_internal_to_ieee_bv_unspecified(width), m);
+}
+
 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
+    expr_ref x(m), x_is_nan(m);
     expr * sgn, * s, * e;
-    split_fp(args[0], sgn, e, s);
-    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
+    x = args[0];
+    split_fp(x, sgn, e, s);
+    mk_is_nan(x, x_is_nan);
+    result = m.mk_ite(x_is_nan, mk_to_ieee_bv_unspecified(m_bv_util.get_bv_size(x)),
+                                m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s));
 }
 
 void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 8dc3dc019..7724d7673 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -136,6 +136,7 @@ public:
 
     expr_ref mk_to_ubv_unspecified(unsigned width);
     expr_ref mk_to_sbv_unspecified(unsigned width);
+    expr_ref mk_to_ieee_bv_unspecified(unsigned width);
     expr_ref mk_to_real_unspecified();
 
     void reset(void);
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 710faf447..27fc8ebc7 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -157,7 +157,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_INTERNAL_BVUNWRAP:
         case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
         case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
-        case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
+        case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
+        case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
+                return BR_FAILED;
         default:
             TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 7d0126d06..b89b9970b 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -1060,7 +1060,7 @@ app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) {
 app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) {
     parameter ps[] = { parameter(width) };
     sort * range = m_bv_util.mk_sort(width);
-    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range);
+    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range);
 }
 
 app * fpa_util::mk_internal_to_real_unspecified() {
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 57fb606ba..8352e14ce 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -107,6 +107,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break;
     case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
         SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break;
+    case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
+        SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break;
 
     case OP_FPA_INTERNAL_BVWRAP:
     case OP_FPA_INTERNAL_BVUNWRAP: