diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 460aff29f..8db839e24 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3072,13 +3072,57 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
             m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
                 m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
                     m_bv_util.mk_numeral(1, 1))));
-    else
-        nanv = mk_to_ieee_bv_unspecified(ebits, sbits);
+    else {
+        expr_ref unspec_bits(m);
+        unspec_bits = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
+        nanv = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-1, unspec_bits),
+               m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
+                                   m_bv_util.mk_extract(sbits-2, 0, unspec_bits)));
+    }
 
     expr_ref sgn_e_s(m);
     sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
     m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
 
+    TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
+    SASSERT(is_well_sorted(m, result));
+}
+
+void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 0);
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
+
+    if (m_hi_fp_unspecified) {
+        result = m_bv_util.mk_concat(m_bv_util.mk_concat(
+                    m_bv_util.mk_numeral(0, 1),
+                    m_bv_util.mk_numeral(-1, ebits)),
+                    m_bv_util.mk_numeral(1, sbits-1));
+    }
+    else {
+        func_decl * fd;
+        if (m_uf2bvuf.find(f, fd))
+            result = m.mk_const(fd);
+        else {
+            fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range());
+            m_uf2bvuf.insert(f, fd);
+            m.inc_ref(f);
+            m.inc_ref(fd);
+            result = m.mk_const(fd);
+
+            expr_ref exp_bv(m), exp_all_ones(m);
+            exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
+            exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits));
+            m_extra_assertions.push_back(exp_all_ones);
+
+            expr_ref sig_bv(m), sig_is_non_zero(m);
+            sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
+            sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
+            m_extra_assertions.push_back(sig_is_non_zero);
+        }
+    }
+
+    TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);
     SASSERT(is_well_sorted(m, result));
 }
 
@@ -3308,41 +3352,10 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits
             m.inc_ref(fd);
         }
         result = m.mk_const(fd);
-        result = unspec;
     }
     return result;
 }
 
-expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
-    expr_ref result(m);
-
-    app_ref unspec(m);
-    unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
-    func_decl * unspec_fd = unspec->get_decl();
-    func_decl * fd;
-    if (!m_uf2bvuf.find(unspec_fd, fd)) {
-        app_ref bvc(m);
-        bvc = m.mk_fresh_const(0, unspec_fd->get_range());
-        fd = bvc->get_decl();
-        m_uf2bvuf.insert(unspec_fd, fd);
-        m.inc_ref(unspec_fd);
-        m.inc_ref(fd);
-    }
-    result = m.mk_const(fd);
-
-    app_ref mask(m), extra(m), result_and_mask(m);
-    mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
-        m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
-            m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
-                m_bv_util.mk_numeral(1, 1))));
-    expr * args[2] = { result, mask };
-    result_and_mask = m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args);
-    extra = m.mk_eq(result_and_mask, mask);
-    m_extra_assertions.push_back(extra);
-
-    return result;
-}
-
 void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
     SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 436f44364..4fcfe42f6 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -133,6 +133,7 @@ public:
     void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
     void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
@@ -152,13 +153,12 @@ public:
     expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
     expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
     expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
-    expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
 
     void reset(void);
 
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;
-    
+
     special_t const & get_min_max_specials() const { return m_min_max_specials; };
     const2bv_t const & get_const2bv() const { return m_const2bv; };
     const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; };
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 5f89e12db..6d4f24856 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -145,7 +145,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
-        case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
+        case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_REWRITE_FULL;
+        case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
 
         case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
         case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
@@ -161,7 +162,6 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
         case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
         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";
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index a3215dd6f..c00bed7ae 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -377,28 +377,28 @@ public:
     app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
     app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits);
 
-    bool is_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
-    bool is_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
-    bool is_bv2rm(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
-    bool is_bv2rm(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; }
+    bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
+    bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; }
+    bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); }
+    bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; }
 
-    bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
-    bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
-    bool is_max_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
-    bool is_max_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
-    bool is_to_ubv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
-    bool is_to_sbv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
-    bool is_to_ieee_bv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
-    bool is_to_real_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
+    bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); }
+    bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); }
+    bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); }
+    bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); }
+    bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); }
+    bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); }
+    bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); }
+    bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); }
 
-    bool is_min_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
-    bool is_min_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
-    bool is_max_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
-    bool is_max_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
-    bool is_to_ubv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
-    bool is_to_sbv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
-    bool is_to_ieee_bv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
-    bool is_to_real_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
+    bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; }
+    bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; }
+    bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; }
+    bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; }
+    bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; }
+    bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; }
+    bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; }
+    bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; }
 
     bool contains_floats(ast * a);
 };
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 92b373ca0..26487c5a4 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -18,11 +18,12 @@ Notes:
 --*/
 #include"fpa_rewriter.h"
 #include"fpa_rewriter_params.hpp"
+#include"ast_smt2_pp.h"
 
 fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) :
     m_util(m),
     m_fm(m_util.fm()),
-    m_hi_fp_unspecified(true) {
+    m_hi_fp_unspecified(false) {
     updt_params(p);
 }
 
@@ -117,34 +118,40 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 
 br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
     bv_util bu(m());
-    if (m_hi_fp_unspecified)
+    if (m_hi_fp_unspecified) {
         // The "hardware interpretation" is 0.
         result = bu.mk_numeral(0, width);
-    else
+        return BR_DONE;
+    }
+    else {
         result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
-
-    return BR_DONE;
+        return BR_REWRITE1;
+    }
 }
 
 br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) {
     bv_util bu(m());
-    if (m_hi_fp_unspecified)
+    if (m_hi_fp_unspecified) {
         // The "hardware interpretation" is 0.
         result = bu.mk_numeral(0, width);
-    else
+        return BR_DONE;
+    }
+    else {
         result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
-
-    return BR_DONE;
+        return BR_REWRITE1;
+    }
 }
 
 br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) {
-    if (m_hi_fp_unspecified)
+    if (m_hi_fp_unspecified) {
         // The "hardware interpretation" is 0.
         result = m_util.au().mk_numeral(rational(0), false);
-    else
+        return BR_DONE;
+    }
+    else {
         result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
-
-    return BR_DONE;
+        return BR_REWRITE1;
+    }
 }
 
 br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@@ -776,10 +783,8 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
         m_util.is_numeral(arg2, v)) {
         const mpf & x = v.get();
 
-        if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
-            mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
-            return BR_REWRITE_FULL;
-        }
+        if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v))
+            return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
 
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
@@ -789,11 +794,13 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz);
         ll = rational(0);
-        if (r >= ll && r <= ul)
+        if (r >= ll && r <= ul) {
             result = bu.mk_numeral(r, bv_sz);
+            return BR_DONE;
+        }
         else
-            mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
-        return BR_DONE;
+            return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
+
     }
 
     return BR_FAILED;
@@ -810,10 +817,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
         m_util.is_numeral(arg2, v)) {
         const mpf & x = v.get();
 
-        if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
-            mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
-            return BR_REWRITE_FULL;
-        }
+        if (m_fm.is_nan(v) || m_fm.is_inf(v))
+            return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
 
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
@@ -823,46 +828,42 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
         rational ul, ll;
         ul = m_fm.m_powers2.m1(bv_sz - 1);
         ll = - m_fm.m_powers2(bv_sz - 1);
-        if (r >= ll && r <= ul)
+        if (r >= ll && r <= ul) {
             result = bu.mk_numeral(r, bv_sz);
+            return BR_DONE;
+        }
         else
-            mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
-        return BR_DONE;
+            return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result);
     }
 
     return BR_FAILED;
 }
 
 br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
+    TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;);
     scoped_mpf v(m_fm);
 
     if (m_util.is_numeral(arg, v)) {
+        TRACE("fp_rewriter", tout << "to_ieee_bv numeral: " << m_fm.to_string(v) << std::endl;);
         bv_util bu(m());
         const mpf & x = v.get();
 
         if (m_fm.is_nan(v)) {
             if (m_hi_fp_unspecified) {
-                result = bu.mk_concat(bu.mk_numeral(0, 1),
-                         bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
-                         bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
-                                      bu.mk_numeral(1, 1))));
+                expr * args[4] = { bu.mk_numeral(0, 1),
+                                   bu.mk_numeral(-1, x.get_ebits()),
+                                   bu.mk_numeral(0, x.get_sbits() - 2),
+                                   bu.mk_numeral(1, 1) };
+                result = bu.mk_concat(4, args);
             }
-            else {
-                app_ref unspec(m()), mask(m()), extra(m());
-                unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
-                mask = bu.mk_concat(bu.mk_numeral(0, 1),
-                       bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()),
-                       bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2),
-                                    bu.mk_numeral(1, 1))));
-                expr * args[2] = { unspec, mask };
-                result = m().mk_app(bu.get_fid(), OP_BOR, 2, args);
-            }
-            return BR_REWRITE_FULL;
+            else
+                result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
+
+            return BR_REWRITE1;
         }
         else {
             scoped_mpz rz(m_fm.mpq_manager());
             m_fm.to_ieee_bv_mpz(v, rz);
-
             result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
             return BR_DONE;
         }
diff --git a/src/ast/rewriter/fpa_rewriter_params.pyg b/src/ast/rewriter/fpa_rewriter_params.pyg
index 85973e744..f0cfbdf55 100644
--- a/src/ast/rewriter/fpa_rewriter_params.pyg
+++ b/src/ast/rewriter/fpa_rewriter_params.pyg
@@ -1,5 +1,5 @@
 def_module_params(module_name='rewriter',
                   class_name='fpa_rewriter_params',
                   export=True,
-				  params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"),
+				  params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"),
 ))
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index fec7922c7..288b61748 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -715,14 +715,14 @@ namespace smt {
 
         fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf();
         for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin();
-             it !=  uf2bvuf.end();
-             it++) {
-            mg.hide(it->m_value);
+            it !=  uf2bvuf.end();
+            it++) {
+            //mg.hide(it->m_value);
         }
         fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials();
         for (fpa2bv_converter::special_t::iterator it = specials.begin();
-             it != specials.end();
-             it++) {
+            it != specials.end();
+            it++) {
             mg.hide(it->m_value.first->get_decl());
             mg.hide(it->m_value.second->get_decl());
         }
@@ -811,7 +811,25 @@ namespace smt {
         return res;
     }
 
-    void theory_fpa::finalize_model(model_generator & mg) {}
+    void theory_fpa::finalize_model(model_generator & mg) {
+        ast_manager & m = get_manager();
+        proto_model & mdl = mg.get_model();
+
+        fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf();
+        for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin();
+            it !=  uf2bvuf.end();
+            it++) {
+            func_decl * bv_fd = it->m_value;
+            if (bv_fd->get_arity() == 0) {
+                expr_ref bve(m), v(m);
+                bve = m.mk_const(bv_fd);
+                mdl.eval(bve, v, true);
+                mdl.register_decl(it->m_key, v);
+            }
+            else
+                NOT_IMPLEMENTED_YET();
+        }
+    }
 
     void theory_fpa::display(std::ostream & out) const
     {