diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index e396bb6b5..94538861d 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -32,6 +32,7 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m_arith_util(m),
     m_mpf_manager(m_util.fm()),
     m_mpz_manager(m_mpf_manager.mpz_manager()),    
+    m_hi_fp_unspecified(true),
     m_extra_assertions(m) {
     m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
 }
@@ -2465,14 +2466,10 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
     mk_is_neg(x, x_is_neg);
     mk_is_nzero(x, x_is_nzero);
 
-    expr_ref undef(m);
-    undef = m_util.mk_internal_to_ubv_unspecified(bv_sz);
-    dbg_decouple("fpa2bv_to_ubv_undef", undef);
-
     // NaN, Inf, or negative (except -0) -> undefined
     expr_ref c1(m), v1(m);
     c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
-    v1 = undef;
+    v1 = mk_to_ubv_unspecified(bv_sz);
     dbg_decouple("fpa2bv_to_ubv_c1", c1);
 
     // +-Zero  -> 0
@@ -2556,8 +2553,8 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
     rounded = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded);
     rnd_has_overflown = m.mk_eq(rnd_overflow, bv1);
 
-    result = m.mk_ite(rnd_has_overflown, undef, rounded);
-    result = m.mk_ite(c_in_limits, result, undef);
+    result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rounded);
+    result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz));
     result = m.mk_ite(c2, v2, result);
     result = m.mk_ite(c1, v1, result);
 
@@ -2664,17 +2661,35 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     
     TRACE("fpa2bv_to_real", tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl; 
                             tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
-
-    expr_ref undef(m);
-    undef = m_util.mk_internal_to_real_unspecified();
     
     result = m.mk_ite(x_is_zero, zero, res);
-    result = m.mk_ite(x_is_inf, undef, result);
-    result = m.mk_ite(x_is_nan, undef, result);    
+    result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result);
+    result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result);
     
     SASSERT(is_well_sorted(m, result));
 }
 
+expr_ref fpa2bv_converter::mk_to_ubv_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_ubv_unspecified(width), m);
+}
+
+expr_ref fpa2bv_converter::mk_to_sbv_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_sbv_unspecified(width), m);
+}
+
+expr_ref fpa2bv_converter::mk_to_real_unspecified() {
+    if (m_hi_fp_unspecified)
+        return expr_ref(m_arith_util.mk_numeral(rational(0), false), m);
+    else
+        return expr_ref(m_util.mk_internal_to_real_unspecified(), m);
+}
+
 void fpa2bv_converter::split_triple(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
     SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FLOAT_TO_FP));
     SASSERT(to_app(e)->get_num_args() == 3);
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 440fc9d14..197c7ce9a 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -51,6 +51,7 @@ protected:
     mpf_manager              & m_mpf_manager;
     unsynch_mpz_manager      & m_mpz_manager;    
     float_decl_plugin        * m_plugin;
+    bool                       m_hi_fp_unspecified;
 
     obj_map<func_decl, expr*>  m_const2bv;
     obj_map<func_decl, expr*>  m_rm_const2bv;
@@ -137,6 +138,11 @@ public:
     void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
+    void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
+    expr_ref mk_to_ubv_unspecified(unsigned width);
+    expr_ref mk_to_sbv_unspecified(unsigned width);
+    expr_ref mk_to_real_unspecified();
+
     obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
     obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
     obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index c9296dd5b..797f681e7 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -24,6 +24,7 @@ Notes:
 #include"rewriter_def.h"
 #include"bv_decl_plugin.h"
 #include"fpa2bv_converter.h"
+#include"fpa2bv_rewriter_params.hpp"
 
 struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
     ast_manager              & m_manager;    
@@ -36,7 +37,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
     ast_manager & m() const { return m_manager; }
 
-    fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
+    fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) :
         m_manager(m),
         m_out(m),
         m_conv(c),
@@ -58,9 +59,16 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
     void reset() {
     }
 
+    void updt_local_params(params_ref const & _p) {
+        fpa2bv_rewriter_params p(_p);
+        bool v = p.hi_fp_unspecified();
+        m_conv.set_unspecified_fp_hi(v);
+    }
+
     void updt_params(params_ref const & p) {
-        m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_max_steps      = p.get_uint("max_steps", UINT_MAX);        
+        m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+        m_max_steps         = p.get_uint("max_steps", UINT_MAX);
+        updt_local_params(p);
     }
 
     bool max_steps_exceeded(unsigned num_steps) const {