diff --git a/src/api/api_context.h b/src/api/api_context.h
index 6312b3f69..58394c028 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -118,7 +118,7 @@ namespace api {
         arith_util & autil() { return m_arith_util; }
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
-        fpa_util & fpa_util() { return m_fpa_util; }
+        fpa_util & fpautil() { return m_fpa_util; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index d9f534499..9d47e152a 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -29,7 +29,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rounding_mode_sort(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);        
-        Z3_sort r = of_sort(ctx->fpa_util().mk_rm_sort());
+        Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -40,7 +40,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -50,7 +50,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rne(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_even());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -61,7 +61,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_nearest_ties_to_away(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -71,7 +71,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rna(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_nearest_ties_to_away());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -82,7 +82,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_toward_positive(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -92,7 +92,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rtp(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_positive());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -103,7 +103,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_toward_negative(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -113,7 +113,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rtn(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_negative());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -124,7 +124,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_toward_zero(c);
         RESET_ERROR_CODE(); 
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -134,7 +134,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rtz(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_toward_zero());
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -148,7 +148,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
         }        
         api::context * ctx = mk_c(c);        
-        Z3_sort r = of_sort(ctx->fpa_util().mk_float_sort(ebits, sbits));
+        Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -190,7 +190,7 @@ extern "C" {
         LOG_Z3_mk_fpa_nan(c, s);
         RESET_ERROR_CODE();         
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_nan(to_sort(s)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -200,8 +200,8 @@ extern "C" {
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_ninf(to_sort(s)) : 
-                                          ctx->fpa_util().mk_pinf(to_sort(s)));
+        Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : 
+                                          ctx->fpautil().mk_pinf(to_sort(s)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -211,8 +211,8 @@ extern "C" {
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_nzero(to_sort(s)) : 
-                                          ctx->fpa_util().mk_pzero(to_sort(s)));
+        Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : 
+                                          ctx->fpautil().mk_pzero(to_sort(s)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -222,7 +222,7 @@ extern "C" {
         LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -232,12 +232,12 @@ extern "C" {
         LOG_Z3_mk_fpa_numeral_float(c, v, ty);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        scoped_mpf tmp(ctx->fpa_util().fm());
-        ctx->fpa_util().fm().set(tmp, 
-                                 ctx->fpa_util().get_ebits(to_sort(ty)), 
-                                 ctx->fpa_util().get_sbits(to_sort(ty)), 
+        scoped_mpf tmp(ctx->fpautil().fm());
+        ctx->fpautil().fm().set(tmp, 
+                                 ctx->fpautil().get_ebits(to_sort(ty)), 
+                                 ctx->fpautil().get_sbits(to_sort(ty)), 
                                  v);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
+        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -247,9 +247,9 @@ extern "C" {
         LOG_Z3_mk_fpa_numeral_double(c, v, ty);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        scoped_mpf tmp(ctx->fpa_util().fm());
-        ctx->fpa_util().fm().set(tmp, ctx->fpa_util().get_ebits(to_sort(ty)), ctx->fpa_util().get_sbits(to_sort(ty)), v);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
+        scoped_mpf tmp(ctx->fpautil().fm());
+        ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v);
+        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -259,12 +259,12 @@ extern "C" {
         LOG_Z3_mk_fpa_numeral_int(c, v, ty);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        scoped_mpf tmp(ctx->fpa_util().fm());
-        ctx->fpa_util().fm().set(tmp,
-                                   ctx->fpa_util().get_ebits(to_sort(ty)),
-                                   ctx->fpa_util().get_sbits(to_sort(ty)),
+        scoped_mpf tmp(ctx->fpautil().fm());
+        ctx->fpautil().fm().set(tmp,
+                                   ctx->fpautil().get_ebits(to_sort(ty)),
+                                   ctx->fpautil().get_sbits(to_sort(ty)),
                                    v);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
+        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -274,12 +274,12 @@ extern "C" {
         LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        scoped_mpf tmp(ctx->fpa_util().fm());
-        ctx->fpa_util().fm().set(tmp, 
-                                   ctx->fpa_util().get_ebits(to_sort(ty)), 
-                                   ctx->fpa_util().get_sbits(to_sort(ty)), 
+        scoped_mpf tmp(ctx->fpautil().fm());
+        ctx->fpautil().fm().set(tmp, 
+                                   ctx->fpautil().get_ebits(to_sort(ty)), 
+                                   ctx->fpautil().get_sbits(to_sort(ty)), 
                                    sgn != 0, sig, exp);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
+        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -289,12 +289,12 @@ extern "C" {
         LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        scoped_mpf tmp(ctx->fpa_util().fm());
-        ctx->fpa_util().fm().set(tmp,
-                                   ctx->fpa_util().get_ebits(to_sort(ty)),
-                                   ctx->fpa_util().get_sbits(to_sort(ty)),
+        scoped_mpf tmp(ctx->fpautil().fm());
+        ctx->fpautil().fm().set(tmp,
+                                   ctx->fpautil().get_ebits(to_sort(ty)),
+                                   ctx->fpautil().get_sbits(to_sort(ty)),
                                    sgn != 0, sig, exp);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
+        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -304,7 +304,7 @@ extern "C" {
         LOG_Z3_mk_fpa_abs(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_abs(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -314,7 +314,7 @@ extern "C" {
         LOG_Z3_mk_fpa_neg(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_neg(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -324,7 +324,7 @@ extern "C" {
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -334,7 +334,7 @@ extern "C" {
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -344,7 +344,7 @@ extern "C" {
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -354,7 +354,7 @@ extern "C" {
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -364,7 +364,7 @@ extern "C" {
         LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -374,7 +374,7 @@ extern "C" {
         LOG_Z3_mk_fpa_sqrt(c, rm, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_sqrt(to_expr(rm), to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -384,7 +384,7 @@ extern "C" {
         LOG_Z3_mk_fpa_rem(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_rem(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -394,7 +394,7 @@ extern "C" {
         LOG_Z3_mk_fpa_round_to_integral(c, rm, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_round_to_integral(to_expr(rm), to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -404,7 +404,7 @@ extern "C" {
         LOG_Z3_mk_fpa_min(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_min(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -414,7 +414,7 @@ extern "C" {
         LOG_Z3_mk_fpa_max(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_max(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -424,7 +424,7 @@ extern "C" {
         LOG_Z3_mk_fpa_leq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_le(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -434,7 +434,7 @@ extern "C" {
         LOG_Z3_mk_fpa_lt(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_lt(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -444,7 +444,7 @@ extern "C" {
         LOG_Z3_mk_fpa_geq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_ge(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -454,7 +454,7 @@ extern "C" {
         LOG_Z3_mk_fpa_gt(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_gt(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -464,7 +464,7 @@ extern "C" {
         LOG_Z3_mk_fpa_eq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_float_eq(to_expr(t1), to_expr(t2)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -474,7 +474,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_normal(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_normal(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -484,7 +484,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_subnormal(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_subnormal(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -494,7 +494,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_zero(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_zero(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -504,7 +504,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_infinite(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_inf(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -514,7 +514,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_nan(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_nan(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -524,7 +524,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_negative(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_negative(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -534,7 +534,7 @@ extern "C" {
         LOG_Z3_mk_fpa_is_positive(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_is_positive(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -545,7 +545,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!ctx->bvutil().is_bv(to_expr(bv)) ||
             !fu.is_float(to_sort(s))) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
@@ -561,7 +561,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_float(c, rm, t, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!fu.is_rm(to_expr(rm)) || 
             !fu.is_float(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
@@ -578,7 +578,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_real(c, rm, t, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!fu.is_rm(to_expr(rm)) ||
             !ctx->autil().is_real(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
@@ -595,7 +595,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_signed(c, rm, t, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!fu.is_rm(to_expr(rm)) ||
             !ctx->bvutil().is_bv(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
@@ -612,7 +612,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_unsigned(c, rm, t, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!fu.is_rm(to_expr(rm)) || 
             !ctx->bvutil().is_bv(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
@@ -629,7 +629,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_to_ubv(to_expr(rm), to_expr(t), sz));
+        Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -639,7 +639,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_to_sbv(to_expr(rm), to_expr(t), sz));
+        Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -649,7 +649,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_real(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_to_real(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -659,7 +659,7 @@ extern "C" {
         LOG_Z3_fpa_get_ebits(c, s);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(s, 0);
-        return mk_c(c)->fpa_util().get_ebits(to_sort(s));
+        return mk_c(c)->fpautil().get_ebits(to_sort(s));
         Z3_CATCH_RETURN(0);
     }
 
@@ -668,7 +668,7 @@ extern "C" {
         LOG_Z3_fpa_get_ebits(c, s);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(s, 0);
-        return mk_c(c)->fpa_util().get_sbits(to_sort(s));
+        return mk_c(c)->fpautil().get_sbits(to_sort(s));
         Z3_CATCH_RETURN(0);
     }
 
@@ -677,7 +677,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
@@ -695,7 +695,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_significand_string(c, t);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
@@ -726,7 +726,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_exponent_string(c, t);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();        
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();        
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
@@ -750,7 +750,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_exponent_string(c, t);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);        
@@ -768,7 +768,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_ieee_bv(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpa_util().mk_float_to_ieee_bv(to_expr(t)));
+        Z3_ast r = of_ast(ctx->fpautil().mk_float_to_ieee_bv(to_expr(t)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -778,7 +778,7 @@ extern "C" {
         LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        fpa_util & fu = ctx->fpa_util();
+        fpa_util & fu = ctx->fpautil();
         if (!fu.is_rm(to_expr(rm)) ||
             !ctx->autil().is_real(to_expr(sig)) ||
             !ctx->autil().is_int(to_expr(exp)) ||
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 277e80c20..446a66bc5 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -59,7 +59,7 @@ extern "C" {
             RETURN_Z3(0);
         }
         sort * _ty = to_sort(ty);
-        bool is_float = mk_c(c)->fpa_util().is_float(_ty);
+        bool is_float = mk_c(c)->fpautil().is_float(_ty);
         std::string fixed_num;
         char const* m = n;
         while (*m) {
@@ -78,7 +78,7 @@ extern "C" {
         ast * a = 0;
         if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) {
             // avoid expanding floats into huge rationals.
-            fpa_util & fu = mk_c(c)->fpa_util();
+            fpa_util & fu = mk_c(c)->fpautil();
             scoped_mpf t(fu.fm());
             fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_TOWARD_ZERO, n);
             a = fu.mk_value(t);
@@ -148,8 +148,8 @@ extern "C" {
         return
             mk_c(c)->autil().is_numeral(e) ||
             mk_c(c)->bvutil().is_numeral(e) ||
-            mk_c(c)->fpa_util().is_numeral(e) ||
-            mk_c(c)->fpa_util().is_rm_numeral(e);
+            mk_c(c)->fpautil().is_numeral(e) ||
+            mk_c(c)->fpautil().is_rm_numeral(e);
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
@@ -191,10 +191,10 @@ extern "C" {
         }
         else {
             // floats are separated from all others to avoid huge rationals.
-            fpa_util & fu = mk_c(c)->fpa_util();
+            fpa_util & fu = mk_c(c)->fpautil();
             scoped_mpf tmp(fu.fm());
             mpf_rounding_mode rm;
-            if (mk_c(c)->fpa_util().is_rm_numeral(to_expr(a), rm)) {
+            if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
                 switch (rm) {
                 case OP_FPA_RM_NEAREST_TIES_TO_EVEN: 
                     return mk_c(c)->mk_external_string("roundNearestTiesToEven"); 
@@ -214,7 +214,7 @@ extern "C" {
                     break;
                 }                
             }
-            else if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) {
+            else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
                 return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
             }
             else {