diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index e6b9dda07..d5849a1fd 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -77,8 +77,8 @@ 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(is_app_of(a, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
-        SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
+        SASSERT(m_util.is_rm_bvwrap(b));
+        SASSERT(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;);
@@ -221,14 +221,14 @@ 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) {
+void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * const * 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());
+        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),
@@ -236,71 +236,171 @@ void fpa2bv_converter::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr
     }
     else if (m_util.is_rm(rng)) {
         app_ref na(m);
-        na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+        na = m.mk_app(fbv, fbv->get_arity(), new_args);
         mk_rm(na, result);
     }
     else
-        result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+        result = m.mk_app(fbv, fbv->get_arity(), new_args);
 }
 
-void fpa2bv_converter::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
+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());
+    }
+
+    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++) {
-        if (is_float(args[i])) {
-            expr * sgn, *exp, *sig;
-            split_fp(args[i], sgn, exp, sig);
-            expr * args[3] = { sgn, exp, sig };
-            new_args.push_back(m_bv_util.mk_concat(3, args));
-        }
-        else if (is_rm(args[i])) {
-            SASSERT(is_app_of(args[i], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
-            new_args.push_back(to_app(args[i])->get_arg(0));
-        }
-        else
-            new_args.push_back(args[i]);
-    }
+    for (unsigned i = 0; i < num; i++)
+        new_args.push_back(replace_float_arg(args[i]));
 
-    func_decl * fd;
-    if (m_uf2bvuf.find(f, fd))
-        mk_uninterpreted_output(f->get_range(), fd, new_args, result);
-    else {
-        sort_ref_buffer new_domain(m);
+    TRACE("fpa2bv", tout << "UF bv-args:";
+                    for (unsigned i = 0; i < num; i++)
+                        tout << " " << mk_ismt2_pp(new_args[i], m);
+                    tout << std::endl; );
 
-        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(di);
-        }
-
-        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);
-
-        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);
-    }
+    func_decl_ref rf(m);
+    rf = replace_function(f);
+    mk_function_output(f->get_range(), rf, new_args.c_ptr(), result);
 
     TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
-
     SASSERT(is_well_sorted(m, result));
 }
 
@@ -548,7 +648,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
 
 void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
 
     expr_ref rm(m), x(m), y(m);
     rm = to_app(args[0])->get_arg(0);
@@ -718,7 +818,7 @@ void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
 
 void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
 
     expr_ref rm(m), x(m), y(m);
     rm = to_app(args[0])->get_arg(0);
@@ -868,7 +968,7 @@ void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref &
 
 void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
     expr_ref rm(m), x(m), y(m);
     rm = to_app(args[0])->get_arg(0);
     x = args[1];
@@ -1308,7 +1408,7 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
 
 void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 4);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
 
     // fusedma means (x * y) + z
     expr_ref rm(m), x(m), y(m), z(m);
@@ -1626,7 +1726,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
 
 void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
 
     expr_ref rm(m), x(m);
     rm = to_app(args[0])->get_arg(0);
@@ -1775,7 +1875,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
 
 void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
 
     expr_ref rm(m), x(m);
     rm = to_app(args[0])->get_arg(0);
@@ -2236,7 +2336,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
 
 
 void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
-    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(rm));
     mk_to_fp_float(s, to_app(rm)->get_arg(0), x, result);
 }
 
@@ -2407,7 +2507,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         "x: " << mk_ismt2_pp(x, m) << std::endl;);
     SASSERT(m_util.is_float(s));
     SASSERT(au().is_real(x) || au().is_int(x));
-    SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(rm));
 
     expr * bv_rm = to_app(rm)->get_arg(0);
     unsigned ebits = m_util.get_ebits(s);
@@ -2542,7 +2642,7 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());
 
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
     expr * bv_rm = to_app(args[0])->get_arg(0);
 
     rational e;
@@ -2700,7 +2800,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
 
     SASSERT(num == 2);
     SASSERT(m_util.is_float(f->get_range()));
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
     SASSERT(m_bv_util.is_bv(args[1]));
 
     expr_ref rm(m), x(m);
@@ -2842,7 +2942,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
 
     SASSERT(num == 2);
     SASSERT(m_util.is_float(f->get_range()));
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
     SASSERT(m_bv_util.is_bv(args[1]));
 
     expr_ref rm(m), x(m);
@@ -2994,7 +3094,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
         tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
 
     SASSERT(num == 2);
-    SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
+    SASSERT(m_util.is_rm_bvwrap(args[0]));
     SASSERT(m_util.is_float(args[1]));
 
     expr * rm = to_app(args[0])->get_arg(0);
@@ -3246,7 +3346,7 @@ expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sb
 
 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, 0, 0, 1, &bv3, m_util.mk_rm_sort());
+    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) {
@@ -3266,7 +3366,7 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
 }
 
 void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const {
-    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
     sgn = to_app(e)->get_arg(0);
     exp = to_app(e)->get_arg(1);
@@ -3274,7 +3374,7 @@ void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & s
 }
 
 void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const {
-    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
     expr *e_sgn, *e_sig, *e_exp;
     split_fp(e, e_sgn, e_exp, e_sig);
@@ -3324,7 +3424,7 @@ void fpa2bv_converter::mk_is_ninf(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
-    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
     expr * a0 = to_app(e)->get_arg(0);
     expr_ref zero(m);
@@ -3333,7 +3433,7 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
-    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
     expr * a0 = to_app(e)->get_arg(0);
     expr_ref one(m);
@@ -3502,7 +3602,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize) {
-    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP));
+    SASSERT(m_util.is_fp(e));
     SASSERT(to_app(e)->get_num_args() == 3);
 
     sort * srt = to_app(e)->get_decl()->get_range();
@@ -3599,9 +3699,9 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
     TRACE("fpa2bv_unpack", tout << "UNPACK EXP = " << mk_ismt2_pp(exp, m) << std::endl; );
 }
 
-void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
+void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
 {
-    switch(f->get_decl_kind())
+    switch(k)
     {
     case OP_FPA_RM_NEAREST_TIES_TO_EVEN: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3); break;
     case OP_FPA_RM_NEAREST_TIES_TO_AWAY: result = m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3); break;
@@ -3618,9 +3718,9 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
 #ifdef Z3DEBUG
     return;
     // CMW: This works only for quantifier-free formulas.
-    if (is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)) {
+    if (m_util.is_fp(e)) {
         expr_ref new_bv(m);
-        expr *e_sgn, *e_sig, *e_exp;
+        expr *e_sgn, *e_sig, *e_exp; 
         split_fp(e, e_sgn, e_exp, e_sig);
         unsigned ebits = m_bv_util.get_bv_size(e_exp);
         unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1;
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 32c3124db..879c1e080 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -72,11 +72,11 @@ public:
     void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
     void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
-    void mk_rounding_mode(func_decl * f, expr_ref & result);
+    void mk_rounding_mode(decl_kind k, expr_ref & result);
     void mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     virtual void mk_const(func_decl * f, expr_ref & result);
     virtual void mk_rm_const(func_decl * f, expr_ref & result);
-    virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_var(unsigned base_inx, sort * srt, expr_ref & result);
 
     void mk_pinf(func_decl * f, expr_ref & result);
@@ -186,7 +186,10 @@ protected:
 
     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);
+    sort_ref replace_float_sorts(sort * s);
+    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);
 
 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 27fc8ebc7..2eb85c87c 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -107,7 +107,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
         case OP_FPA_RM_TOWARD_NEGATIVE:
         case OP_FPA_RM_TOWARD_POSITIVE:
-        case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
+        case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f->get_decl_kind(), result); return BR_DONE;
         case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
         case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
         case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
@@ -152,9 +152,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
         case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
 
-        case OP_FPA_INTERNAL_RM:
         case OP_FPA_INTERNAL_BVWRAP:
-        case OP_FPA_INTERNAL_BVUNWRAP:
+        case OP_FPA_INTERNAL_RM_BVWRAP:
+        
         case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
         case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
         case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
@@ -169,14 +169,14 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
     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_uninterpreted_function(f, num, args, result);
+            m_conv.mk_function(f, num, args, result);
             return BR_DONE;
         }
     }
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 511d36e67..069e7ed18 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -711,18 +711,6 @@ func_decl * fpa_decl_plugin::mk_internal_bv_wrap(decl_kind k, unsigned num_param
     }
 }
 
-func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                                     unsigned arity, sort * const * domain, sort * range) {
-    if (arity != 1)
-        m_manager->raise_exception("invalid number of arguments to bv_unwrap");
-    if (!is_sort_of(domain[0], m_bv_fid, BV_SORT))
-        m_manager->raise_exception("sort mismatch, expected argument of bitvector sort");
-    if (!is_float_sort(range) && !is_rm_sort(range))
-        m_manager->raise_exception("sort mismatch, expected range of FloatingPoint or RoundingMode sort");
-
-    return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
-}
-
 func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified(
     decl_kind k, unsigned num_parameters, parameter const * parameters,
     unsigned arity, sort * const * domain, sort * range) {
@@ -847,12 +835,10 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_FPA_TO_IEEE_BV:
         return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
 
-    case OP_FPA_INTERNAL_RM:
-        return mk_internal_rm(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_INTERNAL_BVWRAP:
-        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
-    case OP_FPA_INTERNAL_BVUNWRAP:
-        return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range);
+        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);    
+    case OP_FPA_INTERNAL_RM_BVWRAP:
+        return mk_internal_rm(k, num_parameters, parameters, arity, domain, range);
 
     case OP_FPA_INTERNAL_MIN_I:
     case OP_FPA_INTERNAL_MAX_I:
@@ -1027,12 +1013,12 @@ sort * fpa_util::mk_float_sort(unsigned ebits, unsigned sbits) {
     return m().mk_sort(m_fid, FLOATING_POINT_SORT, 2, ps);
 }
 
-unsigned fpa_util::get_ebits(sort * s) {
+unsigned fpa_util::get_ebits(sort * s) const {
     SASSERT(is_float(s));
     return static_cast<unsigned>(s->get_parameter(0).get_int());
 }
 
-unsigned fpa_util::get_sbits(sort * s) {
+unsigned fpa_util::get_sbits(sort * s) const {
     SASSERT(is_float(s));
     return static_cast<unsigned>(s->get_parameter(1).get_int());
 }
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index a351b2610..8683bf5f1 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -87,9 +87,8 @@ enum fpa_op_kind {
     OP_FPA_TO_IEEE_BV,
 
     /* Internal use only */
-    OP_FPA_INTERNAL_RM, // Internal conversion from (_ BitVec 3) to RoundingMode
     OP_FPA_INTERNAL_BVWRAP,
-    OP_FPA_INTERNAL_BVUNWRAP,
+    OP_FPA_INTERNAL_RM_BVWRAP, // Internal conversion from (_ BitVec 3) to RoundingMode
 
     OP_FPA_INTERNAL_MIN_I,
     OP_FPA_INTERNAL_MAX_I,
@@ -256,12 +255,13 @@ public:
 
     sort * mk_float_sort(unsigned ebits, unsigned sbits);
     sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
-    bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOATING_POINT_SORT); }
-    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
-    bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
-    bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
-    unsigned get_ebits(sort * s);
-    unsigned get_sbits(sort * s);
+    bool is_float(sort * s) const { return is_sort_of(s, m_fid, FLOATING_POINT_SORT); }
+    bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
+    bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); }
+    bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); }
+    bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }    
+    unsigned get_ebits(sort * s) const;
+    unsigned get_sbits(sort * s) const;
 
     app * mk_round_nearest_ties_to_even() { return m().mk_const(m_fid, OP_FPA_RM_NEAREST_TIES_TO_EVEN); }
     app * mk_round_nearest_ties_to_away() { return m().mk_const(m_fid, OP_FPA_RM_NEAREST_TIES_TO_AWAY); }
@@ -367,8 +367,10 @@ public:
     app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits);
     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); }
+    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; }
 };
 
 #endif
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 6c199fcd8..19b8c3909 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -98,9 +98,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
     case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
         SASSERT(num_args == 2); st = BR_FAILED; break;
+    
+    case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
+    case OP_FPA_INTERNAL_RM_BVWRAP:SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
 
-    case OP_FPA_INTERNAL_RM:
-        SASSERT(num_args == 1);  SASSERT(num_args == 1); st = mk_rm(args[0], result); break;
     case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
     case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
     case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
@@ -108,8 +109,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         st = BR_FAILED;
         break;
 
-    case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
-    case OP_FPA_INTERNAL_BVUNWRAP: SASSERT(num_args == 1); st = mk_bvunwrap(args[0], result); break;
+        
 
     default:
         NOT_IMPLEMENTED_YET();
@@ -924,9 +924,9 @@ 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;
-}
+//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/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 802c2c500..ea8ba0f79 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -83,89 +83,8 @@ namespace smt {
         }
     }
 
-    void theory_fpa::fpa2bv_converter_wrapped::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 if (m_util.is_rm(rng)) {
-            app_ref na(m);
-            na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
-            mk_rm(na, result);
-        }
-        else
-            result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
-    }
-
-    void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-        // TODO: This introduces temporary func_decls that should be filtered in the end.
-
-        TRACE("t_fpa", 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++) {
-            TRACE("t_fpa", tout << "UF arg[" << i << "]: " << mk_ismt2_pp(args[i], m) << std::endl; );
-            if (is_float(args[i]) || is_rm(args[i])) {
-                expr_ref ai(m), wrapped(m);
-                ai = args[i];              
-                wrapped = m_th.wrap(ai);
-                new_args.push_back(wrapped);
-                TRACE("t_fpa", tout << "UF wrap ai: " << mk_ismt2_pp(ai, m) << " --> " << mk_ismt2_pp(wrapped, m) << std::endl; );
-                m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, m.get_sort(ai)), ai));
-            }
-            else
-                new_args.push_back(args[i]);
-        }
-
-        func_decl * fd;
-        if (m_uf2bvuf.find(f, fd)) {
-            TRACE("t_fpa", tout << "UF reused: " << mk_ismt2_pp(fd, m) << std::endl; );
-            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++) {
-                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(di);
-            }
-
-            sort * frng = f->get_range();
-            sort_ref rng(frng, m);
-            if (m_util.is_float(frng))
-                rng = m_bv_util.mk_sort(m_util.get_ebits(frng) + m_util.get_sbits(frng));
-            else if (m_util.is_rm(frng))
-                rng = m_bv_util.mk_sort(3);
-
-            func_decl_ref fbv(m);
-            fbv = m.mk_fresh_func_decl(new_domain.size(), new_domain.c_ptr(), rng);            
-            TRACE("t_fpa", 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(frng, fbv, new_args, result);
-        }
-
-        expr_ref fapp(m);
-        fapp = m.mk_app(f, num, args);
-        m_extra_assertions.push_back(m.mk_eq(fapp, result));        
+    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; );
     }
 
@@ -239,12 +158,10 @@ namespace smt {
             ast_manager & m = get_manager();
             dec_ref_map_values(m, m_conversions);
             dec_ref_map_values(m, m_wraps);
-            dec_ref_map_values(m, m_unwraps);
         }
         else {
             SASSERT(m_conversions.empty());
             SASSERT(m_wraps.empty());
-            SASSERT(m_unwraps.empty());
         }
 
         m_is_initialized = false;
@@ -256,7 +173,6 @@ namespace smt {
     }
 
     app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
-
         TRACE("t_fpa_detail", 
               ast_manager & m = m_th.get_manager();
               for (unsigned i = 0; i < values.size(); i++)
@@ -321,11 +237,11 @@ namespace smt {
         mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
         result = m_fu.mk_value(f);
 
-        TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" <<
+        TRACE("t_fpa", tout << "result: [" <<
                        mpzm.to_string(sgn_z) << "," <<
                        mpzm.to_string(exp_z) << "," <<
                        mpzm.to_string(sig_z) << "] --> " <<
-                       mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
+                       mk_ismt2_pp(result, m_th.get_manager()) << std::endl;);
 
         return result;
     }
@@ -355,20 +271,18 @@ namespace smt {
         default: result = m_fu.mk_round_toward_zero();
         }
 
-        TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
-                               mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
+        TRACE("t_fpa", tout << "result: " << mk_ismt2_pp(result, m_th.get_manager()) << std::endl;);
 
         return result;
     }
 
     app_ref theory_fpa::wrap(expr * e) {
-        SASSERT(!m_fpa_util.is_wrap(e));
+        SASSERT(m_fpa_util.is_float(e) || m_fpa_util.is_rm(e));
+        SASSERT(!m_fpa_util.is_bvwrap(e));
         ast_manager & m = get_manager();
         app_ref res(m);
 
-        if (is_app(e) &&
-            to_app(e)->get_family_id() == get_family_id() &&
-            to_app(e)->get_decl_kind() == OP_FPA_FP) {
+        if (m_fpa_util.is_fp(e)) {
             expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };            
             res = m_bv_util.mk_concat(3, cargs);
             m_th_rw((expr_ref&)res);
@@ -398,35 +312,42 @@ namespace smt {
             res = m.mk_app(w, e);
         }
 
-        TRACE("t_fpa", tout << "e: " << mk_ismt2_pp(e, m) << "\n";
-                       tout << "r: " << mk_ismt2_pp(res, m) << "\n";);
-
-        
         return res;
     }
 
     app_ref theory_fpa::unwrap(expr * e, sort * s) {
-        SASSERT(!m_fpa_util.is_unwrap(e));
+        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);
-
-        func_decl *u;
-
-        if (!m_unwraps.find(bv_srt, u)) {
-            SASSERT(!m_unwraps.contains(bv_srt));
-            u = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
-            m_unwraps.insert(bv_srt, u);
-            m.inc_ref(u);
-        }
-
         app_ref res(m);
-        res = m.mk_app(u, e);
+
+        unsigned bv_sz = m_bv_util.get_bv_size(e);
+
+        if (m_fpa_util.is_rm(s)) {
+            SASSERT(bv_sz == 3);
+            res = m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), m_fpa_util.mk_round_nearest_ties_to_away(),
+                  m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), m_fpa_util.mk_round_nearest_ties_to_even(),
+                  m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3)), m_fpa_util.mk_round_toward_negative(),
+                  m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_fpa_util.mk_round_toward_positive(),
+                           m_fpa_util.mk_round_toward_zero()))));
+        }
+        else {
+            SASSERT(m_fpa_util.is_float(s));
+            unsigned sbits = m_fpa_util.get_sbits(s);
+            SASSERT(bv_sz == m_fpa_util.get_ebits(s) + sbits);
+            res = m_fpa_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e),
+                                   m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
+                                   m_bv_util.mk_extract(sbits - 2, 0, e));
+        }
+        
         return res;
     }
 
     expr_ref theory_fpa::convert_atom(expr * e) {
         ast_manager & m = get_manager();
-        TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";);
+        TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << std::endl;);
         expr_ref res(m);
         proof_ref pr(m);
         m_rw(e, res);
@@ -444,33 +365,24 @@ namespace smt {
         proof_ref pr(m);
         m_rw(e, e_conv);
 
-        TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << "\n";
-                              tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << "\n";);
+        TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
+                              tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
 
         if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
-            if (!m_fpa_util.is_float(e_conv))
+            UNREACHABLE();
+            if (!m_fpa_util.is_float(e_conv) && !m_fpa_util.is_rm(e_conv))
                 m_th_rw(e_conv, res);
-            else {
-                expr_ref bv(m);
-                bv = wrap(e_conv);
-                unsigned bv_sz = m_bv_util.get_bv_size(bv);
-                unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv));
-                SASSERT(bv_sz == m_fpa_util.get_ebits(m.get_sort(e_conv)) + sbits);
-                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),
-                    res);
-            }
+            else
+                res = unwrap(wrap(e_conv), m.get_sort(e));
         }
-        else if (m_fpa_util.is_rm(e)) {
-            SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_INTERNAL_RM));
+        else if (m_fpa_util.is_rm(e)) {            
+            SASSERT(m_fpa_util.is_rm_bvwrap(e_conv));
             expr_ref bv_rm(m);
-            bv_rm = to_app(e_conv)->get_arg(0);
-            m_th_rw(bv_rm);
+            m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
             m_converter.mk_rm(bv_rm, res);
         }
         else if (m_fpa_util.is_float(e)) {
-            SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_FP));
+            SASSERT(m_fpa_util.is_fp(e_conv));
             expr_ref sgn(m), sig(m), exp(m);
             m_converter.split_fp(e_conv, sgn, exp, sig);
             m_th_rw(sgn);
@@ -486,6 +398,7 @@ namespace smt {
     }
 
     expr_ref theory_fpa::convert_conversion_term(expr * e) {
+        SASSERT(to_app(e)->get_family_id() == get_family_id());
         /* This is for the conversion functions fp.to_* */
         ast_manager & m = get_manager();
         expr_ref res(m);
@@ -498,28 +411,6 @@ namespace smt {
         return res;
     }
 
-    expr_ref theory_fpa::convert_unwrap(expr * e) {
-        SASSERT(m_fpa_util.is_unwrap(e));
-        ast_manager & m = get_manager();
-        sort * srt = m.get_sort(e);
-        expr_ref res(m);
-        if (m_fpa_util.is_rm(srt)) {
-            m_converter.mk_rm(to_app(e)->get_arg(0), res);
-        }
-        else {
-            SASSERT(m_fpa_util.is_float(srt));
-            unsigned sbits = m_fpa_util.get_sbits(srt);
-            expr_ref bv(m);
-            bv = to_app(e)->get_arg(0);
-            unsigned bv_sz = m_bv_util.get_bv_size(bv);
-            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),
-                              res);
-        }
-        return res;
-    }
-
     expr_ref theory_fpa::convert(expr * e)
     {
         ast_manager & m = get_manager();
@@ -534,8 +425,8 @@ namespace smt {
                 mk_ismt2_pp(res, m) << std::endl;);
         }
         else {
-            if (m_fpa_util.is_unwrap(e))
-                res = convert_unwrap(e);
+            if (m_fpa_util.is_fp(e))
+                res = e;
             else if (m.is_bool(e))
                 res = convert_atom(e);
             else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
@@ -577,7 +468,7 @@ namespace smt {
 
         m_th_rw(res);
 
-        CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
+        CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << std::endl;);
         return res;
     }
 
@@ -589,18 +480,17 @@ namespace smt {
         literal lit(ctx.get_literal(e));
         ctx.mark_as_relevant(lit);
         ctx.mk_th_axiom(get_id(), 1, &lit);
-        TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
     }
 
     void theory_fpa::attach_new_th_var(enode * n) {
         context & ctx = get_context();
         theory_var v = mk_var(n);
         ctx.attach_th_var(n, this, v);
-        TRACE("t_fpa_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
+        TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
     }
 
     bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
-        TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
+        TRACE("t_fpa_internalize", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
         SASSERT(atom->get_family_id() == get_family_id());
 
         ast_manager & m = get_manager();
@@ -625,11 +515,12 @@ namespace smt {
     }
 
     bool theory_fpa::internalize_term(app * term) {
+        TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
+        SASSERT(term->get_family_id() == get_family_id());
+        SASSERT(!get_context().e_internalized(term));
+        
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
-        SASSERT(term->get_family_id() == get_family_id());
-        SASSERT(!ctx.e_internalized(term));
 
         unsigned num_args = term->get_num_args();
         for (unsigned i = 0; i < num_args; i++)
@@ -638,29 +529,29 @@ namespace smt {
         enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
                                                  ctx.mk_enode(term, false, false, true);
 
-        if (is_attached_to_var(e))
-            return false;
+        if (!is_attached_to_var(e)) {
+            attach_new_th_var(e);
 
-        attach_new_th_var(e);
+            // The conversion operators fp.to_* appear in non-FP constraints.
+            // The corresponding constraints will not be translated and added
+            // via convert(...) and assert_cnstr(...) in initialize_atom(...).
+            // Therefore, we translate and assert them here.
+            fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
+            switch (k) {
+            case OP_FPA_TO_FP:
+            case OP_FPA_TO_UBV:
+            case OP_FPA_TO_SBV:
+            case OP_FPA_TO_REAL:
+            case OP_FPA_TO_IEEE_BV: {
 
-        // The conversion operators fp.to_* appear in non-FP constraints.
-        // The corresponding constraints will not be translated and added
-        // via convert(...) and assert_cnstr(...) in initialize_atom(...).
-        // Therefore, we translate and assert them here.
-        fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
-        switch (k) {
-        case OP_FPA_TO_FP:
-        case OP_FPA_TO_UBV:
-        case OP_FPA_TO_SBV:
-        case OP_FPA_TO_REAL:
-        case OP_FPA_TO_IEEE_BV: {
-            expr_ref conv(m);
-            conv = convert(term);
-            assert_cnstr(m.mk_eq(term, conv));
-            assert_cnstr(mk_side_conditions());
-            break;
-        }
-        default: /* ignore */;
+                expr_ref conv(m);
+                conv = convert(term);
+                assert_cnstr(m.mk_eq(term, conv));
+                assert_cnstr(mk_side_conditions());
+                break;
+            }
+            default: /* ignore */;
+            }
         }
 
         return true;
@@ -669,33 +560,35 @@ namespace smt {
     void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {
         TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
         SASSERT(s->get_family_id() == get_family_id());
+        SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
+        SASSERT(m_fpa_util.is_float(n->get_owner()) || m_fpa_util.is_rm(n->get_owner()));
+        SASSERT(n->get_owner()->get_decl()->get_range() == s);
 
         ast_manager & m = get_manager();
-        context & ctx = get_context();
-
-        app_ref owner(m);
-        owner = n->get_owner();
-
-        SASSERT(owner->get_decl()->get_range() == s);
-
-        if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) &&
-            !is_attached_to_var(n)) {
+        context & ctx = get_context();        
+        app_ref owner(n->get_owner(), m);
 
+        if (!is_attached_to_var(n)) {
             attach_new_th_var(n);
 
             if (m_fpa_util.is_rm(s)) {
                 // For every RM term, we need to make sure that it's
                 // associated bit-vector is within the valid range.
-                if (!m_fpa_util.is_unwrap(owner)) {
+                if (!m_fpa_util.is_rm_bvwrap(owner)) {
                     expr_ref valid(m), limit(m);
                     limit = m_bv_util.mk_numeral(4, 3);
                     valid = m_bv_util.mk_ule(wrap(owner), limit);
                     assert_cnstr(valid);
                 }
             }
-
-            if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner))
-                assert_cnstr(m.mk_eq(unwrap(wrap(owner), s), owner));
+            
+            if (!ctx.relevancy()) {
+                relevant_eh(owner);
+                /*expr_ref wu(m);
+                wu = m.mk_eq(unwrap(wrap(owner), s), owner);
+                TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, get_manager()) << std::endl;);
+                assert_cnstr(wu);*/
+            }
         }
     }
 
@@ -704,9 +597,9 @@ namespace smt {
         enode * e_x = get_enode(x);
         enode * e_y = get_enode(y);
 
-        TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
-        TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " <<
-                                      mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
+        TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;
+                       tout << mk_ismt2_pp(e_x->get_owner(), m) << std::endl << " = " << std::endl <<
+                               mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
 
         fpa_util & fu = m_fpa_util;
 
@@ -714,7 +607,7 @@ namespace smt {
         xe = e_x->get_owner();
         ye = e_y->get_owner();
 
-        if (m_fpa_util.is_wrap(xe) || m_fpa_util.is_wrap(ye))
+        if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
             return;
 
         expr_ref xc(m), yc(m);
@@ -744,9 +637,9 @@ namespace smt {
         enode * e_x = get_enode(x);
         enode * e_y = get_enode(y);
 
-        TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;);
-        TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
-            mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
+        TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;
+                       tout << mk_ismt2_pp(e_x->get_owner(), m) << std::endl << " != " << std::endl <<
+                           mk_ismt2_pp(e_y->get_owner(), m) << std::endl;);
 
         fpa_util & fu = m_fpa_util;
 
@@ -754,7 +647,7 @@ namespace smt {
         xe = e_x->get_owner();
         ye = e_y->get_owner();
 
-        if (m_fpa_util.is_wrap(xe) || m_fpa_util.is_wrap(ye))
+        if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
             return;
 
         expr_ref xc(m), yc(m);
@@ -817,7 +710,7 @@ namespace smt {
         mpf_manager & mpfm = m_fpa_util.fm();
 
         if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
-            if (!m_fpa_util.is_unwrap(n)) {
+            if (!m_fpa_util.is_fp(n)) {
                 expr_ref wrapped(m), c(m);
                 wrapped = wrap(n);
                 mpf_rounding_mode rm;
@@ -838,8 +731,10 @@ namespace smt {
                     assert_cnstr(c);
                 }
                 else {
-                    c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
-                    assert_cnstr(c);
+                    expr_ref wu(m);
+                    wu = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
+                    TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, get_manager()) << std::endl;);
+                    assert_cnstr(wu);
                 }
             }
         }
@@ -862,7 +757,6 @@ namespace smt {
         ast_manager & m = get_manager();
         dec_ref_map_values(m, m_conversions);
         dec_ref_map_values(m, m_wraps);
-        dec_ref_map_values(m, m_unwraps);
         theory::reset_eh();
     }
 
@@ -925,7 +819,7 @@ namespace smt {
                   mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
             res = vp;
         }
-        else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM)) {
+        else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM_BVWRAP)) {
             SASSERT(to_app(owner)->get_num_args() == 1);
             app_ref a0(m);
             a0 = to_app(owner->get_arg(0));
@@ -1012,11 +906,10 @@ namespace smt {
     }
 
     bool theory_fpa::include_func_interp(func_decl * f) {
-        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
-        func_decl * wt;
-
-        if (m_wraps.find(f->get_range(), wt) || m_unwraps.find(f->get_range(), wt))
-            return wt == f;
+        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);        
+        
+        if (f->get_family_id() == get_family_id())
+            return false;
         else if (m_converter.is_uf2bvuf(f) || m_converter.is_special(f))
             return false;
         else
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 38001b5a6..6c71b1d7d 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -82,9 +82,8 @@ namespace smt {
                 m_th(*th) {}
             virtual ~fpa2bv_converter_wrapped() {}
             virtual void mk_const(func_decl * f, expr_ref & result);
-            virtual void mk_rm_const(func_decl * f, expr_ref & result);
-            void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result);
-            virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);            
+            virtual void mk_rm_const(func_decl * f, expr_ref & result);            
+            virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result);            
 
             virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y);
             virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y);
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index fe9fc2a0f..d8b826525 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include"ast_smt2_pp.h"
+#include"fpa_rewriter.h"
 #include"fpa2bv_model_converter.h"
 
 void fpa2bv_model_converter::display(std::ostream & out) {
@@ -101,17 +102,15 @@ 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 fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
+    unsynch_mpz_manager & mpzm = m_fpa_util.fm().mpz_manager();
+    unsynch_mpq_manager & mpqm = m_fpa_util.fm().mpq_manager();
 
     expr_ref res(m);
     mpf fp_val;
 
-    unsigned ebits = fu.get_ebits(s);
-    unsigned sbits = fu.get_sbits(s);
+    unsigned ebits = m_fpa_util.get_ebits(s);
+    unsigned sbits = m_fpa_util.get_sbits(s);
 
     unsigned sgn_sz = 1;
     unsigned exp_sz = ebits;
@@ -119,47 +118,44 @@ expr_ref fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp,
 
     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);
+    if (sgn) m_bv_util.is_numeral(sgn, sgn_q, sgn_sz);
+    if (exp) m_bv_util.is_numeral(exp, exp_q, exp_sz);
+    if (sig) m_bv_util.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);
+    exp_unbiased_q = exp_q - m_fpa_util.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()), exp_z, sig_z);
+    m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
 
     mpzm.del(sig_z);
 
-    res = fu.mk_value(fp_val);
+    res = m_fpa_util.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;);
-    fu.fm().del(fp_val);
+    m_fpa_util.fm().del(fp_val);
 
     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);
+expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * bv) {
+    SASSERT(m_bv_util.is_bv(bv));
 
-    SASSERT(bu.is_bv(bv));
-
-    unsigned ebits = fu.get_ebits(s);
-    unsigned sbits = fu.get_sbits(s);
+    unsigned ebits = m_fpa_util.get_ebits(s);
+    unsigned sbits = m_fpa_util.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);
+    sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
+    exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
+    sig = m_bv_util.mk_extract(sbits - 2, 0, bv);
 
     expr_ref v_sgn(m), v_exp(m), v_sig(m);
     bv_mdl->eval(sgn, v_sgn);
@@ -169,33 +165,28 @@ expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr *
     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 fpa2bv_model_converter::convert_bv2rm(expr * bv_rm) {
     expr_ref res(m);
     rational bv_val(0);
     unsigned sz = 0;
 
-    if (bu.is_numeral(eval_v, bv_val, sz)) {
+    if (m_bv_util.is_numeral(bv_rm, 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_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break;
+        case BV_RM_TIES_TO_EVEN: res = m_fpa_util.mk_round_nearest_ties_to_even(); break;
+        case BV_RM_TO_NEGATIVE: res = m_fpa_util.mk_round_toward_negative(); break;
+        case BV_RM_TO_POSITIVE: res = m_fpa_util.mk_round_toward_positive(); break;
         case BV_RM_TO_ZERO:
-        default: res = fu.mk_round_toward_zero();
+        default: res = m_fpa_util.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 fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, expr * val) {
     expr_ref res(m);
-
     expr_ref eval_v(m);
 
     if (val && bv_mdl->eval(val, eval_v, true))
@@ -204,10 +195,100 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var,
     return res;
 }
 
-void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
-    fpa_util fu(m);
-    bv_util bu(m);
+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);
+    }
+    else if (m_fpa_util.is_rm(s)) {
+        SASSERT(m_bv_util.get_bv_size(e) == 3);
+        result = convert_bv2rm(bv_mdl, e);
+    }
+    else if (is_app(e)) {
+        app * a = to_app(e);
+        expr_ref_vector new_args(m);
+        for (unsigned i = 0; i < a->get_num_args(); i++)
+            new_args.push_back(rebuild_floats(bv_mdl, a->get_decl()->get_domain()[i], a->get_arg(i)));
+        result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
+    }
+
+    return result;
+}
+
+fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
+    SASSERT(f->get_arity() == 0);
+    array_util arr_util(m);
+
+    array_model am(m);
+    sort_ref_vector array_domain(m);    
+    unsigned arity = f->get_range()->get_num_parameters()-1;
+
+    expr_ref as_arr_mdl(m);
+    as_arr_mdl = bv_mdl->get_const_interp(bv_f);
+    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++)
+        array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast()));
+    sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast());
+        
+    bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl));
+
+    am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
+    am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);    
+    am.bv_fd = bv_f;
+    am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
+    return am;
+}
+
+func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {        
+    SASSERT(f->get_arity() > 0);
+    func_interp * result = 0;
+    sort * rng = f->get_range();
+    sort * const * dmn = f->get_domain();     
+
+    unsigned arity = bv_f->get_arity();
+    func_interp * bv_fi = bv_mdl->get_func_interp(bv_f);
+
+    if (bv_fi != 0) {
+        fpa_rewriter rw(m);
+        expr_ref ai(m);
+        result = alloc(func_interp, m, arity);
+
+        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 * ft_dj = dmn[j];
+                expr * bv_aj = bv_args[j];                
+                ai = rebuild_floats(bv_mdl, ft_dj, bv_aj);
+                m_th_rw(ai);
+                new_args.push_back(ai);
+            }
+
+            expr_ref bv_fres(m), ft_fres(m);
+            bv_fres = bv_fe->get_result();
+            ft_fres = rebuild_floats(bv_mdl, rng, bv_fres);
+            m_th_rw(ft_fres);
+            result->insert_new_entry(new_args.c_ptr(), ft_fres);
+        }
+
+        expr_ref bv_els(m), ft_els(m);
+        bv_els = bv_fi->get_else();
+        ft_els = rebuild_floats(bv_mdl, rng, bv_els);
+        m_th_rw(ft_els);
+        result->set_else(ft_els);        
+    }
+
+    return result;
+}
+
+void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
     for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)
         tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
@@ -233,8 +314,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
          it++) {
         func_decl * f = it->m_key;
         expr_ref pzero(m), nzero(m);
-        pzero = fu.mk_pzero(f->get_range());
-        nzero = fu.mk_nzero(f->get_range());
+        pzero = m_fpa_util.mk_pzero(f->get_range());
+        nzero = m_fpa_util.mk_nzero(f->get_range());
 
         expr_ref pn(m), np(m);
         bv_mdl->eval(it->m_value.first, pn, true);
@@ -244,8 +325,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 
         rational pn_num, np_num;
         unsigned bv_sz;
-        bu.is_numeral(pn, pn_num, bv_sz);
-        bu.is_numeral(np, np_num, bv_sz);
+        m_bv_util.is_numeral(pn, pn_num, bv_sz);
+        m_bv_util.is_numeral(np, np_num, bv_sz);
 
         func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
         expr * pn_args[2] = { pzero, nzero };
@@ -263,7 +344,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     {
         func_decl * var = it->m_key;
         app * val = to_app(it->m_value);
-        SASSERT(fu.is_float(var->get_range()));
+        SASSERT(m_fpa_util.is_float(var->get_range()));
         SASSERT(var->get_range()->get_num_parameters() == 2);
 
         expr_ref sgn(m), sig(m), exp(m);
@@ -271,7 +352,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         bv_mdl->eval(val->get_arg(1), exp, true);
         bv_mdl->eval(val->get_arg(2), sig, true);
 
-        SASSERT(val->is_app_of(fu.get_family_id(), OP_FPA_FP));
+        SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
 
 #ifdef Z3DEBUG
         SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
@@ -301,84 +382,33 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
          it++)
     {
         func_decl * var = it->m_key;
-        SASSERT(fu.is_rm(var->get_range()));
+        SASSERT(m_fpa_util.is_rm(var->get_range()));
         expr * val = it->m_value;
-        SASSERT(is_app_of(val, fu.get_family_id(), OP_FPA_INTERNAL_RM));
+        SASSERT(m_fpa_util.is_rm_bvwrap(val));
         expr * bvval = to_app(val)->get_arg(0);
         expr_ref fv(m);
-        fv = convert_bv2rm(bv_mdl, var, bvval);
+        fv = convert_bv2rm(bv_mdl, bvval);
         TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
         float_mdl->register_decl(var, fv);
         seen.insert(to_app(bvval)->get_decl());
     }
 
     for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
-         it != m_uf2bvuf.end();
-         it++) {
+        it != m_uf2bvuf.end();
+        it++) {
         seen.insert(it->m_value);
 
-        func_decl * f = it->m_key;
-        unsigned arity = f->get_arity();
-        sort * rng = f->get_range();
-
-        if (arity > 0) {
-            func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value);            
-
-            if (bv_fi != 0) {
-                func_interp * flt_fi = alloc(func_interp, m, f->get_arity());
-
-                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];
-                        expr_ref saj(m);
-                        bv_mdl->eval(aj, saj, true);
-
-                        if (fu.is_float(dj))
-                            new_args.push_back(convert_bv2fp(bv_mdl, dj, saj));
-                        else if (fu.is_rm(dj)) {
-                            expr_ref fv(m);
-                            fv = convert_bv2rm(saj);
-                            new_args.push_back(fv);
-                        }
-                        else
-                            new_args.push_back(saj);                        
-                    }
-
-                    expr_ref ret(m);
-                    ret = bv_fe->get_result();
-                    bv_mdl->eval(ret, ret);
-                    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);
-            }
-        }
+        func_decl * f = it->m_key;        
+        if (f->get_arity() == 0)
+        {
+            array_model am = convert_array_func_interp(f, it->m_value, bv_mdl);
+            if (am.new_float_fd) float_mdl->register_decl(am.new_float_fd, am.new_float_fi);
+            if (am.result) float_mdl->register_decl(f, am.result);
+            if (am.bv_fd) seen.insert(am.bv_fd);
+        }            
         else {
-            func_decl * bvf = it->m_value;
-            expr_ref c(m), e(m);
-            c = m.mk_const(bvf);
-            bv_mdl->eval(c, e, true);
-            float_mdl->register_decl(f, e);
-            TRACE("fpa2bv_mc", tout << "model value for " << mk_ismt2_pp(f, m) << " is " << mk_ismt2_pp(e, m) << std::endl;);
+            func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl);
+            if (fmv) float_mdl->register_decl(f, fmv);
         }
     }
 
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index 854543f24..f7c817e1b 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/src/tactic/fpa/fpa2bv_model_converter.h
@@ -19,10 +19,15 @@ Notes:
 #ifndef FPA2BV_MODEL_CONVERTER_H_
 #define FPA2BV_MODEL_CONVERTER_H_
 
+#include"th_rewriter.h"
 #include"fpa2bv_converter.h"
 #include"model_converter.h"
 
 class fpa2bv_model_converter : public model_converter {
+    fpa_util    m_fpa_util;
+    bv_util     m_bv_util;
+    th_rewriter m_th_rw;
+
     ast_manager               & m;
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
@@ -30,7 +35,11 @@ class fpa2bv_model_converter : public model_converter {
     obj_map<func_decl, std::pair<app*, app*> > m_specials;
 
 public:
-    fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) {
+    fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : 
+        m(m),
+        m_fpa_util(m),
+        m_bv_util(m),
+        m_th_rw(m) {
         for (obj_map<func_decl, expr*>::iterator it = conv.m_const2bv.begin();
              it != conv.m_const2bv.end();
              it++)
@@ -95,13 +104,32 @@ public:
     virtual model_converter * translate(ast_translation & translator);
 
 protected:
-    fpa2bv_model_converter(ast_manager & m) : m(m){ }
+    fpa2bv_model_converter(ast_manager & m) : 
+        m(m),
+        m_fpa_util(m),
+        m_bv_util(m),
+        m_th_rw(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;
+    expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig);
+    expr_ref convert_bv2fp(model * bv_mdl, sort * s, expr * bv);
+    expr_ref convert_bv2rm(expr * eval_v);
+    expr_ref convert_bv2rm(model * bv_mdl, expr * val);
+
+    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 convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl);
 };