diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 82002c4f7..fd3d1bdc8 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7749,7 +7749,7 @@ class FPRMRef(ExprRef):
         return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
 
   
-def RoundNearestTiesToEven (ctx=None):
+def RoundNearestTiesToEven(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
 
@@ -7757,7 +7757,7 @@ def RNE (ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
 
-def RoundNearestTiesToAway (ctx=None):
+def RoundNearestTiesToAway(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
 
@@ -7765,27 +7765,27 @@ def RNA (ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
 
-def RoundTowardPositive (ctx=None):
+def RoundTowardPositive(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
 
-def RTP (ctx=None):
+def RTP(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
 
-def RoundTowardNegative (ctx=None):
+def RoundTowardNegative(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
 
-def RTN (ctx=None):
+def RTN(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
 
-def RoundTowardZero (ctx=None):
+def RoundTowardZero(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
 
-def RTZ (ctx=None):
+def RTZ(ctx=None):
     ctx = _get_ctx(ctx)
     return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
 
diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index da49f1719..ac1607dda 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3printer.py
@@ -64,9 +64,9 @@ _z3_precedence = {
 
 # FPA operators 
 _z3_op_to_fpa_normal_str = {
-    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RNE()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RNA()',
-    Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RTP()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RTN()',
-    Z3_OP_FPA_RM_TOWARD_ZERO : 'RTZ()',
+    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RoundNearestTiesToEven()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RoundNearestTiesToAway()',
+    Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RoundTowardPositive()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RoundTowardNegative()',
+    Z3_OP_FPA_RM_TOWARD_ZERO : 'RoundTowardZero()',
     Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
     Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : 'PZero', Z3_OP_FPA_MINUS_ZERO : 'NZero',
     Z3_OP_FPA_ADD : 'fpAdd', Z3_OP_FPA_SUB : 'fpSub', Z3_OP_FPA_NEG : 'fpNeg', Z3_OP_FPA_MUL : 'fpMul',
@@ -580,7 +580,7 @@ class Formatter:
         if self.fpa_pretty and a.decl().kind() in _z3_op_to_fpa_pretty_str:
             return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind()))
         else:
-            return to_format(a.as_string())
+            return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind()))
 
     def pp_fp_value(self, a):
         z3._z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')