diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 51d33c896..8ef6fb557 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -109,7 +109,7 @@ public:
          parameters[o]            - (int) m - number of constructors
          parameters[o+1]          - (int) k_1 - offset for constructor definition
          ...
-         parameters[o+m]          - (int) k_m - offset ofr constructor definition
+         parameters[o+m]          - (int) k_m - offset for constructor definition
       
          for each offset k_i at parameters[o+s] for some s in 0..m-1
          parameters[k_i]          - (symbol) name of the constructor
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d5849a1fd..cda3bd27e 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -33,6 +33,9 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m_util(m),
     m_bv_util(m),
     m_arith_util(m),
+    m_array_util(m),
+    m_dt_util(m),
+    m_seq_util(m),
     m_mpf_manager(m_util.fm()),
     m_mpz_manager(m_mpf_manager.mpz_manager()),
     m_hi_fp_unspecified(true),
@@ -46,11 +49,10 @@ fpa2bv_converter::~fpa2bv_converter() {
 
 void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
     if (is_float(a) && is_float(b)) {
-        SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
-        SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
+        SASSERT(m_util.is_fp(a) && m_util.is_fp(b));
 
         TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
-        tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
+                        tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
 
         expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
         m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
@@ -77,11 +79,10 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
         m_simp.mk_or(both_are_nan, both_the_same, result);
     }
     else if (is_rm(a) && is_rm(b)) {
-        SASSERT(m_util.is_rm_bvwrap(b));
-        SASSERT(m_util.is_rm_bvwrap(a));
+        SASSERT(m_util.is_rm_bvwrap(b) && m_util.is_rm_bvwrap(a));
 
         TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
-        tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
+                        tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
 
         m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
     }
@@ -90,8 +91,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
-    SASSERT(is_app_of(t, m_plugin->get_family_id(), OP_FPA_FP));
-    SASSERT(is_app_of(f, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(t) && m_util.is_fp(f));
 
     expr *t_sgn, *t_sig, *t_exp;
     expr *f_sgn, *f_sig, *f_exp;
@@ -103,7 +103,7 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
     m_simp.mk_ite(c, t_sig, f_sig, s);
     m_simp.mk_ite(c, t_exp, f_exp, e);
 
-    mk_fp(sgn, e, s, result);
+    result = m_util.mk_fp(sgn, e, s);
 }
 
 void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -152,7 +152,7 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar
 
         mk_bias(e, biased_exp);
 
-        mk_fp(bv_sgn, biased_exp, bv_sig, result);
+        result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
         TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
             << mk_ismt2_pp(result, m) << std::endl;);
 
@@ -199,7 +199,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
         SASSERT(m_bv_util.get_bv_size(e) == ebits);
 #endif
 
-        mk_fp(sgn, e, s, result);
+        result = m_util.mk_fp(sgn, e, s);
 
         m_const2bv.insert(f, result);
         m.inc_ref(f);
@@ -218,7 +218,7 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
     s = m.mk_var(base_inx+1, m_bv_util.mk_sort(sbits-1));
     e = m.mk_var(base_inx+2, m_bv_util.mk_sort(ebits));
 
-    mk_fp(sgn, e, s, result);
+    result = m_util.mk_fp(sgn, e, s);
 }
 
 void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result) {
@@ -229,176 +229,68 @@ void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * co
 
         app_ref na(m);
         na = m.mk_app(fbv, fbv->get_arity(), new_args);
-        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);
+        result = m_util.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));
     }
     else if (m_util.is_rm(rng)) {
         app_ref na(m);
         na = m.mk_app(fbv, fbv->get_arity(), new_args);
-        mk_rm(na, result);
+        result = m_util.mk_rm(na);
     }
     else
         result = m.mk_app(fbv, fbv->get_arity(), new_args);
 }
 
-sort_ref fpa2bv_converter::replace_float_sorts(sort * s) {
-    sort_ref ns(m);    
-
-    if (m_util.is_float(s))
-        ns = m_bv_util.mk_sort(m_util.get_sbits(s) + m_util.get_ebits(s));
-    else if (m_util.is_rm(s))
-        ns = m_bv_util.mk_sort(3);
-    else
-        ns = s;
-
-    if (ns->get_num_parameters() != 0) {
-        vector<parameter> new_params;
-        unsigned num_params = ns->get_num_parameters();
-        for (unsigned i = 0; i < num_params; i++)
-        {
-            parameter const & pi = ns->get_parameter(i);
-            if (pi.is_ast() && pi.get_ast()->get_kind() == AST_SORT) {
-                sort_ref nsrt(m);
-                nsrt = replace_float_sorts(to_sort(pi.get_ast()));
-                parameter np = parameter((ast*)nsrt);
-                new_params.push_back(np);
-            }
-            else
-                new_params.push_back(pi);
-        }
-
-        TRACE("fpa2bv", tout << "New sort params:";
-                        for (unsigned i = 0; i < new_params.size(); i++)
-                            tout << " " << new_params[i];
-                        tout << std::endl;);
-
-        ns = m.mk_sort(ns->get_family_id(), ns->get_decl_kind(), new_params.size(), new_params.c_ptr());
+func_decl * fpa2bv_converter::get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity) {
+    func_decl * res;
+    if (!m_uf2bvuf.find(f, res)) {
+        res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), arity, f->get_domain(), bv_rng);
+        m_uf2bvuf.insert(f, res);
+        m.inc_ref(f);
+        m.inc_ref(res);
+        TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
     }
-
-    TRACE("fpa2bv", tout << "sorts replaced: " << mk_ismt2_pp(s, m) << " --> " << mk_ismt2_pp(ns, m) << std::endl; );
-    return ns;
-}
-
-func_decl_ref fpa2bv_converter::replace_function(func_decl * f) {
-    TRACE("fpa2bv", tout << "replacing: " << mk_ismt2_pp(f, m) << std::endl;);
-    func_decl_ref res(m);
-
-    sort_ref_buffer new_domain(m);
-    for (unsigned i = 0; i < f->get_arity(); i++) {
-        sort * di = f->get_domain()[i];
-        new_domain.push_back(replace_float_sorts(di));
-    }
-
-    func_decl * fd;
-    if (m_uf2bvuf.find(f, fd))
-        res = fd;
-    else {
-        sort_ref new_range(m);
-        new_range = replace_float_sorts(f->get_range());
-
-        if (f->get_family_id() == null_family_id) {
-            res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), new_domain.size(), new_domain.c_ptr(), new_range);
-            TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
-
-            m_uf2bvuf.insert(f, res);
-            m.inc_ref(f);
-            m.inc_ref(res);
-        }
-        else
-        {
-            TRACE("fpa2bv", tout << "New domain:";
-                            for (unsigned i = 0; i < new_domain.size(); i++)
-                                tout << " " << mk_ismt2_pp(new_domain[i], m);
-                            tout << std::endl;);
-
-            res = m.mk_func_decl(f->get_family_id(), f->get_decl_kind(),
-                                 f->get_num_parameters(), f->get_parameters(),
-                                 new_domain.size(), new_domain.c_ptr(), new_range);
-            TRACE("fpa2bv", tout << "New IF func_decl: " << mk_ismt2_pp(res, m) << std::endl;);
-        }
-    }
-
     return res;
 }
-
-expr_ref fpa2bv_converter::replace_float_arg(expr * a) {
-    expr_ref na(m);
-
-    switch (a->get_kind()) {
-    case AST_APP:
-        if (m_util.is_float(a)) {
-            SASSERT(m_util.is_fp(a));
-            expr * sgn, *exp, *sig;
-            split_fp(a, sgn, exp, sig);
-            expr * args[3] = { sgn, exp, sig };
-            na = m_bv_util.mk_concat(3, args);
-        }
-        else if (is_rm(a)) {
-            SASSERT(m_util.is_rm_bvwrap(a));
-            na = to_app(a)->get_arg(0);
-        }
-        else if (m.is_value(a))
-            na = a;
-        else {            
-            sort_ref ns(m);
-            app_ref ar(m);
-            ar = to_app(a);
-            func_decl * f = to_app(ar)->get_decl();
-            func_decl_ref rf(m);
-            rf = replace_function(f);
-            na = m.mk_app(rf, ar->get_num_args(), ar->get_args());
-        }
-        break;
-    case AST_VAR:
-        na = m.mk_var(to_var(a)->get_idx(), replace_float_sorts(m.get_sort(a)));
-        break;
-    case AST_QUANTIFIER: {
-        quantifier * q = to_quantifier(a);
-        sort * const * srts = q->get_decl_sorts();
-        vector<sort*> new_sorts;
-        for (unsigned i = 0; q->get_num_decls(); i++) {
-            sort_ref ns(m);
-            ns = replace_float_sorts(q->get_decl_sort(i));
-            new_sorts.push_back(ns);
-        }
-        na = m.mk_quantifier(q->is_forall(), 
-                             q->get_num_decls(), new_sorts.c_ptr(),
-                             q->get_decl_names(), q->get_expr(),
-                             q->get_weight(), q->get_qid(), q->get_skid(), 
-                             q->get_num_patterns(), q->get_patterns(), 
-                             q->get_num_no_patterns(), q->get_no_patterns());
-        break;
-    }
-    case AST_SORT:
-    case AST_FUNC_DECL:
-    default:
-        UNREACHABLE();
-    }
-
-    TRACE("fpa2bv", tout << "arg replaced: " << mk_ismt2_pp(a, m) << " --> " << mk_ismt2_pp(na, m) << std::endl; );
-    return na;
-}
-
 void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
 {
     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++)
-        new_args.push_back(replace_float_arg(args[i]));
-
-    TRACE("fpa2bv", tout << "UF bv-args:";
-                    for (unsigned i = 0; i < num; i++)
-                        tout << " " << mk_ismt2_pp(new_args[i], m);
-                    tout << std::endl; );
-
-    func_decl_ref rf(m);
-    rf = replace_function(f);
-    mk_function_output(f->get_range(), rf, new_args.c_ptr(), result);
+    expr_ref fapp(m), feq(m);
+    sort_ref rng(m);
+    app_ref bv_app(m), flt_app(m);
+    rng = f->get_range();
+    fapp = m.mk_app(f, num, args);
+    if (m_util.is_float(rng)) {
+        sort_ref bv_rng(m);        
+        expr_ref new_eq(m);
+        unsigned ebits = m_util.get_ebits(rng);
+        unsigned sbits = m_util.get_sbits(rng);
+        unsigned bv_sz = ebits+sbits;
+        bv_rng = m_bv_util.mk_sort(bv_sz);
+        func_decl * bv_f = get_bv_uf(f, bv_rng, num);
+        bv_app = m.mk_app(bv_f, num, args);
+        flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app),
+                               m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app),
+                               m_bv_util.mk_extract(sbits-2, 0, bv_app));
+        new_eq = m.mk_eq(fapp, flt_app);
+        m_extra_assertions.push_back(new_eq);
+        result = flt_app;
+    }
+    else if (m_util.is_rm(rng)) {
+        sort_ref bv_rng(m);
+        expr_ref new_eq(m);
+        bv_rng = m_bv_util.mk_sort(3);
+        func_decl * bv_f = get_bv_uf(f, bv_rng, num);
+        bv_app = m.mk_app(bv_f, num, args);
+        flt_app = m_util.mk_rm(bv_app);
+        new_eq = m.mk_eq(fapp, flt_app);
+        m_extra_assertions.push_back(new_eq);
+        result = flt_app;
+    }
+    else 
+        result = fapp;
 
     TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
     SASSERT(is_well_sorted(m, result));
@@ -423,7 +315,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
 #endif
             , m_bv_util.mk_sort(3));
 
-        mk_rm(bv3, result);
+        result = m_util.mk_rm(bv3);
         m_rm_const2bv.insert(f, result);
         m.inc_ref(f);
         m.inc_ref(result);
@@ -444,10 +336,7 @@ void fpa2bv_converter::mk_pinf(sort * s, expr_ref & result) {
     unsigned ebits = m_util.get_ebits(s);
     expr_ref top_exp(m);
     mk_top_exp(ebits, top_exp);
-    mk_fp(m_bv_util.mk_numeral(0, 1),
-        top_exp,
-        m_bv_util.mk_numeral(0, sbits-1),
-        result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
 }
 
 void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
@@ -460,10 +349,7 @@ void fpa2bv_converter::mk_ninf(sort * s, expr_ref & result) {
     unsigned ebits = m_util.get_ebits(s);
     expr_ref top_exp(m);
     mk_top_exp(ebits, top_exp);
-    mk_fp(m_bv_util.mk_numeral(1, 1),
-        top_exp,
-        m_bv_util.mk_numeral(0, sbits-1),
-        result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), top_exp, m_bv_util.mk_numeral(0, sbits-1));
 }
 
 void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
@@ -476,10 +362,7 @@ void fpa2bv_converter::mk_nan(sort * s, expr_ref & result) {
     unsigned ebits = m_util.get_ebits(s);
     expr_ref top_exp(m);
     mk_top_exp(ebits, top_exp);
-    mk_fp(m_bv_util.mk_numeral(0, 1),
-        top_exp,
-        m_bv_util.mk_numeral(1, sbits - 1),
-        result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), top_exp, m_bv_util.mk_numeral(1, sbits - 1));
 }
 
 void fpa2bv_converter::mk_nzero(func_decl * f, expr_ref & result) {
@@ -492,10 +375,7 @@ void fpa2bv_converter::mk_nzero(sort * s, expr_ref & result) {
     unsigned ebits = m_util.get_ebits(s);
     expr_ref bot_exp(m);
     mk_bot_exp(ebits, bot_exp);
-    mk_fp(m_bv_util.mk_numeral(1, 1),
-        bot_exp,
-        m_bv_util.mk_numeral(0, sbits - 1),
-        result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(1, 1), bot_exp, m_bv_util.mk_numeral(0, sbits - 1));
 }
 
 void fpa2bv_converter::mk_pzero(func_decl * f, expr_ref & result) {
@@ -508,10 +388,7 @@ void fpa2bv_converter::mk_pzero(sort * s, expr_ref & result) {
     unsigned ebits = m_util.get_ebits(s);
     expr_ref bot_exp(m);
     mk_bot_exp(ebits, bot_exp);
-    mk_fp(m_bv_util.mk_numeral(0, 1),
-        bot_exp,
-        m_bv_util.mk_numeral(0, sbits-1),
-        result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), bot_exp, m_bv_util.mk_numeral(0, sbits-1));
 }
 
 void fpa2bv_converter::mk_zero(sort * s, expr_ref & sgn, expr_ref & result) {
@@ -530,10 +407,7 @@ void fpa2bv_converter::mk_one(sort * s, expr_ref & sign, expr_ref & result) {
     SASSERT(is_float(s));
     unsigned sbits = m_util.get_sbits(s);
     unsigned ebits = m_util.get_ebits(s);
-    mk_fp(sign,
-        m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
-        m_bv_util.mk_numeral(0, sbits-1),
-        result);
+    result = m_util.mk_fp(sign, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits), m_bv_util.mk_numeral(0, sbits-1));
 }
 
 void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
@@ -813,7 +687,7 @@ void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
     nsgn = m_bv_util.mk_bv_not(sgn);
     expr_ref r_sgn(m);
     m_simp.mk_ite(c, sgn, nsgn, r_sgn);
-    mk_fp(r_sgn, e, sig, result);
+    result = m_util.mk_fp(r_sgn, e, sig);
 }
 
 void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -1230,7 +1104,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
     SASSERT(num == 1);
     expr * sgn, * s, * e;
     split_fp(args[0], sgn, e, s);
-    mk_fp(m_bv_util.mk_numeral(0, 1), e, s, result);
+    result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), e, s);
 }
 
 void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -1301,14 +1175,8 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
     }
 
     expr_ref pn(m), np(m);
-    mk_fp(decls.first,
-        m_bv_util.mk_numeral(0, ebits),
-        m_bv_util.mk_numeral(0, sbits - 1),
-        pn);
-    mk_fp(decls.second,
-        m_bv_util.mk_numeral(0, ebits),
-        m_bv_util.mk_numeral(0, sbits - 1),
-        np);
+    pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
+    np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
 
     expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
     mk_is_pzero(x, x_is_pzero);
@@ -1388,14 +1256,8 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
     }
 
     expr_ref pn(m), np(m);
-    mk_fp(decls.first,
-        m_bv_util.mk_numeral(0, ebits),
-        m_bv_util.mk_numeral(0, sbits - 1),
-        pn);
-    mk_fp(decls.second,
-        m_bv_util.mk_numeral(0, ebits),
-        m_bv_util.mk_numeral(0, sbits - 1),
-        np);
+    pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
+    np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
 
     expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
     mk_is_pzero(x, x_is_pzero);
@@ -2286,10 +2148,9 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
         int sz = m_bv_util.get_bv_size(bv);
         SASSERT((unsigned)sz == to_sbits + to_ebits);
 
-        mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
-            m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
-            m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
-            result);
+        result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
+                              m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
+                              m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv));
     }
     else if (num == 2 &&
         m_util.is_rm(args[0]) &&
@@ -2318,7 +2179,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
         SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
         SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
         SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2])+1);
-        mk_fp(args[0], args[1], args[2], result);
+        result = m_util.mk_fp(args[0], args[1], args[2]);
     }
     else if (num == 3 &&
         m_util.is_rm(args[0]) &&
@@ -2545,7 +2406,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
             mk_bias(unbiased_exp, exp);
 
-            mk_fp(sgn, exp, sig, result);
+            result = m_util.mk_fp(sgn, exp, sig);
         }
     }
     else if (m_util.au().is_numeral(x)) {
@@ -2578,32 +2439,32 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
             sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
             mk_bias(unbiased_exp, exp);
-            mk_fp(sgn, exp, sig, v1);
+            v1 = m_util.mk_fp(sgn, exp, sig);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
             sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
             mk_bias(unbiased_exp, exp);
-            mk_fp(sgn, exp, sig, v2);
+            v2 = m_util.mk_fp(sgn, exp, sig);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
             sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
             mk_bias(unbiased_exp, exp);
-            mk_fp(sgn, exp, sig, v3);
+            v3 = m_util.mk_fp(sgn, exp, sig);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
             sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
             mk_bias(unbiased_exp, exp);
-            mk_fp(sgn, exp, sig, v4);
+            v4 = m_util.mk_fp(sgn, exp, sig);
 
             sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
             sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
             unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
             mk_bias(unbiased_exp, exp);
 
-            mk_fp(sgn, exp, sig, result);
+            result = m_util.mk_fp(sgn, exp, sig);
             mk_ite(rm_tn, v4, result, result);
             mk_ite(rm_tp, v3, result, result);
             mk_ite(rm_nte, v2, result, result);
@@ -3344,27 +3205,14 @@ expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sb
     return result;
 }
 
-void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) {
-    SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
-    result = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, m_util.mk_rm_sort());
-}
-
-void fpa2bv_converter::mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result) {
-    SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
-    SASSERT(m_bv_util.is_bv(significand));
-    SASSERT(m_bv_util.is_bv(exponent));
-    result = m.mk_app(m_util.get_family_id(), OP_FPA_FP, sign, exponent, significand);
-}
-
 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);
     SASSERT(m_util.get_sbits(f->get_range()) == m_bv_util.get_bv_size(args[2]) + 1);
     SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
-    mk_fp(args[0], args[1], args[2], result);
+    result = m_util.mk_fp(args[0], args[1], args[2]);
     TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;);
 }
-
 void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
     SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
@@ -3711,7 +3559,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
     default: UNREACHABLE();
     }
 
-    mk_rm(result, result);
+    result = m_util.mk_rm(result);
 }
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
@@ -4109,7 +3957,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
     SASSERT(is_well_sorted(m, res_exp));
 
-    mk_fp(res_sgn, res_exp, res_sig, result);
+    result = m_util.mk_fp(res_sgn, res_exp, res_sig);
 
     TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
 }
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 879c1e080..19c5b3352 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -24,6 +24,11 @@ Notes:
 #include"ref_util.h"
 #include"fpa_decl_plugin.h"
 #include"bv_decl_plugin.h"
+#include"array_decl_plugin.h"
+#include"datatype_decl_plugin.h"
+#include"dl_decl_plugin.h"
+#include"pb_decl_plugin.h"
+#include"seq_decl_plugin.h"
 #include"basic_simplifier_plugin.h"
 
 class fpa2bv_converter {
@@ -33,6 +38,9 @@ protected:
     fpa_util                   m_util;
     bv_util                    m_bv_util;
     arith_util                 m_arith_util;
+    array_util                 m_array_util;
+    datatype_util              m_dt_util;
+    seq_util                   m_seq_util;
     mpf_manager              & m_mpf_manager;
     unsynch_mpz_manager      & m_mpz_manager;
     fpa_decl_plugin          * m_plugin;
@@ -40,7 +48,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*>  m_uf2bvuf;    
 
     obj_map<func_decl, std::pair<app *, app *> > m_specials;
 
@@ -59,12 +67,9 @@ public:
     bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
     bool is_rm(sort * s) { return m_util.is_rm(s); }
     bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
-
-    void mk_rm(expr * bv3, expr_ref & result);
-
-    void mk_fp(expr * sign, expr * exponent, expr * significand, expr_ref & result);
+    
     void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-
+    
     void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
     void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
 
@@ -145,7 +150,7 @@ public:
     expr_ref_vector m_extra_assertions;
 
     bool is_special(func_decl * f) { return m_specials.contains(f); }
-    bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }
+    bool is_uf2bvuf(func_decl * f) { return m_uf2bvuf.contains(f); }    
 
 protected:
     void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);
@@ -190,6 +195,7 @@ protected:
     func_decl_ref replace_function(func_decl * f);
     expr_ref replace_float_arg(expr * a);
     void mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result);
+    func_decl * get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity);
 
 private:
     void mk_nan(sort * s, expr_ref & result);
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 2eb85c87c..7680025e0 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -56,7 +56,10 @@ bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
 
 
 br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-    TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
+    TRACE("fpa2bv_rw", tout << "func: " << f->get_name() << std::endl;
+                       tout << "args: " << std::endl;
+                       for (unsigned i = 0; i < num; i++)
+                           tout << mk_ismt2_pp(args[i], m()) << std::endl;);
 
     if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
         m_conv.mk_const(f, result);
@@ -71,7 +74,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
     if (m().is_eq(f)) {
         SASSERT(num == 2);
         TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
-              mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
+            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)) {
@@ -83,7 +86,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
             return BR_DONE;
         }
         return BR_FAILED;
-    }
+    }    
     else if (m().is_ite(f)) {
         SASSERT(num == 3);
         if (m_conv.is_float(args[1])) {
@@ -100,7 +103,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         }
         return BR_FAILED;
     }
-
+    
     if (m_conv.is_float_family(f)) {
         switch (f->get_decl_kind()) {
         case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
@@ -166,19 +169,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
             NOT_IMPLEMENTED_YET();
         }
     }
-    else {
+    else 
+    {
         SASSERT(!m_conv.is_float_family(f));
-        bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
-        
-        for (unsigned i = 0; i < f->get_arity(); i++) {
-            sort * di = f->get_domain()[i];
-            is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
-        }
-
-        if (is_float_uf) {
-            m_conv.mk_function(f, num, args, result);
-            return BR_DONE;
-        }
+        m_conv.mk_function(f, num, args, result);
+        return BR_DONE;
     }
 
     return BR_FAILED;
@@ -249,17 +244,15 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
 
     expr_ref new_exp(m());
     sort * s = t->get_sort();
-    if (m_conv.is_float(s))
-        {
-            expr_ref new_var(m());
-            unsigned ebits = m_conv.fu().get_ebits(s);
-            unsigned sbits = m_conv.fu().get_sbits(s);
-            new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
-            m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
-                         m_conv.bu().mk_extract(ebits - 1, 0, new_var),
-                         m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
-                         new_exp);
-        }
+    if (m_conv.is_float(s)) {
+        expr_ref new_var(m());
+        unsigned ebits = m_conv.fu().get_ebits(s);
+        unsigned sbits = m_conv.fu().get_sbits(s);
+        new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
+        new_exp = m_conv.fu().mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
+                                    m_conv.bu().mk_extract(ebits - 1, 0, new_var),
+                                    m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var));
+    }
     else
         new_exp = m().mk_var(t->get_idx(), s);
 
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 069e7ed18..22043e7a4 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -691,7 +691,7 @@ func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters
 }
 
 func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                                   unsigned arity, sort * const * domain, sort * range) {
+                                                 unsigned arity, sort * const * domain, sort * range) {
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to bv_wrap");
     if (!is_float_sort(domain[0]) && !is_rm_sort(domain[0]))
@@ -1076,3 +1076,64 @@ app * fpa_util::mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits)
     sort * range = m_a_util.mk_real();
     return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range);
 }
+
+bool fpa_util::contains_floats(ast * a) {
+    switch (a->get_kind()) {
+    case AST_APP: {
+        app * aa = to_app(a);
+        if (contains_floats(aa->get_decl()))
+            return true;
+        else
+            for (unsigned i = 0; i < aa->get_num_args(); i++)
+                if (contains_floats(aa->get_arg(i)))
+                    return true;
+        break;
+    }
+    case AST_VAR:
+        return contains_floats(to_var(a)->get_sort());
+        break;
+    case AST_QUANTIFIER: {
+        quantifier * q = to_quantifier(a);
+        for (unsigned i = 0; i < q->get_num_children(); i++)
+            if (contains_floats(q->get_child(i)))
+                return true;
+        for (unsigned i = 0; i < q->get_num_decls(); i++)
+            if (contains_floats(q->get_decl_sort(i)))
+                return true;
+        if (contains_floats(q->get_expr()))
+            return true;
+        break;
+    }
+    case AST_SORT: {
+        sort * s = to_sort(a);
+        if (is_float(s) || is_rm(s))
+            return true;
+        else {
+            for (unsigned i = 0; i < s->get_num_parameters(); i++) {
+                parameter const & pi = s->get_parameter(i);
+                if (pi.is_ast() && contains_floats(pi.get_ast()))
+                    return true;
+            }
+        }
+        break;
+    }
+    case AST_FUNC_DECL: {
+        func_decl * f = to_func_decl(a);
+        for (unsigned i = 0; i < f->get_arity(); i++)
+            if (contains_floats(f->get_domain(i)))
+                return true;
+        if (contains_floats(f->get_range()))
+            return true;
+        for (unsigned i = 0; i < f->get_num_parameters(); i++) {
+            parameter const & pi = f->get_parameter(i);
+            if (pi.is_ast() && contains_floats(pi.get_ast()))
+                return true;
+        }
+        break;
+    }
+    default:
+        UNREACHABLE();
+    }
+
+    return false;
+}
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 8683bf5f1..33667e3f7 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -294,7 +294,18 @@ public:
     bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
     bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
 
-    app * mk_fp(expr * sgn, expr * exp, expr * sig) { return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); }
+    app * mk_fp(expr * sgn, expr * exp, expr * sig) { 
+        SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
+        SASSERT(m_bv_util.is_bv(exp));
+        SASSERT(m_bv_util.is_bv(sig));
+        return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); 
+    }
+    
+    app * mk_rm(expr * bv3) { 
+        SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
+        return m().mk_app(m_fid, OP_FPA_INTERNAL_RM_BVWRAP, 0, 0, 1, &bv3, mk_rm_sort());
+    }
+
     app * mk_to_fp(sort * s, expr * bv_t) {
         SASSERT(is_float(s) && s->get_num_parameters() == 2);
         return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);
@@ -370,7 +381,9 @@ public:
     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_rm_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP); }
-    bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }
+    bool is_rm_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_RM_BVWRAP; }    
+
+    bool contains_floats(ast * a);
 };
 
 #endif
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 19b8c3909..b4ae744d3 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -109,8 +109,6 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         st = BR_FAILED;
         break;
 
-        
-
     default:
         NOT_IMPLEMENTED_YET();
     }
@@ -892,7 +890,6 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) {
     return BR_FAILED;
 }
 
-
 br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
     if (is_app_of(arg, m_util.get_family_id(), OP_FPA_FP)) {
         bv_util bu(m());
@@ -923,10 +920,3 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
 
     return BR_FAILED;
 }
-
-//br_status fpa_rewriter::mk_bvunwrap(expr * arg, expr_ref & result) {
-//    if (is_app_of(arg, m_util.get_family_id(), OP_FPA_INTERNAL_BVWRAP))
-//        result = to_app(arg)->get_arg(0);
-//    
-//    return BR_FAILED;
-//}
diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h
index f42d7c719..10f4ab4aa 100644
--- a/src/ast/rewriter/fpa_rewriter.h
+++ b/src/ast/rewriter/fpa_rewriter.h
@@ -91,7 +91,6 @@ public:
     br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result);
 
     br_status mk_bvwrap(expr * arg, expr_ref & result);
-    br_status mk_bvunwrap(expr * arg, expr_ref & result);
 };
 
 #endif
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 0268d2353..dca364686 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -54,10 +54,9 @@ namespace smt {
             unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
             unsigned sbits = m_th.m_fpa_util.get_sbits(s);
             SASSERT(bv_sz == m_th.m_fpa_util.get_ebits(s) + sbits);
-            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);
+            result = m_util.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));
             SASSERT(m_th.m_fpa_util.is_float(result));
             m_const2bv.insert(f, result);
             m.inc_ref(f);
@@ -76,7 +75,7 @@ namespace smt {
             SASSERT(is_rm(f->get_range()));
             expr_ref bv(m);
             bv = m_th.wrap(m.mk_const(f));
-            mk_rm(bv, result);
+            result = m_util.mk_rm(bv);
             m_rm_const2bv.insert(f, result);
             m.inc_ref(f);
             m.inc_ref(result);
@@ -84,8 +83,8 @@ namespace smt {
     }
 
     void theory_fpa::fpa2bv_converter_wrapped::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-        return fpa2bv_converter::mk_function(f, num, args, result);
-        TRACE("t_fpa", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
+        // Note: this introduces new UFs that should be filtered afterwards. 
+        return fpa2bv_converter::mk_function(f, num, args, result);        
     }
 
     expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@@ -100,10 +99,9 @@ namespace smt {
         expr_ref a(m), wrapped(m);
         a = m.mk_app(w, x, y);
         wrapped = m_th.wrap(a);
-        m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
-                               m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
-                               m_bv_util.mk_extract(sbits - 2, 0, wrapped),
-                               res);
+        res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
+                           m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
+                           m_bv_util.mk_extract(sbits - 2, 0, wrapped));
 
         expr_ref sc(m);
         m_th.m_converter.mk_is_zero(res, sc);
@@ -123,10 +121,9 @@ namespace smt {
         expr_ref a(m), wrapped(m);
         a = m.mk_app(w, x, y);
         wrapped = m_th.wrap(a);
-        m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
-                               m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
-                               m_bv_util.mk_extract(sbits - 2, 0, wrapped),
-                               res);
+        res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped),
+                           m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped),
+                           m_bv_util.mk_extract(sbits - 2, 0, wrapped));
 
         expr_ref sc(m);
         m_th.m_converter.mk_is_zero(res, sc);
@@ -320,8 +317,7 @@ namespace smt {
         SASSERT(!m_fpa_util.is_fp(e));
         SASSERT(m_bv_util.is_bv(e));
         SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
-        ast_manager & m = get_manager();
-        sort * bv_srt = m.get_sort(e);
+        ast_manager & m = get_manager();        
         app_ref res(m);
 
         unsigned bv_sz = m_bv_util.get_bv_size(e);
@@ -380,7 +376,7 @@ namespace smt {
             SASSERT(m_fpa_util.is_rm_bvwrap(e_conv));
             expr_ref bv_rm(m);
             m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
-            m_converter.mk_rm(bv_rm, res);
+            res = m_fpa_util.mk_rm(bv_rm);
         }
         else if (m_fpa_util.is_float(e)) {
             SASSERT(m_fpa_util.is_fp(e_conv));
@@ -389,7 +385,7 @@ namespace smt {
             m_th_rw(sgn);
             m_th_rw(exp);
             m_th_rw(sig);
-            m_converter.mk_fp(sgn, exp, sig, res);
+            res = m_fpa_util.mk_fp(sgn, exp, sig);
         }
         else
             UNREACHABLE();
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index 41650eda6..64423f224 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -55,6 +55,7 @@ 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) << ")";
     }
+    out << ")";
 }
 
 model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
@@ -197,16 +198,25 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, expr * val) {
 
 expr_ref fpa2bv_model_converter::rebuild_floats(model * bv_mdl, sort * s, expr * e) {
     expr_ref result(m);
-
     TRACE("fpa2bv_mc", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for " << mk_ismt2_pp(e, m) << std::endl;);
 
     if (m_fpa_util.is_float(s)) {
-        SASSERT(m_bv_util.is_bv(e));
-        result = convert_bv2fp(bv_mdl, s, e);
+        if (m_fpa_util.is_numeral(e)) {
+            result = e;
+        }
+        else {
+            SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s)));
+            result = convert_bv2fp(bv_mdl, s, e);
+        }
     }
     else if (m_fpa_util.is_rm(s)) {
-        SASSERT(m_bv_util.get_bv_size(e) == 3);
-        result = convert_bv2rm(bv_mdl, e);
+        if (m_fpa_util.is_rm_numeral(e)) {
+            result = e;
+        }
+        else {
+            SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3);
+            result = convert_bv2rm(bv_mdl, e);
+        }
     }
     else if (is_app(e)) {
         app * a = to_app(e);
@@ -229,6 +239,7 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
 
     expr_ref as_arr_mdl(m);
     as_arr_mdl = bv_mdl->get_const_interp(bv_f);
+    if (as_arr_mdl == 0) return am;
     TRACE("fpa2bv_mc", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;);
     SASSERT(arr_util.is_as_array(as_arr_mdl));
     for (unsigned i = 0; i < arity; i++)
@@ -410,9 +421,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
             }
             else {
                 // Just keep.
+                SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
                 expr_ref val(m);
                 bv_mdl->eval(it->m_value, val);
-                float_mdl->register_decl(f, val);
+                if (val) float_mdl->register_decl(f, val);
             }
         }            
         else {
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index ce38527c1..0e92841de 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/src/tactic/fpa/fpa2bv_model_converter.h
@@ -118,15 +118,14 @@ protected:
 
     func_interp * convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);
     expr_ref rebuild_floats(model * bv_mdl, sort * s, expr * e);
-    
-    
+        
     class array_model {
     public:
         func_decl * new_float_fd;
         func_interp * new_float_fi;
         func_decl * bv_fd;
         expr_ref result;
-        array_model(ast_manager & m) : result(m) {}
+        array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {}
     };
 
     array_model convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);