diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index ce4f2a390..6db0370eb 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -51,7 +51,8 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
     for (auto const& kv : conv.m_uf2bvuf) {
         m_uf2bvuf.insert(kv.m_key, kv.m_value);
         m.inc_ref(kv.m_key);
-        m.inc_ref(kv.m_value);
+        m.inc_ref(kv.m_value.first);
+        m.inc_ref(kv.m_value.second);
     }
     for (auto const& kv : conv.m_min_max_ufs) {
         m_specials.insert(kv.m_key, kv.m_value);
@@ -64,12 +65,18 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) :
 bv2fpa_converter::~bv2fpa_converter() {
     dec_ref_map_key_values(m, m_const2bv);
     dec_ref_map_key_values(m, m_rm_const2bv);
-    dec_ref_map_key_values(m, m_uf2bvuf);
+    for (auto const& kv : m_uf2bvuf) {
+        m.dec_ref(kv.m_key);
+        m.dec_ref(kv.m_value.first);
+        m.dec_ref(kv.m_value.second);
+    }
     for (auto const& kv : m_specials) {
         m.dec_ref(kv.m_key);
         m.dec_ref(kv.m_value.first);
         m.dec_ref(kv.m_value.second);
     }
+    m_uf2bvuf.reset();
+    m_specials.reset();
 }
 
 expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) {
@@ -115,19 +122,19 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
     return res;
 }
 
-expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * bv) {
+expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, expr * bv) {
     SASSERT(m_bv_util.is_bv(bv));
 
     unsigned ebits = m_fpa_util.get_ebits(s);
     unsigned sbits = m_fpa_util.get_sbits(s);
     unsigned bv_sz = sbits + ebits;
 
-    expr_ref bv_num(m);
-    if (m_bv_util.is_numeral(bv))
-        bv_num = bv;
-    else if (!mc->eval(bv->get_decl(), bv_num))
-        bv_num = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(bv));
-
+    expr_ref bv_num(bv, m);
+    if (!m_bv_util.is_numeral(bv) && is_app(bv)) {
+        if (!mc->eval(to_app(bv)->get_decl(), bv_num)) {
+            bv_num = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(bv));
+        }
+    }
     expr_ref sgn(m), exp(m), sig(m);
     sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv_num);
     exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv_num);
@@ -156,27 +163,33 @@ expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) {
         default: res = m_fpa_util.mk_round_toward_zero();
         }
     }
+    else {
+        std::cout << expr_ref(bv_rm, m) << " not converted\n";
+    }
 
     return res;
 }
 
-expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, app * val) {
+expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, expr * val) {
     expr_ref res(m);
 
     if (val) {
         expr_ref eval_v(m);
         if (m_bv_util.is_numeral(val))
             res = convert_bv2rm(val);
-        else if (mc->eval(val->get_decl(), eval_v))
+        else if (is_app(val) && mc->eval(to_app(val)->get_decl(), eval_v))
             res = convert_bv2rm(eval_v);
-        else
+        else {
+            // BUG: doesn't work for parametric definition
+            // needs to be an ite expression.
             res = m_fpa_util.mk_round_toward_zero();
+        }
     }
 
     return res;
 }
 
-expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) {
+expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, expr * e) {
     expr_ref result(m);
     TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for ";
                     if (e) tout << mk_ismt2_pp(e, m);
@@ -206,11 +219,15 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * 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(mc, a->get_decl()->get_domain()[i], to_app(a->get_arg(i))));
+        for (expr* arg : *a) {
+            new_args.push_back(rebuild_floats(mc, m.get_sort(arg), arg));
+        }
         result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr());
     }
-
+    else if (is_var(e)) {
+        result = e;
+    }
+    SASSERT(!result || m.get_sort(result) == s);
     return result;
 }
 
@@ -288,8 +305,8 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
         }
 
         app_ref bv_els(m);
-        bv_els = (app*)bv_fi->get_else();
-        if (bv_els != 0) {
+        bv_els = to_app(bv_fi->get_else());
+        if (bv_els != nullptr) {
             expr_ref ft_els = rebuild_floats(mc, rng, bv_els);
             m_th_rw(ft_els);
             result->set_else(ft_els);
@@ -414,14 +431,16 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta
 
 void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
     for (auto const& kv : m_uf2bvuf) {
-        seen.insert(kv.m_value);
-
         func_decl * f = kv.m_key;
+        func_decl* f_uf = kv.m_value.first;
+        expr*      f_def = kv.m_value.second;
+        seen.insert(f_uf);
+
         if (f->get_arity() == 0)
         {
             array_util au(m);
             if (au.is_array(f->get_range())) {
-                array_model am = convert_array_func_interp(mc, f, kv.m_value);
+                array_model am = convert_array_func_interp(mc, f, f_uf);
                 if (am.new_float_fd) target_model->register_decl(am.new_float_fd, am.new_float_fi);
                 if (am.result) target_model->register_decl(f, am.result);
                 if (am.bv_fd) seen.insert(am.bv_fd);
@@ -430,12 +449,23 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
                 // Just keep.
                 SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range()));
                 expr_ref val(m);
-                if (mc->eval(kv.m_value, val))
+                if (mc->eval(f_uf, val))
                     target_model->register_decl(f, val);
             }
         }
         else if (f->get_family_id() == m_fpa_util.get_fid()) {
-            
+            if (f_def) {
+                func_interp* fi = alloc(func_interp, m, f->get_arity());
+                expr_ref def = rebuild_floats(mc, f->get_range(), to_app(f_def));
+                fi->set_else(def);
+                SASSERT(m.get_sort(def) == f->get_range());
+                target_model->register_decl(f, fi);
+                func_interp* fj = mc->get_func_interp(f_uf);
+                if (fj) {
+                    target_model->register_decl(f_uf, fj->copy());
+                }
+                continue;
+            }
             // kv.m_value contains the model for the unspecified cases of kv.m_key.
             // TBD: instead of mapping the interpretation of f to just the graph for the
             // uninterpreted case, map it to a condition, ite, that filters out the
@@ -446,7 +476,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
             // }
 
 
-            target_model->register_decl(f, convert_func_interp(mc, f, kv.m_value));            
+            target_model->register_decl(f, convert_func_interp(mc, f, f_uf));            
         }
     }
 }
@@ -468,7 +498,7 @@ void bv2fpa_converter::display(std::ostream & out) {
         const symbol & n = kv.m_key->get_name();
         out << "\n  (" << n << " ";
         unsigned indent = n.size() + 4;
-        out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
+        out << mk_ismt2_pp(kv.m_value.first, m, indent) << ")";
     }
     for (auto const& kv : m_specials) {
         const symbol & n = kv.m_key->get_name();
@@ -497,10 +527,12 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
     }
     for (auto const& kv : m_uf2bvuf) {
         func_decl * k = translator(kv.m_key);
-        func_decl * v = translator(kv.m_value);
-        res->m_uf2bvuf.insert(k, v);
+        func_decl * v = translator(kv.m_value.first);
+        expr*       d = translator(kv.m_value.second);
+        res->m_uf2bvuf.insert(k, std::make_pair(v, d));
         translator.to().inc_ref(k);
         translator.to().inc_ref(v);
+        translator.to().inc_ref(d);
     }
     for (auto const& kv : m_specials) {
         func_decl * k = translator(kv.m_key);
diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h
index 3cb7f4c63..778aa1084 100644
--- a/src/ast/fpa/bv2fpa_converter.h
+++ b/src/ast/fpa/bv2fpa_converter.h
@@ -34,7 +34,7 @@ class bv2fpa_converter {
 
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
-    obj_map<func_decl, func_decl*>  m_uf2bvuf;
+    obj_map<func_decl, std::pair<func_decl*, expr*>>  m_uf2bvuf;
     obj_map<func_decl, std::pair<app*, app*> > m_specials;
 
 public:
@@ -46,9 +46,9 @@ public:
     bv2fpa_converter * translate(ast_translation & translator);
 
     expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig);
-    expr_ref convert_bv2fp(model_core * mc, sort * s, app * bv);
+    expr_ref convert_bv2fp(model_core * mc, sort * s, expr * bv);
     expr_ref convert_bv2rm(expr * eval_v);
-    expr_ref convert_bv2rm(model_core * mc, app * val);
+    expr_ref convert_bv2rm(model_core * mc, expr * val);
 
     void convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
     void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
@@ -56,7 +56,7 @@ public:
     void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen);
 
     func_interp * convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
-    expr_ref rebuild_floats(model_core * mc, sort * s, app * e);
+    expr_ref rebuild_floats(model_core * mc, sort * s, expr * e);
 
     class array_model {
     public:
@@ -70,4 +70,4 @@ public:
     array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);
 };
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 26d5dc33a..4407a824f 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -93,8 +93,8 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
 
 void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
     if (m_util.is_fp(t) && m_util.is_fp(f)) {
-        expr *t_sgn, *t_sig, *t_exp;
-        expr *f_sgn, *f_sig, *f_exp;
+        expr_ref t_sgn(m), t_sig(m), t_exp(m);
+        expr_ref f_sgn(m), f_sig(m), f_exp(m);
         split_fp(t, t_sgn, t_exp, t_sig);
         split_fp(f, f_sgn, f_exp, f_sig);
 
@@ -695,7 +695,7 @@ void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args,
 }
 
 void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
-    expr * sgn, *sig, *e;
+    expr_ref sgn(m), sig(m), e(m);
     split_fp(x, sgn, e, sig);
     expr_ref c(m), nsgn(m);
     mk_is_nan(x, c);
@@ -1075,8 +1075,8 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
     // exp(x) < exp(y) -> x
     unsigned ebits = m_util.get_ebits(s);
     unsigned sbits = m_util.get_sbits(s);
-    expr * x_sgn, *x_sig, *x_exp;
-    expr * y_sgn, *y_sig, *y_exp;
+    expr_ref x_sgn(m), x_sig(m), x_exp(m);
+    expr_ref y_sgn(m), y_sig(m), y_exp(m);
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
     expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m);
@@ -1214,7 +1214,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args,
 }
 
 void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
-    expr * sgn, *sig, *exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(x, sgn, exp, sig);
     result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig);
 }
@@ -1224,8 +1224,8 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
 
     expr * x = args[0], * y = args[1];
 
-    expr * x_sgn, *x_sig, *x_exp;
-    expr * y_sgn, *y_sig, *y_exp;
+    expr_ref x_sgn(m), x_sig(m), x_exp(m);
+    expr_ref y_sgn(m), y_sig(m), y_exp(m);
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
 
@@ -1269,8 +1269,8 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
 
     expr * x = args[0], *y = args[1];
 
-    expr * x_sgn, *x_sig, *x_exp;
-    expr * y_sgn, *y_sig, *y_exp;
+    expr_ref x_sgn(m), x_sig(m), x_exp(m);
+    expr_ref y_sgn(m), y_sig(m), y_exp(m);
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
 
@@ -2150,8 +2150,8 @@ void fpa2bv_converter::mk_float_eq(sort * s, expr_ref & x, expr_ref & y, expr_re
     mk_is_zero(y, y_is_zero);
     m_simp.mk_and(x_is_zero, y_is_zero, c2);
 
-    expr * x_sgn, * x_sig, * x_exp;
-    expr * y_sgn, * y_sig, * y_exp;
+    expr_ref x_sgn(m), x_sig(m), x_exp(m);
+    expr_ref y_sgn(m), y_sig(m), y_exp(m);
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
 
@@ -2189,8 +2189,8 @@ void fpa2bv_converter::mk_float_lt(sort * s, expr_ref & x, expr_ref & y, expr_re
     mk_is_zero(y, y_is_zero);
     m_simp.mk_and(x_is_zero, y_is_zero, c2);
 
-    expr * x_sgn, * x_sig, * x_exp;
-    expr * y_sgn, * y_sig, * y_exp;
+    expr_ref x_sgn(m), x_sig(m), x_exp(m);
+    expr_ref y_sgn(m), y_sig(m), y_exp(m);
     split_fp(x, x_sgn, x_exp, x_sig);
     split_fp(y, y_sgn, y_exp, y_sig);
 
@@ -3140,7 +3140,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     expr_ref x(m), x_is_nan(m);
-    expr * sgn, * s, * e;
+    expr_ref sgn(m), s(m), e(m);
     x = args[0];
     split_fp(x, sgn, e, s);
     mk_is_nan(x, x_is_nan);
@@ -3201,6 +3201,30 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     sort * xs = m.get_sort(x);
     sort * bv_srt = f->get_range();
 
+#if 0
+    // for this to work, the following is required:
+    // 1. split_fp should succeed even if the argument does not satisfy is_fp
+    //    we would need functions to access the sgn, exp and sig fields
+    // 2. an inverse of bv2rm, here called rm2bv. 
+    expr_ref arg1(m), arg2(m), _rm(m);
+    
+    var_subst vsubst(m, false);
+    expr* def = get_bv_def(f);
+    if (def) {
+        result = vsubst(def, 2, args);
+        return;
+    }    
+    arg1 = m.mk_var(0, m.get_sort(args[0]));
+    arg2 = m.mk_var(1, m.get_sort(args[1]));
+    _rm = m_util.mk_rm2bv(arg1);    
+    rm = _rm;
+    x = arg2;
+#endif
+
+    expr_ref sgn(m), sig(m), exp(m), lz(m);
+    unpack(x, sgn, sig, exp, lz, true);
+    
+
     unsigned ebits = m_util.get_ebits(xs);
     unsigned sbits = m_util.get_sbits(xs);
     unsigned bv_sz = (unsigned)f->get_parameter(0).get_int();
@@ -3230,8 +3254,6 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     dbg_decouple("fpa2bv_to_bv_c2", c2);
 
     // Otherwise...
-    expr_ref sgn(m), sig(m), exp(m), lz(m);
-    unpack(x, sgn, sig, exp, lz, true);
 
     dbg_decouple("fpa2bv_to_bv_sgn", sgn);
     dbg_decouple("fpa2bv_to_bv_sig", sig);
@@ -3348,6 +3370,10 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
     result = m.mk_ite(c2, v2, result);
     result = m.mk_ite(c1, v1, result);
 
+#if 0
+    set_bv_def(f, result);    
+    result = vsubst(result, 2, args);
+#endif
     SASSERT(is_well_sorted(m, result));
 }
 
@@ -3416,34 +3442,23 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
     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);
-    sgn = to_app(e)->get_arg(0);
-    exp = to_app(e)->get_arg(1);
-    sig = to_app(e)->get_arg(2);
-}
 
 void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const {
-    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);
+    expr* e_sgn = nullptr, *e_exp = nullptr, *e_sig = nullptr;
+    VERIFY(m_util.is_fp(e, e_sgn, e_exp, e_sig));
     sgn = e_sgn;
     exp = e_exp;
     sig = e_sig;
 }
 
 void fpa2bv_converter::join_fp(expr * e, expr_ref & res) {
-    SASSERT(m_util.is_fp(e));
-    SASSERT(to_app(e)->get_num_args() == 3);
-    expr *sgn, *exp, *sig;
+    expr_ref sgn(m), exp(m), sig(m);
     split_fp(e, sgn, exp, sig);
     res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig);
 }
 
 void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
 
     // exp == 1^n , sig != 0
@@ -3458,7 +3473,7 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
     expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
     mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
@@ -3501,7 +3516,7 @@ void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
     expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
     mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
@@ -3512,7 +3527,7 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
     expr_ref e_is_zero(m), eq(m), one_1(m);
     mk_is_zero(e, e_is_zero);
@@ -3522,7 +3537,7 @@ void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
     expr_ref e_is_zero(m), eq(m), nil_1(m);
     mk_is_zero(e, e_is_zero);
@@ -3532,7 +3547,7 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
-    expr * sgn, *sig, *exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
 
     expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
@@ -3545,7 +3560,7 @@ void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
 }
 
 void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
-    expr * sgn, * sig, * exp;
+    expr_ref sgn(m), sig(m), exp(m);
     split_fp(e, sgn, exp, sig);
 
     expr_ref is_special(m), is_denormal(m), p(m), is_zero(m);
@@ -3779,7 +3794,7 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
     // CMW: This works only for quantifier-free formulas.
     if (m_util.is_fp(e)) {
         expr_ref new_bv(m);
-        expr *e_sgn, *e_sig, *e_exp;
+        expr_ref e_sgn(m), e_sig(m), e_exp(m);
         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;
@@ -4173,24 +4188,52 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
 void fpa2bv_converter::reset() {
     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);
+    for (auto const& kv : m_uf2bvuf) {
+        m.dec_ref(kv.m_key);
+        m.dec_ref(kv.m_value.first);
+        m.dec_ref(kv.m_value.second);
+    }
     for (auto const& kv : m_min_max_ufs) {
         m.dec_ref(kv.m_key);
         m.dec_ref(kv.m_value.first);
         m.dec_ref(kv.m_value.second);
     }
+    m_uf2bvuf.reset();
     m_min_max_ufs.reset();
     m_extra_assertions.reset();
 }
 
 func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
-    func_decl * res;
+    std::pair<func_decl*, expr*> res;
     if (!m_uf2bvuf.find(f, res)) {
-        res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
-        m_uf2bvuf.insert(f, res);
+        res.first = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
+        res.second = nullptr;
         m.inc_ref(f);
-        m.inc_ref(res);
-        TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;);
+        m.inc_ref(res.first);
+        m_uf2bvuf.insert(f, res);
+        TRACE("fpa2bv", tout << "New UF func_decl: " << res.first->get_id() << std::endl << mk_ismt2_pp(res.first, m) << std::endl;);
     }
-    return res;
+    return res.first;
+}
+
+expr* fpa2bv_converter::get_bv_def(func_decl* f) {
+    std::pair<func_decl*, expr*> res(nullptr, nullptr);
+    m_uf2bvuf.find(f, res);
+    TRACE("fpa2bv", tout << "get_bv_def " << mk_ismt2_pp(res.first, m) << " " << res.second << std::endl;);
+    return res.second;
+}
+
+/**
+   \brief expand the definition of bit-vector function f
+   as an expression of what is defined and what is not
+   defined.
+*/
+void fpa2bv_converter::set_bv_def(func_decl* f, expr* def) {
+    auto res = m_uf2bvuf[f];
+    SASSERT(res.first);
+    SASSERT(!res.second);
+    res.second = def;
+    m.inc_ref(def);
+    m_uf2bvuf.insert(f, res);
+
 }
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 812c24155..85a866bc0 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -35,7 +35,7 @@ class fpa2bv_converter {
 public:
     typedef obj_map<func_decl, std::pair<app *, app *> > special_t;
     typedef obj_map<func_decl, expr*> const2bv_t;
-    typedef obj_map<func_decl, func_decl*> uf2bvuf_t;
+    typedef obj_map<func_decl, std::pair<func_decl*, expr*> > uf2bvuf_t;
 
 protected:
     ast_manager              & m;
@@ -74,7 +74,7 @@ public:
 
     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 * & sgn, expr * & exp, expr * & sig) const;
     void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
     void join_fp(expr * e, expr_ref & res);
 
@@ -219,6 +219,9 @@ private:
     void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
 
     func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range);
+    void set_bv_def(func_decl * f, expr* def);
+    expr* get_bv_def(func_decl * f);
+
     expr_ref nan_wrap(expr * n);
 
     expr_ref extra_quantify(expr * e);
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index 9b961fb52..dbd2faf35 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -226,7 +226,7 @@ public:
     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); }
+    bool is_fp(expr const * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
     unsigned get_ebits(sort * s) const;
     unsigned get_sbits(sort * s) const;
 
@@ -357,6 +357,8 @@ public:
     bool is_to_ieee_bv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV; }
 
     bool contains_floats(ast * a);
+
+    MATCH_TERNARY(is_fp);
 };
 
 #endif
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 30babdd33..e348c8859 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -87,7 +87,7 @@ class fpa2bv_tactic : public tactic {
                         // Inject auxiliary lemmas that fix e to the one and only NaN value,
                         // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
                         // has a value to propagate.
-                        expr * sgn, *sig, *exp;
+                        expr_ref sgn(m), sig(m), exp(m);
                         m_conv.split_fp(new_curr, sgn, exp, sig);
                         result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
                         result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_bv_neg(m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(exp)))));