diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index ae9f321d1..30d41bc53 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -285,7 +285,21 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
             bv_fres = bv_fe->get_result();
             ft_fres = rebuild_floats(mc, rng, to_app(bv_fres));
             m_th_rw(ft_fres);
-            result->insert_new_entry(new_args.c_ptr(), ft_fres);
+            TRACE("bv2fpa",
+                  for (unsigned i = 0; i < new_args.size(); i++)
+                      tout << mk_ismt2_pp(bv_args[i], m) << " == " <<
+                        mk_ismt2_pp(new_args[i], m) << std::endl;
+                  tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
+            func_entry * fe = result->get_entry(new_args.c_ptr());
+            if (fe == 0)
+                result->insert_new_entry(new_args.c_ptr(), ft_fres);
+            else {
+                // The BV model may have multiple equivalent entries using different
+                // representations of NaN. We can only keep one and we check that
+                // the results for all those entries are the same.
+                if (ft_fres != fe->get_result())
+                    throw default_exception("BUG: UF function entries disagree with each other");
+            }
         }
 
         app_ref bv_els(m);
@@ -462,6 +476,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
                         args.push_back(m.mk_var(i, f->get_domain()[i]));
                     fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
 #else
+
                     fmv->set_else(0);
 #endif
                     target_model->register_decl(f, fmv);
@@ -476,7 +491,6 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
 }
 
 void bv2fpa_converter::display(std::ostream & out) {
-    out << "(fpa2bv-model-converter";
     for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
         it != m_const2bv.end();
         it++) {
@@ -510,7 +524,6 @@ void bv2fpa_converter::display(std::ostream & out) {
         out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
             mk_ismt2_pp(it->m_value.second, m, indent) << ")";
     }
-    out << ")";
 }
 
 bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index f0707a273..5314bed07 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3312,11 +3312,11 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m);
     big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift),
                                              m_bv_util.mk_bv_shl(big_sig, shift));
-    int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-bv_sz-3, big_sig_shifted);
+    int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted);
     SASSERT(m_bv_util.get_bv_size(int_part) == bv_sz+3);
-    last     = m_bv_util.mk_extract(big_sig_sz-bv_sz-4, big_sig_sz-bv_sz-4, big_sig_shifted);
-    round    = m_bv_util.mk_extract(big_sig_sz-bv_sz-5, big_sig_sz-bv_sz-5, big_sig_shifted);
-    stickies = m_bv_util.mk_extract(big_sig_sz-bv_sz-6, 0, big_sig_shifted);
+    last     = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted);
+    round    = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted);
+    stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted);
     sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, stickies);
     dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);
     dbg_decouple("fpa2bv_to_bv_int_part", int_part);
@@ -3335,25 +3335,25 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     dbg_decouple("fpa2bv_to_bv_inc", inc);
     dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded);
 
-    expr_ref out_of_range(m);
+    expr_ref in_range(m);
     if (!is_signed) {
         expr_ref ul(m);
-        ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
-        out_of_range = m_bv_util.mk_ule(ul, pre_rounded);
+        ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz));
+        in_range = m_bv_util.mk_ule(pre_rounded, ul);
     }
     else {
         expr_ref ll(m), ul(m);
         ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1)));
         ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1));
-        out_of_range = m.mk_not(m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)));
+        in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul));
     }
-    dbg_decouple("fpa2bv_to_bv_out_of_range", out_of_range);
+    dbg_decouple("fpa2bv_to_bv_in_range", in_range);
 
     expr_ref rounded(m);
     rounded = m_bv_util.mk_extract(bv_sz-1, 0, pre_rounded);
     dbg_decouple("fpa2bv_to_bv_rounded", rounded);
 
-    result = m.mk_ite(out_of_range, unspec_v, rounded);
+    result = m.mk_ite(m.mk_not(in_range), unspec_v, rounded);
     result = m.mk_ite(c2, v2, result);
     result = m.mk_ite(c1, v1, result);
 
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 6c7190ebc..3e30faa6d 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -854,13 +854,11 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
     scoped_mpf v(m_fm);
 
     if (m_util.is_numeral(arg, v)) {
-        if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) {
+        if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
             if (m_hi_fp_unspecified) {
                 result = m_util.arith_util().mk_numeral(rational(0), false);
                 return BR_DONE;
             }
-            else
-                return BR_FAILED;
         }
         else {
             scoped_mpq r(m_fm.mpq_manager());
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 7287b69cf..5e7233110 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -1217,12 +1217,18 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
         default: UNREACHABLE();
         }
         if (inc) m_mpz_manager.inc(z);
+        TRACE("mpf_dbg_sbv",
+              tout << "SBV: (" << to_string(x) << ") == " << m_mpq_manager.to_string(z) << std::endl;
+              tout << "sign=" << t.sign() << " last=" << last << " round=" << round <<
+                  " sticky=" << sticky << " inc=" << inc << std::endl; );
     }
     else
         m_mpz_manager.mul2k(z, (unsigned) e);
 
     m_mpq_manager.set(o, z);
     if (x.sign) m_mpq_manager.neg(o);
+
+    TRACE("mpf_dbg", tout << "SBV = " << m_mpq_manager.to_string(o) << std::endl;);
 }
 
 void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
@@ -1248,6 +1254,8 @@ void mpf_manager::to_ieee_bv_mpz(const mpf & x, scoped_mpz & o) {
         m_mpz_manager.mul2k(o, sbits - 1);
         m_mpz_manager.add(o, sig(x), o);
     }
+
+    TRACE("mpf_dbg", tout << "IEEE_BV = " << m_mpz_manager.to_string(o) << std::endl;);
 }
 
 void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, mpz & sig) {