diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index f81edb653..efc4d9179 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -45,7 +45,7 @@ class fpa2bv_converter {
 protected:
     ast_manager              & m;
     basic_simplifier_plugin    m_simp;
-    float_util                 m_util;
+    fpa_util                   m_util;
     bv_util                    m_bv_util;
     arith_util                 m_arith_util;
     mpf_manager              & m_mpf_manager;
@@ -62,7 +62,7 @@ public:
     fpa2bv_converter(ast_manager & m);    
     ~fpa2bv_converter();
 
-    float_util & fu() { return m_util; }
+    fpa_util & fu() { return m_util; }
     bv_util & bu() { return m_bv_util; }
     arith_util & au() { return m_arith_util; }
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 055f79b9d..487908173 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -700,7 +700,7 @@ namespace smt {
 
     void theory_fpa::init_model(model_generator & mg) {
         TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
-        m_factory = alloc(fpa_factory, get_manager(), get_family_id());
+        m_factory = alloc(fpa_value_factory, get_manager(), get_family_id());
         mg.register_factory(m_factory);
     }
 
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 58af5ad1c..33733d7d9 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -29,7 +29,7 @@ Revision History:
 
 namespace smt {
 
-    class fpa_value_actory : public value_factory {
+    class fpa_value_factory : public value_factory {
         fpa_util          m_util;
 
         virtual app * mk_value_core(mpf const & val, sort * s) {
@@ -39,11 +39,11 @@ namespace smt {
         }
 
     public:
-        fpa_value_actory(ast_manager & m, family_id fid) :
+        fpa_value_factory(ast_manager & m, family_id fid) :
             value_factory(m, fid),
             m_util(m) {}
 
-        virtual ~fpa_value_actory() {}
+        virtual ~fpa_value_factory() {}
 
         virtual expr * get_some_value(sort * s) {
             mpf_manager & mpfm = m_util.fm();
@@ -97,7 +97,7 @@ namespace smt {
 
         public:
             fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : 
-                m_th(*th), m_fu(th->m_float_util), m_bu(th->m_bv_util), m(th->get_manager()),
+                m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()),
                 m_ebits(ebits), m_sbits(sbits) {}
             
             virtual ~fpa_value_proc() {}
@@ -112,15 +112,15 @@ namespace smt {
         };
 
         class fpa_rm_value_proc : public model_value_proc {
-            theory_fpa & m_th;
+            theory_fpa  & m_th;
             ast_manager & m;
-            float_util & m_fu;
-            bv_util    & m_bu;
+            fpa_util    & m_fu;
+            bv_util     & m_bu;
             buffer<model_value_dependency> m_deps;
 
         public:
             fpa_rm_value_proc(theory_fpa * th) : 
-                m_th(*th), m_fu(th->m_float_util), m_bu(th->m_bv_util), m(th->get_manager()) {}
+                m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()) {}
 
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
 
@@ -137,8 +137,8 @@ namespace smt {
         fpa2bv_rewriter           m_rw;
         th_rewriter               m_th_rw;
         th_trail_stack            m_trail_stack;
-        fpa_factory *             m_factory;
-        float_util              & m_float_util;
+        fpa_value_factory *       m_factory;
+        fpa_util                & m_fpa_util;
         bv_util                 & m_bv_util;
         arith_util              & m_arith_util;
         obj_map<sort, func_decl*> m_wraps;
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index e205a6c5e..5bc006f00 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -48,6 +48,10 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
     return st;
 }
 
+tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p) {
+    return mk_qffp_tactic(m, p);
+}
+
 struct is_non_qffp_predicate {
     struct found {};
     ast_manager & m;
@@ -90,3 +94,6 @@ probe * mk_is_qffp_probe() {
     return alloc(is_qffp_probe);
 }
     
+probe * mk_is_qffpbv_probe() {
+    return alloc(is_qffp_probe);
+}
diff --git a/src/tactic/fpa/qffp_tactic.h b/src/tactic/fpa/qffp_tactic.h
index 2842e3f73..5c8caba2b 100644
--- a/src/tactic/fpa/qffp_tactic.h
+++ b/src/tactic/fpa/qffp_tactic.h
@@ -25,6 +25,7 @@ class ast_manager;
 class tactic;
 
 tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p = params_ref());
+tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 /*
   ADD_TACTIC("qffp", "(try to) solve goal using the tactic for QF_FP.", "mk_qffp_tactic(m, p)")
   ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).", "mk_qffpbv_tactic(m, p)")