diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 96480890d..cda3bd27e 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -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,281 +229,70 @@ 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);
-
-    sort * found_sort;
-    if (m_subst_sorts.find(s, found_sort)) {
-        ns = found_sort;
+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;);
     }
-    else {
-        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 if (m_array_util.is_array(s)) {
-            SASSERT(s->get_num_parameters() > 0);
-            vector<parameter> new_params;
-            unsigned num_params = s->get_num_parameters();
-            for (unsigned i = 0; i < num_params; i++)
-            {
-                parameter const & pi = s->get_parameter(i);
-                if (pi.is_ast() && is_sort(pi.get_ast())) {
-                    sort_ref nsrt(m);
-                    nsrt = replace_float_sorts(to_sort(pi.get_ast()));
-                    parameter np((ast*)nsrt);
-                    new_params.push_back(np);
-                }
-                else
-                    new_params.push_back(pi);
-            }
-            ns = m.mk_sort(s->get_family_id(), s->get_decl_kind(), new_params.size(), new_params.c_ptr());
-        }
-        else if (m_dt_util.is_datatype(s)) {
-            TRACE("fpa2bv", tout << "datatype:"; m_dt_util.display_datatype(s, tout); );
-            bool is_recursive = m_dt_util.is_recursive(s);
-            SASSERT(!is_recursive);
-            ptr_vector<func_decl> const * cs = m_dt_util.get_datatype_constructors(s);
-            ptr_vector<constructor_decl> new_css;
-            bool has_news = false;
-            for (unsigned i = 0; i < cs->size(); i++) {
-                func_decl * cf = cs->get(i);
-                func_decl * rf = m_dt_util.get_constructor_recognizer(cf);
-                ptr_vector<func_decl> new_rf;
-                ptr_vector<func_decl> const * cas = m_dt_util.get_constructor_accessors(cf);
-                ptr_vector<accessor_decl> new_cas;
-                for (unsigned j = 0; j < cas->size(); j++) {
-                    func_decl * ca = cas->get(j);
-                    sort * s1 = ca->get_range();
-                    sort_ref s1r(m);
-                    s1r = replace_float_sorts(s1);
-
-                    symbol name(ca->get_name());
-                    if (s1r != s1) {
-                        std::stringstream ss;
-                        ss << name << "!fpa2bv";
-                        name = symbol(ss.str().c_str());
-                        has_news = true;
-                    }
-
-                    accessor_decl * ad = mk_accessor_decl(name, type_ref(s1r.get()));
-                    new_cas.push_back(ad);
-                }
-
-                constructor_decl * cd = 0;
-                symbol name(cf->get_name());
-                symbol rf_name(rf->get_name());
-
-                if (has_news) {
-                    std::stringstream ss;
-                    ss << name << "!fpa2bv";
-                    name = symbol(ss.str().c_str());
-                    std::stringstream ss2;
-                    ss2 << rf_name << "!fpa2bv";
-                    rf_name = symbol(ss2.str().c_str());
-                }
-
-                cd = mk_constructor_decl(name, rf_name, new_cas.size(), new_cas.c_ptr());
-                new_css.push_back(cd);
-            }
-
-            if (has_news) {
-                std::stringstream ss;
-                ss << s->get_name() << "!fpa2bv";
-                symbol name(ss.str().c_str());
-                datatype_decl * dtd = mk_datatype_decl(name, new_css.size(), new_css.c_ptr());                
-                datatype_decl_plugin * dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(m.mk_family_id("datatype")));
-                sort_ref_vector sorts(m);
-                bool is_ok = dtp->mk_datatypes(1, &dtd, sorts);
-                SASSERT(is_ok);
-                ns = sorts.get(0);
-                TRACE("fpa2bv", tout << "new datatype:"; m_dt_util.display_datatype(ns, tout); );
-            }
-            else
-                ns = s;
-        }
-        else if (m_seq_util.is_seq(s)) {
-            NOT_IMPLEMENTED_YET();
-        }
-        else
-            ns = s;
-
-        if (ns != s) {
-            m_subst_sorts.insert(s, ns);
-            m.inc_ref(s);
-            m.inc_ref(ns);
-        }
-    }
-
-    SASSERT(ns != 0);
-    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 << "Old domain:" << std::endl;
-                            for (unsigned i = 0; i < f->get_arity(); i++) {
-                                if (m_dt_util.is_datatype(f->get_domain(i)))
-                                    m_dt_util.display_datatype(f->get_domain(i), tout);
-                                else
-                                    tout << mk_ismt2_pp(f->get_domain(i), m);
-                                tout << std::endl;
-                            });
-
-            TRACE("fpa2bv", tout << "New domain:" << std::endl;
-                            for (unsigned i = 0; i < new_domain.size(); i++) {
-                                if (m_dt_util.is_datatype(new_domain[i]))
-                                    m_dt_util.display_datatype(new_domain[i], tout);
-                                else
-                                    tout << mk_ismt2_pp(new_domain[i], m);
-                                tout << std::endl;
-                            });
-            
-            vector<parameter> new_params;
-            for (unsigned i = 0; i < f->get_num_parameters(); i++) {
-                parameter const & pi = f->get_parameter(i);
-                if (pi.is_ast() && is_sort(pi.get_ast())) {
-                    sort_ref ns(m);
-                    ns = replace_float_sorts(to_sort(pi.get_ast()));
-                    parameter np((ast*)ns);
-                    new_params.push_back(np);
-                }
-                else
-                    new_params.push_back(pi);
-            }
-
-            res = m.mk_func_decl(f->get_family_id(), f->get_decl_kind(),
-                                 new_params.size(), new_params.c_ptr(),                                 
-                                 new_domain.size(), new_domain.c_ptr(), new_range);
-            TRACE("fpa2bv", tout << "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);
-        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]));
-
-
-    CTRACE("fpa2bv", num > 0, 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);
-
-    TRACE("fpa2bv", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; 
-                    tout << "old: " << mk_ismt2_pp(f->get_range(), m) << std::endl; 
-                    tout << "new: " << mk_ismt2_pp(m.get_sort(result), m) << std::endl;
-                    tout << "equal: " << (f->get_range() == m.get_sort(result)) << std::endl;);
+    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));
 }
 
@@ -526,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);
@@ -547,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) {
@@ -563,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) {
@@ -579,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) {
@@ -595,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) {
@@ -611,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) {
@@ -633,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,
@@ -916,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) {
@@ -1333,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) {
@@ -1404,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);
@@ -1491,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);
@@ -2389,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]) &&
@@ -2421,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]) &&
@@ -2648,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)) {
@@ -2681,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);
@@ -3447,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);
@@ -3814,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) {
@@ -4212,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; );
 }
@@ -4221,7 +3966,6 @@ void fpa2bv_converter::reset(void) {
     dec_ref_map_key_values(m, m_const2bv);
     dec_ref_map_key_values(m, m_rm_const2bv);
     dec_ref_map_key_values(m, m_uf2bvuf);
-    dec_ref_map_key_values(m, m_subst_sorts);
     for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
         it != m_specials.end();
         it++) {
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 17648917f..19c5b3352 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -48,8 +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<sort, sort*>       m_subst_sorts;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;    
 
     obj_map<func_decl, std::pair<app *, app *> > m_specials;
 
@@ -68,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;
 
@@ -199,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 2a66da8d7..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);
@@ -166,12 +169,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
             NOT_IMPLEMENTED_YET();
         }
     }
-    else if (f->get_arity() > 0 && !m_conv.is_float_family(f)) {
-        expr_ref q(m().mk_app(f, num, args), m());
-        if (m_conv.fu().contains_floats(q)) {
-            m_conv.mk_function(f, num, args, result);
-            return BR_DONE;
-        }
+    else 
+    {
+        SASSERT(!m_conv.is_float_family(f));
+        m_conv.mk_function(f, num, args, result);
+        return BR_DONE;
     }
 
     return BR_FAILED;
@@ -247,10 +249,9 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
         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);
+        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.h b/src/ast/fpa_decl_plugin.h
index 725e7371a..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);
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 0268d2353..c6c302ded 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);
@@ -380,7 +377,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 +386,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 db8b13913..64423f224 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -46,12 +46,6 @@ void fpa2bv_model_converter::display(std::ostream & out) {
         unsigned indent = n.size() + 4;
         out << mk_ismt2_pp(it->m_value, m, indent) << ")";
     }
-    for (obj_map<sort, sort*>::iterator it = m_subst_sorts.begin();
-         it != m_subst_sorts.end();
-         it++) {
-        out << "\n  " << mk_ismt2_pp(it->m_key, m) << " -> ";
-        out << mk_ismt2_pp(it->m_value, m);
-    }    
     for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
          it != m_specials.end();
          it++) {
@@ -95,15 +89,6 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
         translator.to().inc_ref(k);
         translator.to().inc_ref(v);
     }
-    for (obj_map<sort, sort*>::iterator it = m_subst_sorts.begin();
-         it != m_subst_sorts.end();
-         it++) {
-        sort * k = translator(it->m_key);
-        sort * v = translator(it->m_value);
-        res->m_subst_sorts.insert(k, v);
-        translator.to().inc_ref(k);
-        translator.to().inc_ref(v);
-    }
     for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
          it != m_specials.end();
          it++) {
@@ -213,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);
@@ -245,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++)
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index bb7c78067..0e92841de 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/src/tactic/fpa/fpa2bv_model_converter.h
@@ -32,7 +32,6 @@ class fpa2bv_model_converter : public model_converter {
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
     obj_map<func_decl, func_decl*>  m_uf2bvuf;
-    obj_map<sort, sort*>        m_subst_sorts;
     obj_map<func_decl, std::pair<app*, app*> > m_specials;
 
 public:
@@ -65,14 +64,6 @@ public:
             m.inc_ref(it->m_key);
             m.inc_ref(it->m_value);
         }
-        for (obj_map<sort, sort*>::iterator it = conv.m_subst_sorts.begin();
-            it != conv.m_subst_sorts.end();
-            it++)
-        {
-            m_subst_sorts.insert(it->m_key, it->m_value);
-            m.inc_ref(it->m_key);
-            m.inc_ref(it->m_value);
-        }
         for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = conv.m_specials.begin();
              it != conv.m_specials.end();
              it++) {
@@ -87,7 +78,6 @@ public:
         dec_ref_map_key_values(m, m_const2bv);
         dec_ref_map_key_values(m, m_rm_const2bv);
         dec_ref_map_key_values(m, m_uf2bvuf);
-        dec_ref_map_key_values(m, m_subst_sorts);
         for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
              it != m_specials.end();
              it++) {
@@ -128,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);