Bugfixes for unspecified results from fp.to_* (models are still incomplete).

Relates to #507

src/ast/fpa/fpa2bv_converter.cpp

@@ -2647,8 +2647,8 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;);
 
     result = m.mk_ite(x_is_zero, zero, res);
-    result = m.mk_ite(x_is_inf, mk_to_real_unspecified(), result);
+    result = m.mk_ite(x_is_inf, mk_to_real_unspecified(ebits, sbits), result);
-    result = m.mk_ite(x_is_nan, mk_to_real_unspecified(), result);
+    result = m.mk_ite(x_is_nan, mk_to_real_unspecified(ebits, sbits), result);
 
     SASSERT(is_well_sorted(m, result));
 }
@@ -2925,13 +2925,6 @@ 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);
@@ -2941,17 +2934,31 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     mk_is_nan(x, x_is_nan);
 
     sort * fp_srt = m.get_sort(x);
+    unsigned ebits = m_util.get_ebits(fp_srt);
     unsigned sbits = m_util.get_sbits(fp_srt);
 
-    expr_ref sig_unspec(s, m);
+    expr_ref nanv(m);
-    if (sbits > 2)
+    if (m_hi_fp_unspecified)
-        sig_unspec = m_bv_util.mk_concat(
+        // The "hardware interpretation" is 01...10...01.
-            mk_to_ieee_bv_unspecified(sbits - 2),
+        nanv = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
-            m_bv_util.mk_numeral(1, 1));
+               m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
-    else
+               m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
-        sig_unspec = m_bv_util.mk_numeral(1, 1);
+                                   m_bv_util.mk_numeral(1, 1))));
+    else {
+        app_ref unspec(m), mask(m);
+        unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
+        m_unspecified_ufs.insert_if_not_there(unspec->get_decl());
+        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] = { unspec, mask };
+        nanv = m_bv_util.mk_bv_or(2, args);
+    }
 
-    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), m.mk_ite(x_is_nan, sig_unspec, s));
+    result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s));
+
+    SASSERT(is_well_sorted(m, result));
 }
 
 void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
@@ -2987,7 +2994,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
         c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero)));
     else
         c1 = m.mk_or(x_is_nan, x_is_inf);
-    v1 = mk_to_ubv_unspecified(bv_sz);
+    v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
     dbg_decouple("fpa2bv_to_bv_c1", c1);
 
     // +-Zero  -> 0
@@ -3086,8 +3093,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
 
     dbg_decouple("fpa2bv_to_bv_rnd", rnd);
 
-    result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rnd);
+    result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(ebits, sbits, bv_sz), rnd);
-    result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz));
+    result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(ebits, sbits, bv_sz));
     result = m.mk_ite(c2, v2, result);
     result = m.mk_ite(c1, v1, result);
 
@@ -3106,25 +3113,43 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     mk_to_bv(f, num, args, true, result);
 }
 
-expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) {
+expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
+    expr_ref result(m);
     if (m_hi_fp_unspecified)
-        return expr_ref(m_bv_util.mk_numeral(0, width), m);
+        result = m_bv_util.mk_numeral(0, width);
-    else
+    else {
-        return expr_ref(m_util.mk_internal_to_ubv_unspecified(width), m);
+        app_ref unspec(m);
+        unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
+        m_unspecified_ufs.insert_if_not_there(unspec->get_decl());
+        result = unspec;
+    }
+    return result;
 }
 
-expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned width) {
+expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
+    expr_ref result(m);
     if (m_hi_fp_unspecified)
-        return expr_ref(m_bv_util.mk_numeral(0, width), m);
+        result = m_bv_util.mk_numeral(0, width);
-    else
+    else {
-        return expr_ref(m_util.mk_internal_to_sbv_unspecified(width), m);
+        app_ref unspec(m);
+        unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
+        m_unspecified_ufs.insert_if_not_there(unspec->get_decl());
+        result = unspec;
+    }
+    return result;
 }
 
-expr_ref fpa2bv_converter::mk_to_real_unspecified() {
+expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) {
+    expr_ref result(m);
     if (m_hi_fp_unspecified)
-        return expr_ref(m_arith_util.mk_numeral(rational(0), false), m);
+        result = m_arith_util.mk_numeral(rational(0), false);
-    else
+    else {
-        return expr_ref(m_util.mk_internal_to_real_unspecified(), m);
+        app_ref unspec(m);
+        unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits);
+        m_unspecified_ufs.insert_if_not_there(unspec->get_decl());
+        result = unspec;
+    }
+    return result;
 }
 
 void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) {

src/ast/fpa/fpa2bv_converter.h

@@ -41,6 +41,7 @@ protected:
     obj_map<func_decl, expr*>  m_const2bv;
     obj_map<func_decl, expr*>  m_rm_const2bv;
     obj_map<func_decl, func_decl*>  m_uf2bvuf;
+    obj_hashtable<func_decl>   m_unspecified_ufs;
 
     obj_map<func_decl, std::pair<app *, app *> > m_specials;
 
@@ -134,10 +135,9 @@ public:
     void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
 
-    expr_ref mk_to_ubv_unspecified(unsigned width);
+    expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    expr_ref mk_to_sbv_unspecified(unsigned width);
+    expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    expr_ref mk_to_ieee_bv_unspecified(unsigned width);
+    expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
-    expr_ref mk_to_real_unspecified();
 
     void reset(void);
 

src/ast/fpa_decl_plugin.cpp

@@ -728,12 +728,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
     unsigned arity, sort * const * domain, sort * range) {
     if (arity != 0)
         m_manager->raise_exception("invalid number of arguments to fp.to_ubv_unspecified");
-    if (num_parameters != 1)
+    if (num_parameters != 3)
-        m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1");
+        m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3");
-    if (!parameters[0].is_int())
+    if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer");
+        m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers");
 
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
+    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
     return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
 }
 
@@ -742,11 +742,12 @@ func_decl * fpa_decl_plugin::mk_internal_to_sbv_unspecified(
     unsigned arity, sort * const * domain, sort * range) {
     if (arity != 0)
         m_manager->raise_exception("invalid number of arguments to fp.to_sbv_unspecified");
-    if (num_parameters != 1)
+    if (num_parameters != 3)
-        m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 1");
+        m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3");
-    if (!parameters[0].is_int())
+    if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting an integer");
+        m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers");
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
+
+    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, &parameters[2]);
     return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
 }
 
@@ -755,6 +756,10 @@ func_decl * fpa_decl_plugin::mk_internal_to_real_unspecified(
     unsigned arity, sort * const * domain, sort * range) {
     if (arity != 0)
         m_manager->raise_exception("invalid number of arguments to fp.to_real_unspecified");
+    if (num_parameters != 2)
+        m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2");
+    if (!parameters[0].is_int() || !parameters[1].is_int())
+        m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers");
     if (!is_sort_of(range, m_arith_fid, REAL_SORT))
         m_manager->raise_exception("sort mismatch, expected range of Real sort");
 
@@ -765,16 +770,15 @@ func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_unspecified(
     decl_kind k, unsigned num_parameters, parameter const * parameters,
     unsigned arity, sort * const * domain, sort * range) {
     if (arity != 0)
-        m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified");
+        m_manager->raise_exception("invalid number of arguments to to_ieee_bv_unspecified; expecting none");
-    if (num_parameters != 1)
+    if (num_parameters != 2)
-        m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 1");
+        m_manager->raise_exception("invalid number of parameters to to_ieee_bv_unspecified; expecting 2");
-    if (!parameters[0].is_int())
+    if (!parameters[0].is_int() || !parameters[1].is_int())
-        m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting an integer");
+        m_manager->raise_exception("invalid parameters type provided to to_ieee_bv_unspecified; expecting 2 integers");
-    if (!is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
 
-    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters);
+    parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) };
-    return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
+    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p);
+    return m_manager->mk_func_decl(symbol("to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
 }
 
 
@@ -1063,25 +1067,26 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) {
     return mk_value(v);
 }
 
-app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) {
+app * fpa_util::mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    parameter ps[] = { parameter(width) };
+    parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) };
     sort * range = m_bv_util.mk_sort(width);
-    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range);
+    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range);
 }
 
-app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) {
+app * fpa_util::mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) {
-    parameter ps[] = { parameter(width) };
+    parameter ps[] = { parameter(ebits), parameter(sbits), 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_SBV_UNSPECIFIED, 3, ps, 0, 0, range);
 }
 
-app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned width) {
+app * fpa_util::mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) {
-    parameter ps[] = { parameter(width) };
+    parameter ps[] = { parameter(ebits), parameter(sbits) };
-    sort * range = m_bv_util.mk_sort(width);
+    sort * range = m_bv_util.mk_sort(ebits+sbits);
-    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 1, ps, 0, 0, range);
+    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range);
 }
 
-app * fpa_util::mk_internal_to_real_unspecified() {
+app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits) {
+    parameter ps[] = { parameter(ebits), parameter(sbits) };
     sort * range = m_a_util.mk_real();
-    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range);
+    return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range);
 }

src/ast/fpa_decl_plugin.h

@@ -346,10 +346,10 @@ public:
 
     app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); }
 
-    app * mk_internal_to_ubv_unspecified(unsigned width);
+    app * mk_internal_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    app * mk_internal_to_sbv_unspecified(unsigned width);
+    app * mk_internal_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
-    app * mk_internal_to_ieee_bv_unspecified(unsigned width);
+    app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
-    app * mk_internal_to_real_unspecified();
+    app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits);
 
     bool is_wrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); }
     bool is_unwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVUNWRAP); }

src/ast/rewriter/fpa_rewriter.cpp

@@ -106,7 +106,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
         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;
+        SASSERT(num_args == 0); st = mk_to_real_unspecified(f, result); break;
     case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
         SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break;
 
@@ -122,61 +122,55 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 }
 
 br_status fpa_rewriter::mk_to_ubv_unspecified(func_decl * f, expr_ref & result) {
-    SASSERT(f->get_num_parameters() == 1);
+    SASSERT(f->get_num_parameters() == 3);
     SASSERT(f->get_parameter(0).is_int());
-    unsigned bv_sz = f->get_parameter(0).get_int();
+    SASSERT(f->get_parameter(1).is_int());
+    SASSERT(f->get_parameter(2).is_int());
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
+    unsigned width = f->get_parameter(2).get_int();
 
     bv_util bu(m());
     if (m_hi_fp_unspecified)
         // The "hardware interpretation" is 0.
-        result = bu.mk_numeral(0, bv_sz);
+        result = bu.mk_numeral(0, ebits+sbits);
     else
-        result = m_util.mk_internal_to_ubv_unspecified(bv_sz);
+        result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width);
 
     return BR_DONE;
 }
 
 br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) {
-    SASSERT(f->get_num_parameters() == 1);
+    SASSERT(f->get_num_parameters() == 3);
     SASSERT(f->get_parameter(0).is_int());
-    unsigned bv_sz = f->get_parameter(0).get_int();
+    SASSERT(f->get_parameter(1).is_int());
+    SASSERT(f->get_parameter(2).is_int());
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
+    unsigned width = f->get_parameter(2).get_int();
 
     bv_util bu(m());
     if (m_hi_fp_unspecified)
         // The "hardware interpretation" is 0.
-        result = bu.mk_numeral(0, bv_sz);
+        result = bu.mk_numeral(0, ebits+sbits);
     else
-        result = m_util.mk_internal_to_sbv_unspecified(bv_sz);
+        result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width);
 
     return BR_DONE;
 }
 
-br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) {
+br_status fpa_rewriter::mk_to_real_unspecified(func_decl * f, expr_ref & result) {
-    bv_util bu(m());
+    SASSERT(f->get_num_parameters() == 2);
-    unsigned bv_sz = bu.get_bv_size(f->get_range());
+    SASSERT(f->get_parameter(0).is_int());
+    SASSERT(f->get_parameter(1).is_int());
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
 
-    if (m_hi_fp_unspecified)
-        // The "hardware interpretation" is 0.
-        result = bu.mk_numeral(0, bv_sz);
-    else {
-        unsigned sbits = m_util.get_sbits(f->get_domain()[0]);
-
-        if (sbits > 2)
-            result = bu.mk_concat(m_util.mk_internal_to_ieee_bv_unspecified(sbits - 2),
-                                  bu.mk_numeral(1, 1));
-        else
-            result = bu.mk_numeral(1, 1);
-    }
-
-    return BR_DONE;
-}
-
-br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
     if (m_hi_fp_unspecified)
         // The "hardware interpretation" is 0.
         result = m_util.au().mk_numeral(rational(0), false);
     else
-        result = m_util.mk_internal_to_real_unspecified();
+        result = m_util.mk_internal_to_real_unspecified(ebits, sbits);
 
     return BR_DONE;
 }
@@ -865,20 +859,43 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
     return BR_FAILED;
 }
 
+br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) {
+    SASSERT(f->get_num_parameters() == 2);
+    SASSERT(f->get_parameter(0).is_int());
+    SASSERT(f->get_parameter(1).is_int());
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
+
+    bv_util bu(m());
+
+    if (m_hi_fp_unspecified)
+        // The "hardware interpretation" is 01...10...01.
+        result = bu.mk_concat(bu.mk_numeral(0, 1),
+                 bu.mk_concat(bu.mk_numeral(-1, ebits),
+                 bu.mk_concat(bu.mk_numeral(0, sbits - 2),
+                              bu.mk_numeral(1, 1))));
+    else
+        result = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits);
+
+    return BR_DONE;
+}
+
 br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) {
     scoped_mpf v(m_fm);
 
     if (m_util.is_numeral(arg, v)) {
+        bv_util bu(m());
+        const mpf & x = v.get();
 
         if (m_fm.is_nan(v)) {
-            mk_to_ieee_bv_unspecified(f, result);
+            result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits());
-            return BR_REWRITE_FULL;
+            return BR_REWRITE1;
         }
         else {
-            bv_util bu(m());
             scoped_mpz rz(m_fm.mpq_manager());
             m_fm.to_ieee_bv_mpz(v, rz);
-            result = bu.mk_numeral(rational(rz), v.get().get_ebits() + v.get().get_sbits());
+
+            result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits());
             return BR_DONE;
         }
     }
@@ -891,7 +908,8 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
 
     if (m_util.is_numeral(arg, v)) {
         if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
-            result = m_util.mk_internal_to_real_unspecified();
+            const mpf & x = v.get();
+            result = m_util.mk_internal_to_real_unspecified(x.get_ebits(), x.get_sbits());
         }
         else {
             scoped_mpq r(m_fm.mpq_manager());

src/ast/rewriter/fpa_rewriter.h

@@ -89,7 +89,7 @@ public:
     br_status mk_to_ubv_unspecified(func_decl * f, expr_ref & result);
     br_status mk_to_sbv_unspecified(func_decl * f, expr_ref & result);
     br_status mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result);
-    br_status mk_to_real_unspecified(expr_ref & result);
+    br_status mk_to_real_unspecified(func_decl * f, expr_ref & result);
 };
 
 #endif

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -54,6 +54,14 @@ void fpa2bv_model_converter::display(std::ostream & out) {
         out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " <<
                mk_ismt2_pp(it->m_value.second, m, indent) << ")";
     }
+    for (obj_hashtable<func_decl>::iterator it = m_unspecified_ufs.begin();
+         it != m_unspecified_ufs.end();
+         it++)
+    {
+        const symbol & n = (*it)->get_name();
+        unsigned indent = n.size() + 4;
+        out << n << " ";
+    }
     out << ")" << std::endl;
 }
 
@@ -99,6 +107,14 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
         translator.to().inc_ref(v1);
         translator.to().inc_ref(v2);
     }
+    for (obj_hashtable<func_decl>::iterator it = m_unspecified_ufs.begin();
+         it != m_unspecified_ufs.end();
+         it++)
+    {
+        func_decl * k = translator(*it);
+        res->m_unspecified_ufs.insert(k);
+        translator.to().inc_ref(k);
+    }
     return res;
 }
 
@@ -367,6 +383,22 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         float_mdl->register_decl(f, flt_fi);
     }
 
+    // fp.to_*_unspecified UFs.
+    for (obj_hashtable<func_decl>::iterator it = m_unspecified_ufs.begin();
+         it != m_unspecified_ufs.end();
+         it++)
+    {
+        func_decl * f = *it;
+
+        if (bv_mdl->has_interpretation(f)) {
+            func_interp * val = bv_mdl->get_func_interp(f)->copy();
+            TRACE("fpa2bv_mc", tout << "Keeping interpretation for " << mk_ismt2_pp(f, m) << std::endl;);
+            float_mdl->register_decl(f, val);
+        }
+        else
+            TRACE("fpa2bv_mc", tout << "No interpretation for " << mk_ismt2_pp(f, m) << std::endl;);
+    }
+
     // Keep all the non-float constants.
     unsigned sz = bv_mdl->get_num_constants();
     for (unsigned i = 0; i < sz; i++)

src/tactic/fpa/fpa2bv_model_converter.h

@@ -28,6 +28,7 @@ class fpa2bv_model_converter : public model_converter {
     obj_map<func_decl, expr*>   m_rm_const2bv;
     obj_map<func_decl, func_decl*>  m_uf2bvuf;
     obj_map<func_decl, std::pair<app*, app*> > m_specials;
+    obj_hashtable<func_decl>    m_unspecified_ufs;
 
 public:
     fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) {
@@ -63,6 +64,13 @@ public:
             m.inc_ref(it->m_value.first);
             m.inc_ref(it->m_value.second);
         }
+        for (obj_hashtable<func_decl>::iterator it = conv.m_unspecified_ufs.begin();
+             it != conv.m_unspecified_ufs.end();
+             it++)
+        {
+            m_unspecified_ufs.insert(*it);
+            m.inc_ref(*it);
+        }
     }
 
     virtual ~fpa2bv_model_converter() {
@@ -76,6 +84,7 @@ public:
             m.dec_ref(it->m_value.first);
             m.dec_ref(it->m_value.second);
         }
+        dec_ref_collection_values(m, m_unspecified_ufs);
     }
 
     virtual void operator()(model_ref & md, unsigned goal_idx) {