diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 94dfaaa68..219f9b166 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -200,7 +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->fpa_util().mk_ninf(to_sort(s)) : 
+                                          ctx->fpa_util().mk_pinf(to_sort(s)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -210,7 +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->fpa_util().mk_nzero(to_sort(s)) : 
+                                          ctx->fpa_util().mk_pzero(to_sort(s)));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
@@ -231,7 +233,10 @@ extern "C" {
         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);
+        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));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
@@ -667,6 +672,84 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
+        Z3_TRY;
+        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();
+        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);        
+        *sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val);
+        return r;
+        Z3_CATCH_RETURN(0);
+    }
+    
+    Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
+        Z3_TRY;
+        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();
+        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        scoped_mpf val(mpfm);
+        if (!plugin->is_numeral(to_expr(t), val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return "";
+        }
+        unsigned sbits = val.get().get_sbits();
+        scoped_mpq q(mpqm);
+        mpqm.set(q, mpfm.sig(val));
+        mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
+        std::stringstream ss;
+        mpqm.display_decimal(ss, q, sbits);
+        return mk_c(c)->mk_external_string(ss.str());
+        Z3_CATCH_RETURN("");
+
+    }
+
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
+        Z3_TRY;
+        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();
+        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
+        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);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return "";
+        }
+        const mpf_exp_t exp = mpfm.exp(val);        
+        std::stringstream ss;
+        ss << exp;
+        return mk_c(c)->mk_external_string(ss.str());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
+        Z3_TRY;
+        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();
+        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
+        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);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpfm.exp(val);
+        return 1;
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_to_ieee_bv(c, t);
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index 0745a8709..d5a25dfc2 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -50,7 +50,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_numeral(Z3_context c, const char* n, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_numeral(c, n, ty);
-        RESET_ERROR_CODE();          
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -64,20 +64,19 @@ extern "C" {
         char const* m = n;
         while (*m) {
             if (!(('0' <= *m && *m <= '9') ||
-                  ('/' == *m) || ('-' == *m) ||
-                  (' ' == *m) || ('\n' == *m) ||
-                  ('.' == *m) || ('e' == *m) ||
-                  ('E' == *m) ||
-                  (('p' == *m) && is_float) || 
-                  (('P' == *m)) && is_float)) {
+                ('/' == *m) || ('-' == *m) ||
+                (' ' == *m) || ('\n' == *m) ||
+                ('.' == *m) || ('e' == *m) ||
+                ('E' == *m) ||
+                (('p' == *m) && is_float) ||
+                (('P' == *m)) && is_float)) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR);
                 return 0;
             }
             ++m;
         }
-        ast * a = 0;        
-        if (_ty->get_family_id() == mk_c(c)->get_fpa_fid())
-        {
+        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();
             scoped_mpf t(fu.fm());
@@ -90,23 +89,11 @@ extern "C" {
         RETURN_Z3(of_ast(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_int(Z3_context c, int value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_int(c, value, ty);
-        RESET_ERROR_CODE();  
-        if (!check_numeral_sort(c, ty)) {
-            RETURN_Z3(0);
-        }
-        ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
-        RETURN_Z3(of_ast(a)); 
-        Z3_CATCH_RETURN(0);
-    }
-    
-    Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned value, Z3_sort ty) {
-        Z3_TRY;
-        LOG_Z3_mk_unsigned_int(c, value, ty);
-        RESET_ERROR_CODE();   
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -114,11 +101,23 @@ extern "C" {
         RETURN_Z3(of_ast(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
+    Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned value, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_unsigned_int(c, value, ty);
+        RESET_ERROR_CODE();
+        if (!check_numeral_sort(c, ty)) {
+            RETURN_Z3(0);
+        }
+        ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_int64(Z3_context c, long long value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_int64(c, value, ty);
-        RESET_ERROR_CODE();  
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -127,11 +126,11 @@ extern "C" {
         RETURN_Z3(of_ast(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned long long value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_unsigned_int64(c, value, ty);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -146,10 +145,11 @@ extern "C" {
         LOG_Z3_is_numeral_ast(c, a);
         RESET_ERROR_CODE();
         expr* e = to_expr(a);
-        return 
+        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_numeral(e) ||
+            mk_c(c)->fpa_util().is_rm_numeral(e);
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
@@ -193,7 +193,28 @@ extern "C" {
             // floats are separated from all others to avoid huge rationals.
             fpa_util & fu = mk_c(c)->fpa_util();
             scoped_mpf tmp(fu.fm());
-            if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) {
+            mpf_rounding_mode rm;
+            if (mk_c(c)->fpa_util().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"); 
+                    break;
+                case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
+                    return mk_c(c)->mk_external_string("roundNearestTiesToAway"); 
+                    break;
+                case OP_FPA_RM_TOWARD_POSITIVE:
+                    return mk_c(c)->mk_external_string("roundTowardPositive");
+                    break;
+                case OP_FPA_RM_TOWARD_NEGATIVE:
+                    return mk_c(c)->mk_external_string("roundTowardNegative");
+                    break;
+                case OP_FPA_RM_TOWARD_ZERO:
+                default:
+                    return mk_c(c)->mk_external_string("roundTowardZero");
+                    break;
+                }                
+            }
+            else if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) {
                 return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
             }
             else {
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 89a89b959..70777a6e8 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3465,82 +3465,82 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRNE()
+        public FPRMNum MkFPRNE()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_rne(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRoundNearestTiesToAway()
+        public FPRMNum MkFPRoundNearestTiesToAway()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRNA()
+        public FPRMNum MkFPRNA()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_rna(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRoundTowardPositive()
+        public FPRMNum MkFPRoundTowardPositive()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRTP()
+        public FPRMNum MkFPRTP()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_rtp(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRoundTowardNegative()
+        public FPRMNum MkFPRoundTowardNegative()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRTN()
+        public FPRMNum MkFPRTN()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_rtn(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRoundTowardZero()
+        public FPRMNum MkFPRoundTowardZero()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
         }
 
         /// <summary>
         /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
         /// </summary>
-        public FPRMExpr MkFPRTZ()
+        public FPRMNum MkFPRTZ()
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPRMExpr(this, Native.Z3_mk_fpa_rtz(nCtx));
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
         }        
         #endregion
         #endregion
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index eb1d1c02d..e3ff27da1 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -1470,7 +1470,12 @@ namespace Microsoft.Z3
         /// <summary>
         /// Indicates whether the term is a floating-point numeral
         /// </summary>
-        public bool IsFPNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NUM; } }
+        public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point rounding mode numeral
+        /// </summary>
+        public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
 
         /// <summary>
         /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
@@ -1809,7 +1814,7 @@ namespace Microsoft.Z3
                     case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
                     case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
                     case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
-                    case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
+                    case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
                 }
             }
 
diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index 14c089198..e85687ccf 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -27,6 +27,63 @@ namespace Microsoft.Z3
     [ContractVerification(true)]
     public class FPNum : FPExpr
     {
+        /// <summary>
+        /// Retrieves the sign of a floating-point literal
+        /// </summary>
+        /// <remarks>
+        /// Remarks: returns true if the numeral is negative
+        /// </remarks>
+        public bool Sign
+        {
+            get
+            {
+                int res = 0;
+                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)                
+                    throw new Z3Exception("Sign is not a Boolean value");
+                return res != 0;
+            }
+        }
+
+        /// <summary>
+        /// The significand value of a floating-point numeral as a string
+        /// </summary>
+        /// <remarks>
+        /// The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
+        /// enough to represent the real significand precisely.
+        /// </remarks>
+        public string Significand
+        {
+            get
+            {
+                return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Return the exponent value of a floating-point numeral as a string
+        /// </summary>
+        public string Exponent
+        {
+            get
+            {
+                return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Return the exponent value of a floating-point numeral as a signed 64-bit integer
+        /// </summary>
+        public Int64 ExponentInt64
+        {
+            get
+            {
+                Int64 result = 0;
+                if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
+                    throw new Z3Exception("Exponent is not a 64 bit integer");
+                return result;
+            }
+        }
+
         #region Internal
         internal FPNum(Context ctx, IntPtr obj)
             : base(ctx, obj)
diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs
index 47ea3e670..896c3e6b9 100644
--- a/src/api/dotnet/FPRMExpr.cs
+++ b/src/api/dotnet/FPRMExpr.cs
@@ -30,56 +30,6 @@ namespace Microsoft.Z3
     /// </summary>
     public class FPRMExpr : Expr
     {
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
-        /// </summary>
-        public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
-        /// </summary>
-        public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
-        /// </summary>
-        public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
-        /// </summary>
-        public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
-        /// </summary>
-        public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
-        /// </summary>
-        public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
-        /// </summary>
-        public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
-        /// </summary>
-        public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
-        /// </summary>
-        public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
-
-        /// <summary>
-        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
-        /// </summary>
-        public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
-
         #region Internal
         /// <summary> Constructor for FPRMExpr </summary>
         internal FPRMExpr(Context ctx, IntPtr obj)
diff --git a/src/api/dotnet/FPRMNum.cs b/src/api/dotnet/FPRMNum.cs
new file mode 100644
index 000000000..81cff167e
--- /dev/null
+++ b/src/api/dotnet/FPRMNum.cs
@@ -0,0 +1,100 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Floating Point Rounding Mode Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Floating-point rounding mode numerals
+    /// </summary>
+    public class FPRMNum : FPRMExpr
+    {
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+        /// </summary>
+        public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+        /// </summary>
+        public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+        /// </summary>
+        public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+        /// </summary>
+        public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+        /// </summary>
+        public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+        /// </summary>
+        public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+        /// </summary>
+        public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+        /// </summary>
+        public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
+        /// </summary>
+        public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
+        /// </summary>
+        public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>        
+        public override string ToString()
+        {
+            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
+        }
+
+        #region Internal
+        /// <summary> Constructor for FPRMNum </summary>
+        internal FPRMNum(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 29be4aae8..cfbd7c2c8 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2865,90 +2865,90 @@ public class Context extends IDisposable
      * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
      * @throws Z3Exception on error
      **/
-    public FPRMExpr mkFPRoundNearestTiesToEven() throws Z3Exception
+    public FPRMNum mkFPRoundNearestTiesToEven() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRNE() throws Z3Exception
+    public FPRMNum mkFPRNE() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRne(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRne(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRoundNearestTiesToAway() throws Z3Exception
+    public FPRMNum mkFPRoundNearestTiesToAway() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRNA() throws Z3Exception
+    public FPRMNum mkFPRNA() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRna(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRna(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRoundTowardPositive() throws Z3Exception
+    public FPRMNum mkFPRoundTowardPositive() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRoundTowardPositive(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRTP() throws Z3Exception
+    public FPRMNum mkFPRTP() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRtp(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRoundTowardNegative() throws Z3Exception
+    public FPRMNum mkFPRoundTowardNegative() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRoundTowardNegative(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRTN() throws Z3Exception
+    public FPRMNum mkFPRTN() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRtn(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRoundTowardZero() throws Z3Exception
+    public FPRMNum mkFPRoundTowardZero() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRoundTowardZero(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
     }
 
     /** 
      * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
      * @throws Z3Exception 
      **/
-    public FPRMExpr mkFPRTZ() throws Z3Exception
+    public FPRMNum mkFPRTZ() throws Z3Exception
     {
-        return new FPRMExpr(this, Native.mkFpaRtz(nCtx()));
+        return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
     }        
 
     /** FloatingPoint Sorts **/
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 49f49a295..57f53ec6b 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1714,98 +1714,105 @@ public class Expr extends AST
      * Indicates whether the terms is of floating-point sort.
      * @throws Z3Exception 
      */
-    public boolean IsFP() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
+    public boolean isFP() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
 
     /**
      * Indicates whether the terms is of floating-point rounding mode sort.
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRM() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
+    public boolean isFPRM() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
 
     /**
      * Indicates whether the term is a floating-point numeral
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPNumeral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NUM; }
+    public boolean isFPNumeral() throws Z3Exception { return isFP() && isNumeral(); }
+    
+    /**
+     * Indicates whether the term is a floating-point rounding mode numeral
+     * @return
+     * @throws Z3Exception 
+     */
+    public boolean isFPRMNumeral() throws Z3Exception { return isFPRM() && isNumeral(); } 
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+    public boolean isFPRMNumRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
     
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }        
+    public boolean isFPRMNumRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }        
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
+    public boolean isFPRMNumRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+    public boolean isFPRMNumRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardZero
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+    public boolean isFPRMNumRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+    public boolean isFPRMNumRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
     
     /**
      *  Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }        
+    public boolean isFPRMNumRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }        
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
+    public boolean isFPRMNumRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+    public boolean isFPRMNumRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardZero
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNumRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+    public boolean isFPRMNumRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
 
     /**
      * Indicates whether the term is a floating-point rounding mode numeral
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRMNum() throws Z3Exception {
+    public boolean isFPRMNum() throws Z3Exception {
     	return isApp() &&
     			(getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY ||
                 getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN  ||
@@ -1819,42 +1826,42 @@ public class Expr extends AST
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPPlusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; }
+    public boolean isFPPlusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; }
 
     /**
      * Indicates whether the term is a floating-point -oo
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPMinusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; }
+    public boolean isFPMinusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; }
 
     /**
      * Indicates whether the term is a floating-point NaN
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NAN; }
+    public boolean isFPNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NAN; }
 
     /**
      * Indicates whether the term is a floating-point +zero
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPPlusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; }
+    public boolean isFPPlusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; }
 
     /**
      * Indicates whether the term is a floating-point -zero
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPMinusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; }
+    public boolean isFPMinusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; }
 
     /**
      * Indicates whether the term is a floating-point addition term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPAdd() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ADD; }
+    public boolean isFPAdd() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ADD; }
 
 
     /**
@@ -1862,211 +1869,210 @@ public class Expr extends AST
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPSub() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SUB; }
+    public boolean isFPSub() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SUB; }
 
     /**
      * Indicates whether the term is a floating-point negation term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPNeg() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NEG; }
+    public boolean isFPNeg() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NEG; }
 
     /**
      * Indicates whether the term is a floating-point multiplication term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPMul() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MUL; }
+    public boolean isFPMul() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MUL; }
                 
     /**
      * Indicates whether the term is a floating-point divison term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPDiv() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_DIV; }
+    public boolean isFPDiv() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_DIV; }
 
     /**
      * Indicates whether the term is a floating-point remainder term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRem() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_REM; }
+    public boolean isFPRem() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_REM; }
 
     /**
      * Indicates whether the term is a floating-point term absolute value term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPAbs() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ABS; }
+    public boolean isFPAbs() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ABS; }
 
     /**
      * Indicates whether the term is a floating-point minimum term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPMin() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MIN; }
+    public boolean isFPMin() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MIN; }
 
     /**
      * Indicates whether the term is a floating-point maximum term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPMax() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MAX; }
+    public boolean isFPMax() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MAX; }
 
     /**
      * Indicates whether the term is a floating-point fused multiply-add term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPFMA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FMA; }
+    public boolean isFPFMA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FMA; }
 
     /**
      * Indicates whether the term is a floating-point square root term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPSqrt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SQRT; }
+    public boolean isFPSqrt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SQRT; }
 
     /**
      * Indicates whether the term is a floating-point roundToIntegral term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPRoundToIntegral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; }
+    public boolean isFPRoundToIntegral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; }
 
     /**
      * Indicates whether the term is a floating-point equality term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPEq() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_EQ; }
+    public boolean isFPEq() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_EQ; }
 
     /**
      * Indicates whether the term is a floating-point less-than term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPLt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LT; }
+    public boolean isFPLt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LT; }
 
     /**
      * Indicates whether the term is a floating-point greater-than term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPGt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GT; }
+    public boolean isFPGt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GT; }
 
     /**
      * Indicates whether the term is a floating-point less-than or equal term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPLe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LE; }
+    public boolean isFPLe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LE; }
 
     /**
      * Indicates whether the term is a floating-point greater-than or erqual term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPGe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GE; } 
+    public boolean isFPGe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GE; } 
 
     /**
      * Indicates whether the term is a floating-point isNaN predicate term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NAN; }
+    public boolean isFPisNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NAN; }
 
     /**
      * Indicates whether the term is a floating-point isInf predicate term
      * @return 
      * @throws Z3Exception 
      */
-    public boolean IsFPisInf() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_INF; }
+    public boolean isFPisInf() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_INF; }
 
     /**
      * Indicates whether the term is a floating-point isZero predicate term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; }
+    public boolean isFPisZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; }
 
     /**
      * Indicates whether the term is a floating-point isNormal term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisNormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; }
+    public boolean isFPisNormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; }
 
     /**
      * Indicates whether the term is a floating-point isSubnormal predicate term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisSubnormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; }
+    public boolean isFPisSubnormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; }
 
     /**
      * Indicates whether the term is a floating-point isNegative predicate term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; }     
+    public boolean isFPisNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; }     
 
     /**
      * Indicates whether the term is a floating-point isPositive predicate term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPisPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; }    
+    public boolean isFPisPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; }    
 
     /**
      * Indicates whether the term is a floating-point constructor term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPFP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FP; }
+    public boolean isFPFP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FP; }
 
     /**
      * Indicates whether the term is a floating-point conversion term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToFp() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP; }
+    public boolean isFPToFp() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP; }
 
     /**
      * Indicates whether the term is a floating-point conversion from unsigned bit-vector term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToFpUnsigned() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; }
+    public boolean isFPToFpUnsigned() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; }
 
     /**
      * Indicates whether the term is a floating-point conversion to unsigned bit-vector term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToUBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } 
+    public boolean isFPToUBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } 
 
     /**
      * Indicates whether the term is a floating-point conversion to signed bit-vector term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToSBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_SBV; }
+    public boolean isFPToSBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_SBV; }
 
     /**
      * Indicates whether the term is a floating-point conversion to real term
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToReal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_REAL; }    
-
+    public boolean isFPToReal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_REAL; }    
 
     /**
      * Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term1
      * @return
      * @throws Z3Exception 
      */
-    public boolean IsFPToIEEEBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; }    
+    public boolean isFPToIEEEBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; }    
     
     
 	/**
@@ -2140,6 +2146,8 @@ public class Expr extends AST
 				return new BitVecNum(ctx, obj);
 			case Z3_FLOATING_POINT_SORT:
 				return new FPNum(ctx, obj);
+			case Z3_ROUNDING_MODE_SORT:
+				return new FPRMNum(ctx, obj);
 			default: ;
 			}
 		}
diff --git a/src/api/java/FPExpr.java b/src/api/java/FPExpr.java
new file mode 100644
index 000000000..e5193a042
--- /dev/null
+++ b/src/api/java/FPExpr.java
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPExpr.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+/**
+ * FloatingPoint Expressions
+ */
+public class FPExpr extends Expr
+{   
+    /**
+     * The number of exponent bits.
+     * @throws Z3Exception 
+     */
+    public int getEBits() throws Z3Exception { return ((FPSort)getSort()).getEBits(); }
+
+    /**
+     * The number of significand bits.
+     * @throws Z3Exception 
+     */
+    public int getSBits() throws Z3Exception { return ((FPSort)getSort()).getSBits(); }
+    
+    public FPExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj); 
+    }
+
+}
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
new file mode 100644
index 000000000..f2c9b7f98
--- /dev/null
+++ b/src/api/java/FPNum.java
@@ -0,0 +1,86 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPNum.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+/**
+ * FloatingPoint Numerals
+ */
+public class FPNum extends FPExpr
+{
+	/**
+	 * Retrieves the sign of a floating-point literal	 
+     * Remarks: returns true if the numeral is negative 
+	 * @throws Z3Exception 
+     */
+    public boolean getSign() throws Z3Exception {
+    	Native.IntPtr res = new Native.IntPtr();
+        if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true)                
+            throw new Z3Exception("Sign is not a Boolean value");
+        return res.value != 0;
+        
+        
+    }
+
+    /**
+     * The significand value of a floating-point numeral as a string
+     * Remarks: The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
+     * enough to represent the real significand precisely.
+     * @throws Z3Exception 
+     **/
+    public String getSignificand() throws Z3Exception {
+        return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Return the exponent value of a floating-point numeral as a string
+     * @throws Z3Exception 
+     */
+    public String getExponent() throws Z3Exception {
+        return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Return the exponent value of a floating-point numeral as a signed 64-bit integer
+     * @throws Z3Exception 
+     */
+    public long getExponentInt64() throws Z3Exception  {
+        Native.LongPtr res = new Native.LongPtr();
+        if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
+            throw new Z3Exception("Exponent is not a 64 bit integer");
+        return res.value;
+    }
+    
+    public FPNum(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
+    
+    /**
+     * Returns a string representation of the numeral.
+     */           
+    public String toString()
+    {
+        try
+        {
+            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
+        } catch (Z3Exception e)
+        {
+            return "Z3Exception: " + e.getMessage();
+        }
+    }
+
+}
diff --git a/src/api/java/FPRMExpr.java b/src/api/java/FPRMExpr.java
new file mode 100644
index 000000000..482c3b899
--- /dev/null
+++ b/src/api/java/FPRMExpr.java
@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMExpr.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+/**
+ * FloatingPoint RoundingMode Expressions
+ */
+public class FPRMExpr extends Expr
+{       
+    public FPRMExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
+
+}
diff --git a/src/api/java/FPRMNum.java b/src/api/java/FPRMNum.java
new file mode 100644
index 000000000..04e7727e2
--- /dev/null
+++ b/src/api/java/FPRMNum.java
@@ -0,0 +1,90 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMNum.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+import com.microsoft.z3.enumerations.Z3_decl_kind;
+
+/**
+ * FloatingPoint RoundingMode Numerals
+ */
+public class FPRMNum extends FPRMExpr {
+
+	/**
+     * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+     * @throws Z3Exception 
+     * **/
+    public boolean isRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+     * @throws Z3Exception 
+     */
+    public boolean isRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+     * @throws Z3Exception 
+     */
+    public boolean isRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+     * @throws Z3Exception 
+     */
+    public boolean isRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+     * @throws Z3Exception 
+     */
+    public boolean isRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+     * @throws Z3Exception 
+     */
+    public boolean isRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+     * @throws Z3Exception 
+     */
+    public boolean isRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+     * @throws Z3Exception 
+     */
+    public boolean isRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } 
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardZero
+     * @throws Z3Exception 
+     */
+    public boolean isRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+
+    /**
+     * Indicates whether the term is the floating-point rounding numeral roundTowardZero
+     * @throws Z3Exception 
+     */
+    public boolean isRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+    
+	public FPRMNum(Context ctx, long obj) throws Z3Exception {
+		super(ctx, obj);
+	}
+
+}
diff --git a/src/api/java/FPRMSort.java b/src/api/java/FPRMSort.java
new file mode 100644
index 000000000..ff6422ef6
--- /dev/null
+++ b/src/api/java/FPRMSort.java
@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMExpr.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+/**
+ * The FloatingPoint RoundingMode sort
+ **/
+public class FPRMSort extends Sort
+{
+
+    public FPRMSort(Context ctx) throws Z3Exception
+    {        
+        super(ctx, Native.mkFpaRoundingModeSort(ctx.nCtx()));
+    }
+
+    public FPRMSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj); 
+    }
+
+}
\ No newline at end of file
diff --git a/src/api/java/FPSort.java b/src/api/java/FPSort.java
new file mode 100644
index 000000000..284979524
--- /dev/null
+++ b/src/api/java/FPSort.java
@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPSort.java
+
+Abstract:
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+package com.microsoft.z3;
+
+/**
+ * A FloatingPoint sort
+ **/
+public class FPSort extends Sort
+{
+
+    public FPSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);        
+    }
+    
+    public FPSort(Context ctx, int ebits, int sbits) throws Z3Exception
+	{
+    	super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));	    
+	}
+    
+    /**
+     * The number of exponent bits.
+     */
+    public int getEBits() throws Z3Exception {
+    	return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());    	
+    }
+    
+    /**
+     * The number of significand bits.
+     */
+    public int getSBits() throws Z3Exception {
+    	return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());    	
+    }
+    
+}
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 043d43e2f..7457ed9a3 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -834,6 +834,47 @@ extern "C" {
     */
     unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
 
+    /**
+        \brief Retrieves the sign of a floating-point literal
+
+        Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise.
+
+        \param t a floating-point numeral.
+
+        def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
+
+    /**
+        \brief Return the significand value of a floating-point numeral as a string
+
+        Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
+        enough to represent the real significand precisely.
+
+        \param t a floating-point numeral.
+
+        def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Return the exponent value of a floating-point numeral as a string
+
+        \param t a floating-point numeral.
+
+        def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
+
+        \param t a floating-point numeral.
+
+        def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
+
     /**
         \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.