diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 998c10d58..968f5dd9a 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -4254,3 +4254,107 @@ func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sor
     }
     return res;
 }
+
+void fpa2bv_converter_wrapped::mk_const(func_decl* f, expr_ref& result) {
+    SASSERT(f->get_family_id() == null_family_id);
+    SASSERT(f->get_arity() == 0);
+    expr* r;
+    if (m_const2bv.find(f, r)) {
+        result = r;
+    }
+    else {
+        sort* s = f->get_range();
+        expr_ref bv(m);
+        bv = wrap(m.mk_const(f));
+        unsigned bv_sz = m_bv_util.get_bv_size(bv);
+        unsigned sbits = m_util.get_sbits(s);
+        SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
+        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_util.is_float(result));
+        m_const2bv.insert(f, result);
+        m.inc_ref(f);
+        m.inc_ref(result);
+    }
+}
+
+app_ref fpa2bv_converter_wrapped::wrap(expr* e) {
+    SASSERT(m_util.is_float(e) || m_util.is_rm(e));
+    SASSERT(!m_util.is_bvwrap(e));
+    app_ref res(m);
+
+    if (m_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) };
+        expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);        
+        m_rw(tmp);
+        res = to_app(tmp);
+    }
+    else {
+        sort* es = m.get_sort(e);
+
+        sort_ref bv_srt(m);
+        if (is_rm(es))
+            bv_srt = m_bv_util.mk_sort(3);
+        else {
+            SASSERT(m_converter.is_float(es));
+            unsigned ebits = m_util.get_ebits(es);
+            unsigned sbits = m_util.get_sbits(es);
+            bv_srt = m_bv_util.mk_sort(ebits + sbits);
+        }
+
+        func_decl_ref wrap_fd(m);
+        wrap_fd = m.mk_func_decl(m_util.get_family_id(), OP_FPA_BVWRAP, 0, nullptr, 1, &es, bv_srt);
+        res = m.mk_app(wrap_fd, e);
+    }
+
+    return res;
+}
+
+app_ref fpa2bv_converter_wrapped::unwrap(expr* e, sort* s) {
+    SASSERT(!m_util.is_fp(e));
+    SASSERT(m_bv_util.is_bv(e));
+    SASSERT(m_util.is_float(s) || m_util.is_rm(s));
+    app_ref res(m);
+
+    unsigned bv_sz = m_bv_util.get_bv_size(e);
+
+    if (m_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_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_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_util.mk_round_toward_negative(),
+                    m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_util.mk_round_toward_positive(),
+                        m_util.mk_round_toward_zero()))));
+    }
+    else {
+        SASSERT(m_util.is_float(s));
+        unsigned sbits = m_util.get_sbits(s);
+        SASSERT(bv_sz == m_util.get_ebits(s) + sbits);
+        res = m_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;
+}
+
+
+void fpa2bv_converter_wrapped::mk_rm_const(func_decl* f, expr_ref& result) {
+    SASSERT(f->get_family_id() == null_family_id);
+    SASSERT(f->get_arity() == 0);
+    expr* r;
+    if (m_rm_const2bv.find(f, r)) {
+        result = r;
+    }
+    else {
+        SASSERT(is_rm(f->get_range()));
+        expr_ref bv(m);
+        bv = wrap(m.mk_const(f));
+        result = m_util.mk_bv2rm(bv);
+        m_rm_const2bv.insert(f, result);
+        m.inc_ref(f);
+        m.inc_ref(result);
+    }
+}
+
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index b6675e8e1..1c48fa7cb 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -29,6 +29,7 @@ Notes:
 #include "ast/pb_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 
 class fpa2bv_converter {
 public:
@@ -39,7 +40,6 @@ public:
 protected:
     ast_manager              & m;
     bool_rewriter              m_simp;
-    fpa_util                   m_util;
     bv_util                    m_bv_util;
     arith_util                 m_arith_util;
     datatype_util              m_dt_util;
@@ -58,6 +58,8 @@ protected:
     friend class bv2fpa_converter;
 
 public:
+    fpa_util                   m_util;
+
     fpa2bv_converter(ast_manager & m);
     ~fpa2bv_converter();
 
@@ -224,3 +226,18 @@ private:
     expr_ref extra_quantify(expr * e);
 };
 
+class fpa2bv_converter_wrapped : public fpa2bv_converter {
+    th_rewriter& m_rw;
+ public:
+
+    fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
+        fpa2bv_converter(m),
+        m_rw(rw) {}
+    virtual ~fpa2bv_converter_wrapped() {}
+    void mk_const(func_decl * f, expr_ref & result) override;
+    void mk_rm_const(func_decl * f, expr_ref & result) override;
+    app_ref wrap(expr * e);
+    app_ref unwrap(expr * e, sort * s);
+    
+};
+
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 962deda65..d53d31ce0 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -271,3 +271,77 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
 }
 
 template class rewriter_tpl<fpa2bv_rewriter_cfg>;
+
+expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) {
+    TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m) << std::endl;);
+    expr_ref res(m_cfg.m());
+    proof_ref pr(m_cfg.m());
+    (*this)(e, res);
+    rw(res, res);
+    SASSERT(is_app(res));
+    SASSERT(m.is_bool(res));
+    return res;
+}
+
+expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
+    SASSERT(m_fpa_util.is_rm(e) || m_fpa_util.is_float(e));
+    ast_manager& m = m_cfg.m();
+    
+    expr_ref e_conv(m), res(m);
+    proof_ref pr(m);
+    
+    (*this)(e, e_conv);
+    
+    TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
+          tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
+    
+    if (m_cfg.m_conv.m_util.is_rm(e)) {
+        SASSERT(m_cfg.m_conv.m_util.is_bv2rm(e_conv));
+        expr_ref bv_rm(m);
+        rw(to_app(e_conv)->get_arg(0), bv_rm);
+        res = m_cfg.m_conv.m_util.mk_bv2rm(bv_rm);
+    }
+    else if (m_cfg.m_conv.m_util.is_float(e)) {
+        SASSERT(m_cfg.m_conv.m_util.is_fp(e_conv));
+        expr_ref sgn(m), sig(m), exp(m);
+        m_cfg.m_conv.split_fp(e_conv, sgn, exp, sig);
+        rw(sgn);
+        rw(exp);
+        rw(sig);
+        res = m_cfg.m_conv.m_util.mk_fp(sgn, exp, sig);
+    }
+    else
+        UNREACHABLE();
+    
+    return res;
+}
+
+expr_ref fpa2bv_rewriter::convert_conversion_term(th_rewriter& rw, expr * e) {
+    SASSERT(to_app(e)->get_family_id() == m_cfg.m_conv.m_util.get_family_id());
+    /* This is for the conversion functions fp.to_* */
+    expr_ref res(m_cfg.m());
+    (*this)(e, res);
+    rw(res, res);
+    return res;
+}
+
+expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
+    ast_manager& m = m_cfg.m();
+    expr_ref res(m);
+    TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
+    
+    if (m_cfg.m_conv.m_util.is_fp(e))
+        res = e;
+    else if (m.is_bool(e))
+        res = convert_atom(rw, e);
+    else if (m_cfg.m_conv.m_util.is_float(e) || m_cfg.m_conv.m_util.is_rm(e))
+        res = convert_term(rw, e);
+    else
+        res = convert_conversion_term(rw, e);
+    
+    TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
+          tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
+          mk_ismt2_pp(res, m) << std::endl;);
+    
+    return res;
+}
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 754061938..2f1db4c37 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -74,5 +74,10 @@ struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
         rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
         m_cfg(m, c, p) {
     }
+
+    expr_ref convert_atom(th_rewriter& rw, expr * e);
+    expr_ref convert_term(th_rewriter& rw, expr * e);
+    expr_ref convert_conversion_term(th_rewriter& rw, expr * e);
+    expr_ref convert(th_rewriter& rw, expr * e);
 };
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index aa458b672..eeee6297f 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -42,53 +42,12 @@ namespace smt {
         }
     };
 
-    void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) {
-        SASSERT(f->get_family_id() == null_family_id);
-        SASSERT(f->get_arity() == 0);
-        expr * r;
-        if (m_const2bv.find(f, r)) {
-            result = r;
-        }
-        else {
-            sort * s = f->get_range();
-            expr_ref bv(m);
-            bv = m_th.wrap(m.mk_const(f));
-            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);
-            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);
-            m.inc_ref(result);
-        }
-    }
-
-    void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
-        SASSERT(f->get_family_id() == null_family_id);
-        SASSERT(f->get_arity() == 0);
-        expr * r;
-        if (m_rm_const2bv.find(f, r)) {
-            result = r;
-        }
-        else {
-            SASSERT(is_rm(f->get_range()));
-            expr_ref bv(m);
-            bv = m_th.wrap(m.mk_const(f));
-            result = m_util.mk_bv2rm(bv);
-            m_rm_const2bv.insert(f, result);
-            m.inc_ref(f);
-            m.inc_ref(result);
-        }
-    }
 
     theory_fpa::theory_fpa(context& ctx) :
         theory(ctx, ctx.get_manager().mk_family_id("fpa")),
-        m_converter(ctx.get_manager(), this),
-        m_rw(ctx.get_manager(), m_converter, params_ref()),
         m_th_rw(ctx.get_manager()),
+        m_converter(ctx.get_manager(), m_th_rw),
+        m_rw(ctx.get_manager(), m_converter, params_ref()),
         m_trail_stack(*this),
         m_fpa_util(m_converter.fu()),
         m_bv_util(m_converter.bu()),
@@ -224,117 +183,6 @@ namespace smt {
         return result;
     }
 
-    app_ref theory_fpa::wrap(expr * e) {
-        SASSERT(m_fpa_util.is_float(e) || m_fpa_util.is_rm(e));
-        SASSERT(!m_fpa_util.is_bvwrap(e));
-        app_ref res(m);
-
-        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) };
-            expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
-            m_th_rw(tmp);
-            res = to_app(tmp);
-        }
-        else {
-            sort * es = m.get_sort(e);
-
-            sort_ref bv_srt(m);
-            if (m_converter.is_rm(es))
-                bv_srt = m_bv_util.mk_sort(3);
-            else {
-                SASSERT(m_converter.is_float(es));
-                unsigned ebits = m_fpa_util.get_ebits(es);
-                unsigned sbits = m_fpa_util.get_sbits(es);
-                bv_srt = m_bv_util.mk_sort(ebits + sbits);
-            }
-
-            func_decl_ref wrap_fd(m);
-            wrap_fd = m.mk_func_decl(get_family_id(), OP_FPA_BVWRAP, 0, nullptr, 1, &es, bv_srt);
-            res = m.mk_app(wrap_fd, e);
-        }
-
-        return res;
-    }
-
-    app_ref theory_fpa::unwrap(expr * e, sort * s) {
-        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));
-        app_ref res(m);
-
-        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) {
-        TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m) << std::endl;);
-        expr_ref res(m);
-        proof_ref pr(m);
-        m_rw(e, res);
-        m_th_rw(res, res);
-        SASSERT(is_app(res));
-        SASSERT(m.is_bool(res));
-        return res;
-    }
-
-    expr_ref theory_fpa::convert_term(expr * e) {
-        SASSERT(m_fpa_util.is_rm(e) || m_fpa_util.is_float(e));
-
-        expr_ref e_conv(m), res(m);
-        proof_ref pr(m);
-
-        m_rw(e, e_conv);
-
-        TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
-                              tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
-
-        if (m_fpa_util.is_rm(e)) {
-            SASSERT(m_fpa_util.is_bv2rm(e_conv));
-            expr_ref bv_rm(m);
-            m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
-            res = m_fpa_util.mk_bv2rm(bv_rm);
-        }
-        else if (m_fpa_util.is_float(e)) {
-            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);
-            m_th_rw(exp);
-            m_th_rw(sig);
-            res = m_fpa_util.mk_fp(sgn, exp, sig);
-        }
-        else
-            UNREACHABLE();
-
-        return res;
-    }
-
-    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_* */
-        expr_ref res(m);
-        m_rw(e, res);
-        m_th_rw(res, res);
-        return res;
-    }
 
     expr_ref theory_fpa::convert(expr * e)
     {
@@ -349,14 +197,7 @@ namespace smt {
                 mk_ismt2_pp(res, m) << std::endl;);
         }
         else {
-            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))
-                res = convert_term(e);
-            else
-                res = convert_conversion_term(e);
+            res = m_rw.convert(m_th_rw, e);
 
             TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
                                   tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
@@ -421,7 +262,7 @@ namespace smt {
         literal l(ctx.mk_bool_var(atom));
         ctx.set_var_theory(l.var(), get_id());
 
-        expr_ref bv_atom(convert_atom(atom));
+        expr_ref bv_atom(m_rw.convert_atom(m_th_rw, atom));
         expr_ref bv_atom_w_side_c(m), atom_eq(m);
         bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
         m_th_rw(bv_atom_w_side_c);
@@ -486,7 +327,7 @@ namespace smt {
                 if (!m_fpa_util.is_bv2rm(owner)) {
                     expr_ref valid(m), limit(m);
                     limit = m_bv_util.mk_numeral(4, 3);
-                    valid = m_bv_util.mk_ule(wrap(owner), limit);
+                    valid = m_bv_util.mk_ule(m_converter.wrap(owner), limit);
                     assert_cnstr(valid);
                 }
             }
@@ -622,7 +463,7 @@ namespace smt {
         if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
             if (!m_fpa_util.is_fp(n)) {
                 expr_ref wrapped(m), c(m);
-                wrapped = wrap(n);
+                wrapped = m_converter.wrap(n);
                 mpf_rounding_mode rm;
                 scoped_mpf val(mpfm);
                 if (m_fpa_util.is_rm_numeral(n, rm)) {
@@ -646,7 +487,7 @@ namespace smt {
                 }
                 else {
                     expr_ref wu(m);
-                    wu = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
+                    wu = m.mk_eq(m_converter.unwrap(wrapped, m.get_sort(n)), n);
                     TRACE("t_fpa", tout << "w/u eq: " << std::endl << mk_ismt2_pp(wu, m) << std::endl;);
                     assert_cnstr(wu);
                 }
@@ -736,7 +577,7 @@ namespace smt {
         model_value_proc * res = nullptr;
 
         app_ref wrapped(m);
-        wrapped = wrap(owner);
+        wrapped = m_converter.wrap(owner);
         SASSERT(m_bv_util.is_bv(wrapped));
 
         CTRACE("t_fpa_detail", !ctx.e_internalized(wrapped),
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index b485d1e39..f5ce63e70 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -85,16 +85,6 @@ namespace smt {
     protected:
         typedef trail_stack<theory_fpa> th_trail_stack;
 
-        class fpa2bv_converter_wrapped : public fpa2bv_converter {
-        public:
-            theory_fpa & m_th;
-            fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) :
-                fpa2bv_converter(m),
-                m_th(*th) {}
-            virtual ~fpa2bv_converter_wrapped() {}
-            void mk_const(func_decl * f, expr_ref & result) override;
-            void mk_rm_const(func_decl * f, expr_ref & result) override;
-        };
 
         class fpa_value_proc : public model_value_proc {
         protected:
@@ -144,9 +134,9 @@ namespace smt {
         };
 
     protected:
+        th_rewriter               m_th_rw;
         fpa2bv_converter_wrapped  m_converter;
         fpa2bv_rewriter           m_rw;
-        th_rewriter               m_th_rw;
         th_trail_stack            m_trail_stack;
         fpa_value_factory *       m_factory;
         fpa_util                & m_fpa_util;
@@ -184,15 +174,10 @@ namespace smt {
     protected:
         expr_ref mk_side_conditions();
         expr_ref convert(expr * e);
-        expr_ref convert_atom(expr * e);
-        expr_ref convert_term(expr * e);
-        expr_ref convert_conversion_term(expr * e);
 
         void attach_new_th_var(enode * n);
         void assert_cnstr(expr * e);
 
-        app_ref wrap(expr * e);
-        app_ref unwrap(expr * e, sort * s);
 
         enode* ensure_enode(expr* e);
         enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }