diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 8d012ca9b..b96874667 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -207,90 +207,76 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
     mk_fp(sgn, e, s, result);
 }
 
+void fpa2bv_converter::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result) {
+    if (m_util.is_float(rng)) {
+        unsigned ebits = m_util.get_ebits(rng);
+        unsigned sbits = m_util.get_sbits(rng);
+        unsigned bv_sz = ebits + sbits;
+
+        app_ref na(m);
+        na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+        mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
+              m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
+              m_bv_util.mk_extract(sbits - 2, 0, na),
+              result);
+    }
+    else
+        result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+}
+
 void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
 {
-    TRACE("fpa2bv_dbg", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
+    TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
     SASSERT(f->get_arity() == num);
 
     expr_ref_buffer new_args(m);
 
-    for (unsigned i = 0; i < num ; i ++)
-        if (is_float(args[i]))
-        {
-            expr * sgn, * sig, * exp;
+    for (unsigned i = 0; i < num; i++) {
+        if (is_float(args[i])) {
+            expr * sgn, *exp, *sig;
             split_fp(args[i], sgn, exp, sig);
-            new_args.push_back(sgn);
-            new_args.push_back(sig);
-            new_args.push_back(exp);
+            expr * args[3] = { sgn, exp, sig };
+            new_args.push_back(m_bv_util.mk_concat(3, args));
         }
         else
             new_args.push_back(args[i]);
+    }
 
     func_decl * fd;    
-    func_decl_triple fd3;
-    if (m_uf2bvuf.find(f, fd)) {
-        result = m.mk_app(fd, new_args.size(), new_args.c_ptr());
-    }
-    else if (m_uf23bvuf.find(f, fd3))
-    {
-        expr_ref a_sgn(m), a_sig(m), a_exp(m);
-        a_sgn = m.mk_app(fd3.f_sgn, new_args.size(), new_args.c_ptr());
-        a_sig = m.mk_app(fd3.f_sig, new_args.size(), new_args.c_ptr());
-        a_exp = m.mk_app(fd3.f_exp, new_args.size(), new_args.c_ptr());            
-        mk_fp(a_sgn, a_exp, a_sig, result);
-    }
+    if (m_uf2bvuf.find(f, fd))
+        mk_uninterpreted_output(f->get_range(), fd, new_args, result);
     else {
         sort_ref_buffer new_domain(m);
-    
-        for (unsigned i = 0; i < f->get_arity() ; i ++)
-            if (is_float(f->get_domain()[i]))
-            {
-                new_domain.push_back(m_bv_util.mk_sort(1));            
-                new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(f->get_domain()[i])-1));
-                new_domain.push_back(m_bv_util.mk_sort(m_util.get_ebits(f->get_domain()[i])));                                
-            }
+
+        for (unsigned i = 0; i < f->get_arity(); i++) {
+            sort * di = f->get_domain()[i];
+            if (is_float(di))
+                new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(di) + m_util.get_ebits(di)));
+            else if (is_rm(di))
+                new_domain.push_back(m_bv_util.mk_sort(3));
             else
-                new_domain.push_back(f->get_domain()[i]);
-
-        if (!is_float(f->get_range()))
-        {            
-            func_decl_ref fbv(m);
-            fbv = (f->get_info()) ? m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range(), *f->get_info()) :
-                                    m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range());
-            TRACE("fpa2bv_dbg", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl; );
-            m_uf2bvuf.insert(f, fbv);
-            m.inc_ref(f);
-            m.inc_ref(fbv);
-            result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+                new_domain.push_back(di);
         }
-        else
-        {
-            string_buffer<> name_buffer;
-            name_buffer.reset(); name_buffer << f->get_name() << ".sgn";        
-            func_decl * f_sgn = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(1));
-            name_buffer.reset(); name_buffer << f->get_name() << ".sig";
-            func_decl * f_sig = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_sbits(f->get_range())-1));
-            name_buffer.reset(); name_buffer << f->get_name() << ".exp";
-            func_decl * f_exp = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_ebits(f->get_range())));
 
-            expr_ref a_sgn(m), a_sig(m), a_exp(m);
-            a_sgn = m.mk_app(f_sgn, new_args.size(), new_args.c_ptr());
-            a_sig = m.mk_app(f_sig, new_args.size(), new_args.c_ptr());
-            a_exp = m.mk_app(f_exp, new_args.size(), new_args.c_ptr());            
-            TRACE("fpa2bv_dbg", tout << "New UF func_decls : " << std::endl;
-                                tout << mk_ismt2_pp(f_sgn, m) << std::endl;
-                                tout << mk_ismt2_pp(f_sig, m) << std::endl;
-                                tout << mk_ismt2_pp(f_exp, m) << std::endl; );
-            m_uf23bvuf.insert(f, func_decl_triple(f_sgn, f_sig, f_exp));
-            m.inc_ref(f);
-            m.inc_ref(f_sgn);
-            m.inc_ref(f_sig);
-            m.inc_ref(f_exp);
-            mk_fp(a_sgn, a_exp, a_sig, result);
-        }               
-    }    
+        sort * orig_rng = f->get_range();
+        sort_ref rng(orig_rng, m);
+        if (m_util.is_float(orig_rng))
+            rng = m_bv_util.mk_sort(m_util.get_ebits(orig_rng) + m_util.get_sbits(orig_rng));
+        else if (m_util.is_rm(orig_rng))
+            rng = m_bv_util.mk_sort(3);
 
-    TRACE("fpa2bv_dbg", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
+        func_decl_ref fbv(m);
+        fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), rng);
+        TRACE("fpa2bv", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl;);
+
+        m_uf2bvuf.insert(f, fbv);
+        m.inc_ref(f);
+        m.inc_ref(fbv);
+
+        mk_uninterpreted_output(f->get_range(), fbv, new_args, result);        
+    }
+
+    TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
 
     SASSERT(is_well_sorted(m, result));
 }
@@ -3709,15 +3695,5 @@ void fpa2bv_converter::reset(void) {
     dec_ref_map_key_values(m, m_rm_const2bv);
     dec_ref_map_key_values(m, m_uf2bvuf);
 
-    obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-    obj_map<func_decl, func_decl_triple>::iterator end = m_uf23bvuf.end();
-    for (; it != end; ++it) {
-        m.dec_ref(it->m_key);
-        m.dec_ref(it->m_value.f_sgn);
-        m.dec_ref(it->m_value.f_sig);
-        m.dec_ref(it->m_value.f_exp);
-    }
-    m_uf23bvuf.reset();
-
     m_extra_assertions.reset();
 }
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 7127c9b69..b91ced404 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -55,8 +55,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_map<func_decl, func_decl_triple>  m_uf23bvuf;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;    
     
 public:
     fpa2bv_converter(ast_manager & m);    
@@ -143,8 +142,7 @@ public:
 
     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; }
-    obj_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; }
+    obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }    
 
     void reset(void);
 
@@ -189,6 +187,8 @@ protected:
     app * mk_fresh_const(char const * prefix, unsigned sz);
 
     void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result);
+
+    void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result);
 };
 
 #endif
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index b77026eae..7d0f4d06b 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -91,7 +91,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
         if (m().is_eq(f)) {
             SASSERT(num == 2);
-            SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
+            TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << 
+                                                mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
+            SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));            
             sort * ds = f->get_domain()[0];
             if (m_conv.is_float(ds)) {
                 m_conv.mk_eq(args[0], args[1], result);
@@ -178,13 +180,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
         if (f->get_family_id() != 0 && f->get_family_id() != m_conv.fu().get_family_id())
         {
-            bool is_float_uf = m_conv.is_float(f->get_range());
-            unsigned i = 0;
-            while (!is_float_uf && i < num)
-            {
-                is_float_uf = m_conv.is_float(f->get_domain()[i]);
-                i++;
-            }
+            bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
+            
+            for (unsigned i = 0; i < num; i++)
+                is_float_uf |= m_conv.is_float(f->get_domain()[i]) || m_conv.is_rm(f->get_domain()[i]);
 
             if (is_float_uf)
             {
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index c4407a011..053cd36ae 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -84,37 +84,69 @@ namespace smt {
     void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
         SASSERT(f->get_family_id() != m_th.get_family_id());
         SASSERT(f->get_arity() == num);
-
+        
         expr_ref_buffer new_args(m);
 
         for (unsigned i = 0; i < num; i++)
             if (is_float(args[i]) || is_rm(args[i])) {
-                expr_ref unwrapped(m);
-                unwrapped = m_th.unwrap(m_th.wrap(args[i]), m.get_sort(args[i]));
-                new_args.push_back(unwrapped);
+                expr_ref wrapped(m);
+                wrapped = m_th.wrap(args[i]);
+                new_args.push_back(wrapped);
             }
             else
                 new_args.push_back(args[i]);
 
-        if (is_float(f->get_range())) {
-            sort * s = f->get_range();
-            unsigned ebits = m_th.m_fpa_util.get_ebits(s);
-            unsigned sbits = m_th.m_fpa_util.get_sbits(s);
-            unsigned bv_sz = ebits + sbits;
+        func_decl * fd;
+        func_decl_triple fd3;
+        if (m_uf2bvuf.find(f, fd)) {
+            result = m.mk_app(fd, new_args.size(), new_args.c_ptr());
+        }
+        else {
 
-            expr_ref bv(m);
-            bv = m_th.wrap(m.mk_app(f, num, new_args.c_ptr()));
-            m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
-                                   m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
-                                   m_bv_util.mk_extract(sbits - 2, 0, bv),
-                                   result);
+            sort_ref_buffer new_domain(m);
+
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                sort * di = f->get_domain()[i];
+                if (is_float(di)) {
+                    unsigned ebits = m_th.m_fpa_util.get_ebits(di);
+                    unsigned sbits = m_th.m_fpa_util.get_sbits(di);
+                    unsigned bv_sz = ebits + sbits;
+                    new_domain.push_back(m_bv_util.mk_sort(bv_sz));
+                }
+                else
+                    new_domain.push_back(di);
+            }
+
+
+            if (!is_float(f->get_range())) {
+                func_decl_ref fbv(m);
+                fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), f->get_range());
+                TRACE("t_fpa_detail", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl;);
+                m_uf2bvuf.insert(f, fbv);
+                m.inc_ref(f);
+                result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+            }
+            else {
+                sort * s = f->get_range();
+                unsigned ebits = m_th.m_fpa_util.get_ebits(s);
+                unsigned sbits = m_th.m_fpa_util.get_sbits(s);
+                unsigned bv_sz = ebits + sbits;
+
+                func_decl * f_sgn = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(1));
+                func_decl * f_exp = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(ebits));
+                func_decl * f_sig = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(sbits-1));                
+
+                expr_ref a_sgn(m), a_sig(m), a_exp(m);
+                a_sgn = m.mk_app(f_sgn, new_args.size(), new_args.c_ptr());                
+                a_exp = m.mk_app(f_exp, new_args.size(), new_args.c_ptr());
+                a_sig = m.mk_app(f_sig, new_args.size(), new_args.c_ptr());
+
+
+                m_th.m_converter.mk_fp(a_sgn, a_exp, a_sig, result);
+            }
         }
-        else if (is_rm(f->get_range())) {
-            func_decl_ref bv_f(m);
-            result = m_th.wrap(m.mk_app(f, num, new_args.c_ptr()));
-        }
-        else
-            result = m.mk_app(f, num, new_args.c_ptr());
+
+        TRACE("t_fpa_detail", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl;);
     }
 
     theory_fpa::theory_fpa(ast_manager & m) :
@@ -315,8 +347,7 @@ namespace smt {
         m_rw(e, e_conv);
         
         if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
-            app * a = to_app(e_conv);
-            m_converter.mk_uninterpreted_function(a->get_decl(), a->get_num_args(), a->get_args(), res);
+            m_th_rw(e_conv, res);
         }
         else if (m_fpa_util.is_rm(e)) {
             SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
@@ -578,6 +609,9 @@ namespace smt {
         xc = convert(xe);
         yc = convert(ye);
 
+        TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl <<
+                                      "yc = " << mk_ismt2_pp(yc, m) << std::endl;);
+
         expr_ref c(m);
 
         if (fu.is_float(xe) && fu.is_float(ye))
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index 5c12cbd8f..f0b745764 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -44,18 +44,7 @@ void fpa2bv_model_converter::display(std::ostream & out) {
         out << "\n  (" << n << " ";
         unsigned indent = n.size() + 4;
         out << mk_ismt2_pp(it->m_value, m, indent) << ")";
-    }
-    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-         it != m_uf23bvuf.end();
-         it++) {
-        const symbol & n = it->m_key->get_name();
-        out << "\n  (" << n << " ";
-        unsigned indent = n.size() + 4;
-        out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " <<
-            mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
-            mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
-            ")";
-    }
+    }    
     out << ")" << std::endl;
 }
 
@@ -84,10 +73,111 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
     return res;
 }
 
+expr_ref fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const {
+    fpa_util fu(m);
+    bv_util bu(m);
+    unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
+    unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
+
+    expr_ref res(m);
+    mpf fp_val;
+
+    unsigned ebits = fu.get_ebits(s);
+    unsigned sbits = fu.get_sbits(s);
+
+    unsigned sgn_sz = 1;
+    unsigned exp_sz = ebits;
+    unsigned sig_sz = sbits - 1;
+
+    rational sgn_q(0), sig_q(0), exp_q(0);
+
+    if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
+    if (exp) bu.is_numeral(exp, exp_q, exp_sz);
+    if (sig) bu.is_numeral(sig, sig_q, sig_sz);
+
+    // un-bias exponent
+    rational exp_unbiased_q;
+    exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits - 1);
+
+    mpz sig_z; mpf_exp_t exp_z;
+    mpzm.set(sig_z, sig_q.to_mpq().numerator());
+    exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
+
+    fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
+
+    mpzm.del(sig_z);
+
+    res = fu.mk_value(fp_val);
+
+    TRACE("fpa2bv_mc", tout << "[" << mk_ismt2_pp(sgn, m) << 
+                               " " << mk_ismt2_pp(exp, m) << 
+                               " " << mk_ismt2_pp(sig, m) << "] == " << 
+                               mk_ismt2_pp(res, m) << std::endl;);
+
+    return res;
+}
+
+expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * bv) const {    
+    fpa_util fu(m);
+    bv_util bu(m);
+
+    SASSERT(bu.is_bv(bv));
+
+    unsigned ebits = fu.get_ebits(s);
+    unsigned sbits = fu.get_sbits(s);
+    unsigned bv_sz = sbits + ebits;
+
+    expr_ref sgn(m), exp(m), sig(m);
+    sgn = bu.mk_extract(bv_sz - 1, bv_sz - 1, bv);
+    exp = bu.mk_extract(bv_sz - 2, sbits - 1, bv);
+    sig = bu.mk_extract(sbits - 2, 0, bv);
+
+    expr_ref v_sgn(m), v_exp(m), v_sig(m);
+    bv_mdl->eval(sgn, v_sgn);
+    bv_mdl->eval(exp, v_exp);
+    bv_mdl->eval(sig, v_sig);
+
+    return convert_bv2fp(s, v_sgn, v_exp, v_sig);
+}
+
+expr_ref fpa2bv_model_converter::convert_bv2rm(expr * eval_v) const {
+    fpa_util fu(m);
+    bv_util bu(m);
+    expr_ref res(m);   
+    rational bv_val(0);
+    unsigned sz = 0;
+
+    if (bu.is_numeral(eval_v, bv_val, sz)) {
+        SASSERT(bv_val.is_uint64());
+        switch (bv_val.get_uint64()) {
+        case BV_RM_TIES_TO_AWAY: res = fu.mk_round_nearest_ties_to_away(); break;
+        case BV_RM_TIES_TO_EVEN: res = fu.mk_round_nearest_ties_to_even(); break;
+        case BV_RM_TO_NEGATIVE: res = fu.mk_round_toward_negative(); break;
+        case BV_RM_TO_POSITIVE: res = fu.mk_round_toward_positive(); break;
+        case BV_RM_TO_ZERO:
+        default: res = fu.mk_round_toward_zero();
+        }
+    }
+
+    return res;
+}
+
+expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var, expr * val) const {
+    fpa_util fu(m);
+    bv_util bu(m);
+    expr_ref res(m);
+
+    expr_ref eval_v(m);        
+
+    if (val && bv_mdl->eval(val, eval_v, true))
+        res = convert_bv2rm(eval_v);
+
+    return res;
+}
+
 void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     fpa_util fu(m);
     bv_util bu(m);
-    mpf fp_val;
     unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
     unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
 
@@ -104,27 +194,24 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
          it++)
     {
         func_decl * var = it->m_key;
-        app * a = to_app(it->m_value);
+        app * val = to_app(it->m_value);
         SASSERT(fu.is_float(var->get_range()));
         SASSERT(var->get_range()->get_num_parameters() == 2);
 
-        unsigned ebits = fu.get_ebits(var->get_range());
-        unsigned sbits = fu.get_sbits(var->get_range());
-
         expr_ref sgn(m), sig(m), exp(m);        
-        bv_mdl->eval(a->get_arg(0), sgn, true);        
-        bv_mdl->eval(a->get_arg(1), exp, true);
-        bv_mdl->eval(a->get_arg(2), sig, true);
+        bv_mdl->eval(val->get_arg(0), sgn, true);
+        bv_mdl->eval(val->get_arg(1), exp, true);
+        bv_mdl->eval(val->get_arg(2), sig, true);
 
-        SASSERT(a->is_app_of(fu.get_family_id(), OP_FPA_FP));
+        SASSERT(val->is_app_of(fu.get_family_id(), OP_FPA_FP));
 
-#ifdef Z3DEBUG                
-        SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0);
-        SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0);
-        SASSERT(to_app(a->get_arg(2))->get_decl()->get_arity() == 0);        
-        seen.insert(to_app(a->get_arg(0))->get_decl());
-        seen.insert(to_app(a->get_arg(1))->get_decl());
-        seen.insert(to_app(a->get_arg(2))->get_decl());
+#ifdef Z3DEBUG
+        SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
+        SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
+        SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
+        seen.insert(to_app(val->get_arg(0))->get_decl());
+        seen.insert(to_app(val->get_arg(1))->get_decl());
+        seen.insert(to_app(val->get_arg(2))->get_decl());
 #else        
         SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
         SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
@@ -134,32 +221,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         if (!sgn && !sig && !exp)
             continue;
 
-        unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));        
-        unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(1)));
-        unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(2))) - 1;
+        expr_ref cv(m);
+        cv = convert_bv2fp(var->get_range(), sgn, exp, sig);
+        float_mdl->register_decl(var, cv);
 
-        rational sgn_q(0), sig_q(0), exp_q(0);
-
-        if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
-        if (sig) bu.is_numeral(sig, sig_q, sig_sz);
-        if (exp) bu.is_numeral(exp, exp_q, exp_sz);
-
-        // un-bias exponent
-        rational exp_unbiased_q;
-        exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits - 1);
-
-        mpz sig_z; mpf_exp_t exp_z;
-        mpzm.set(sig_z, sig_q.to_mpq().numerator());
-        exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
-
-        TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " <<
-              mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl;);
-
-        fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
-
-        float_mdl->register_decl(var, fu.mk_value(fp_val));
-
-        mpzm.del(sig_z);
+        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;);
     }
 
     for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
@@ -167,44 +233,69 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
          it++)
     {
         func_decl * var = it->m_key;
-        expr * v = it->m_value;
-        expr_ref eval_v(m);
         SASSERT(fu.is_rm(var->get_range()));
-        rational bv_val(0);
-        unsigned sz = 0;
-        if (v && bv_mdl->eval(v, eval_v, true) && bu.is_numeral(eval_v, bv_val, sz)) {
-            TRACE("fpa2bv_mc", tout << var->get_name() << " == " << bv_val.to_string() << std::endl;);
-            SASSERT(bv_val.is_uint64());
-            switch (bv_val.get_uint64())
-            {
-            case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
-            case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
-            case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
-            case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
-            case BV_RM_TO_ZERO:
-            default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
-            }
-            SASSERT(v->get_kind() == AST_APP);
-            seen.insert(to_app(v)->get_decl());
-        }
+        expr * val = it->m_value;
+        expr_ref fv(m);
+        fv = convert_bv2rm(bv_mdl, var, val);
+        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
+        float_mdl->register_decl(var, fv);
+        seen.insert(to_app(val)->get_decl());
     }
 
     for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
          it != m_uf2bvuf.end();
-         it++)
-         seen.insert(it->m_value);
+         it++) {
+        seen.insert(it->m_value);
 
-    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-         it != m_uf23bvuf.end();
-         it++)
-    {
-        seen.insert(it->m_value.f_sgn);
-        seen.insert(it->m_value.f_sig);
-        seen.insert(it->m_value.f_exp);
+        func_decl * f = it->m_key;
+        unsigned arity = f->get_arity();
+        sort * rng = f->get_range();
+        func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
+
+        func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value);
+        SASSERT(bv_fi->args_are_values());
+
+        for (unsigned i = 0; i < bv_fi->num_entries(); i++) {
+            func_entry const * bv_fe = bv_fi->get_entry(i);
+            expr * const * bv_args = bv_fe->get_args();
+            expr_ref_buffer new_args(m);
+
+            for (unsigned j = 0; j < arity; j++) {
+                sort * dj = f->get_domain(j);
+                expr * aj = bv_args[j];
+                if (fu.is_float(dj))
+                    new_args.push_back(convert_bv2fp(bv_mdl, dj, aj));
+                else if (fu.is_rm(dj)) {
+                    expr_ref fv(m);
+                    fv = convert_bv2rm(aj);
+                    new_args.push_back(fv);
+                }
+                else
+                    new_args.push_back(aj);
+            }
+            
+            expr_ref ret(m);
+            ret = bv_fe->get_result();
+            if (fu.is_float(rng))
+                ret = convert_bv2fp(bv_mdl, rng, ret);
+            else if (fu.is_rm(rng))
+                ret = convert_bv2rm(ret);
+
+            flt_fi->insert_new_entry(new_args.c_ptr(), ret);            
+        }
+
+        expr_ref els(m);
+        els = bv_fi->get_else();
+        if (fu.is_float(rng))
+            els = convert_bv2fp(bv_mdl, rng, els);
+        else if (fu.is_rm(rng))
+            els = convert_bv2rm(els);
+
+        flt_fi->set_else(els);
+
+        float_mdl->register_decl(f, flt_fi);        
     }
 
-    fu.fm().del(fp_val);
-
     // Keep all the non-float constants.
     unsigned sz = bv_mdl->get_num_constants();
     for (unsigned i = 0; i < sz; i++)
@@ -239,7 +330,6 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 model_converter * mk_fpa2bv_model_converter(ast_manager & m,
                                             obj_map<func_decl, expr*> const & const2bv,
                                             obj_map<func_decl, expr*> const & rm_const2bv,
-                                            obj_map<func_decl, func_decl*> const & uf2bvuf,
-                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
-    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf) {
+    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf);
 }
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index f36e8e068..021538ac1 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/src/tactic/fpa/fpa2bv_model_converter.h
@@ -27,13 +27,11 @@ class fpa2bv_model_converter : public model_converter {
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
     obj_map<func_decl, func_decl*>  m_uf2bvuf;
-    obj_map<func_decl, func_decl_triple>  m_uf23bvuf;
 
 public:
     fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
                            obj_map<func_decl, expr*> const & rm_const2bv,
-                           obj_map<func_decl, func_decl*> const & uf2bvuf,
-                           obj_map<func_decl, func_decl_triple> const & uf23bvuf) :
+                           obj_map<func_decl, func_decl*> const & uf2bvuf) :
                            m(m) {
         // Just create a copy?
         for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
@@ -60,32 +58,12 @@ public:
             m.inc_ref(it->m_key);
             m.inc_ref(it->m_value);
         }
-        for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
-             it != uf23bvuf.end();
-             it++)
-        {
-            m_uf23bvuf.insert(it->m_key, it->m_value);
-            m.inc_ref(it->m_key);
-            m.inc_ref(it->m_value.f_sgn);
-            m.inc_ref(it->m_value.f_sig);
-            m.inc_ref(it->m_value.f_exp);
-        }
     }
 
     virtual ~fpa2bv_model_converter() {
         dec_ref_map_key_values(m, m_const2bv);
         dec_ref_map_key_values(m, m_rm_const2bv);
         dec_ref_map_key_values(m, m_uf2bvuf);
-
-        obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
-        obj_map<func_decl, func_decl_triple>::iterator end = m_uf23bvuf.end();
-        for (; it != end; ++it) {
-            m.dec_ref(it->m_key);
-            m.dec_ref(it->m_value.f_sgn);
-            m.dec_ref(it->m_value.f_sig);
-            m.dec_ref(it->m_value.f_exp);
-        }
-        m_uf23bvuf.reset();
     }
 
     virtual void operator()(model_ref & md, unsigned goal_idx) {
@@ -108,13 +86,16 @@ protected:
     fpa2bv_model_converter(ast_manager & m) : m(m) { }
 
     void convert(model * bv_mdl, model * float_mdl);
+    expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const;
+    expr_ref convert_bv2fp(model * bv_mdl, sort * s, expr * bv) const;
+    expr_ref convert_bv2rm(expr * eval_v) const;
+    expr_ref convert_bv2rm(model * bv_mdl, func_decl * var, expr * val) const;
 };
 
 
 model_converter * mk_fpa2bv_model_converter(ast_manager & m,
                                             obj_map<func_decl, expr*> const & const2bv,
                                             obj_map<func_decl, expr*> const & rm_const2bv,
-                                            obj_map<func_decl, func_decl*> const & uf2bvuf,
-                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf);
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf);
 
 #endif
\ No newline at end of file
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 9149f1b9a..07669f513 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -107,7 +107,7 @@ class fpa2bv_tactic : public tactic {
             }
 
             if (g->models_enabled())  
-                mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.uf23bvuf());
+                mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf());
 
             g->inc_depth();
             result.push_back(g.get());