diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 69855fc4f..986efc94d 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3439,65 +3439,118 @@ namespace Microsoft.Z3
         #endregion
 
         #region Floating-Point Arithmetic
+
+        #region Rounding Modes
+        #region RoundingMode Sort
         /// <summary>
-        /// Create a floating point rounding mode sort.
+        /// Create the floating-point RoundingMode sort.
         /// </summary>    
-        public FPRMSort MkFPRMSort()
+        public FPRMSort MkFPRoundingModeSort()
         {
             Contract.Ensures(Contract.Result<FPRMSort>() != null);
             return new FPRMSort(this);
         }
-
+        #endregion
+        
+        #region Numerals
         /// <summary>
-        /// Create a NearestTiesToEven rounding mode numeral.
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
         /// </summary>
-        public FPRMNum MkFPRMNearestTiesToEven()
+        public FPRMNum MkFPRoundNearestTiesToEven()
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
             return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
         }
 
         /// <summary>
-        /// Create a NearestTiesToAway rounding mode numeral.
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
         /// </summary>
-        public FPRMNum MkFPRMNearestTiesToAway()
+        public FPRMNum MkFPRNE()
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            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 FPRMNum MkFPRoundNearestTiesToAway()
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
             return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
         }
 
         /// <summary>
-        /// Create a TowardPositive rounding mode numeral.
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
         /// </summary>
-        public FPRMNum MkFPRMTowardPositive()
+        public FPRMNum MkFPRNA()
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            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 FPRMNum MkFPRoundTowardPositive()
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
             return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
         }
 
         /// <summary>
-        /// Create a TowardNegative rounding mode numeral.
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
         /// </summary>
-        public FPRMNum MkFPRMTowardNegative()
+        public FPRMNum MkFPRTP()
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            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 FPRMNum MkFPRoundTowardNegative()
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
             return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
         }
 
         /// <summary>
-        /// Create a TowardZero rounding mode numeral.
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
         /// </summary>
-        public FPRMNum MkFPRMTowardZero()
+        public FPRMNum MkFPRTN()
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            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 FPRMNum MkFPRoundTowardZero()
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
             return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
         }
 
         /// <summary>
-        /// Create a floating point sort.
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
         /// </summary>
-        /// <param name="ebits">exponent bits in the floating point sort.</param>
-        /// <param name="sbits">significand bits in the floating point sort.</param>
+        public FPRMNum MkFPRTZ()
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
+        }        
+        #endregion
+        #endregion
+
+        #region FloatingPoint Sorts
+        /// <summary>
+        /// Create a FloatingPoint sort.
+        /// </summary>
+        /// <param name="ebits">exponent bits in the FloatingPoint sort.</param>
+        /// <param name="sbits">significand bits in the FloatingPoint sort.</param>
         public FPSort MkFPSort(uint ebits, uint sbits)
         {
             Contract.Ensures(Contract.Result<FPSort>() != null);
@@ -3505,9 +3558,83 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a floating point NaN numeral.
+        /// Create the half-precision (16-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortHalf()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
+        }
+
+        /// <summary>
+        /// Create the half-precision (16-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort16()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
+        }
+
+        /// <summary>
+        /// Create the single-precision (32-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortSingle()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
+        }
+
+        /// <summary>
+        /// Create the single-precision (32-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort32()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
+        }
+
+        /// <summary>
+        /// Create the double-precision (64-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortDouble()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
+        }
+
+        /// <summary>
+        /// Create the double-precision (64-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort64()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
+        }
+
+        /// <summary>
+        /// Create the quadruple-precision (128-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortQuadruple()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
+        }
+
+        /// <summary>
+        /// Create the quadruple-precision (128-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort128()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
+        }
+        #endregion
+        
+        #region Numerals
+        /// <summary>
+        /// Create a NaN of sort s.
         /// </summary>        
-        /// <param name="s">floating point sort.</param>        
+        /// <param name="s">FloatingPoint sort.</param>        
         public FPNum MkFPNaN(FPSort s)
         {
             Contract.Ensures(Contract.Result<FPRMNum>() != null);
@@ -3515,9 +3642,9 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a floating point Inf numeral.
+        /// Create a floating-point infinity of sort s.
         /// </summary>        
-        /// <param name="s">floating point sort.</param>   
+        /// <param name="s">FloatingPoint sort.</param>   
         /// <param name="negative">indicates whether the result should be negative.</param>
         public FPNum MkFPInf(FPSort s, bool negative)
         {
@@ -3526,20 +3653,141 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a floating point numeral.
-        /// </summary>
-        /// <param name="v">A string representing the value in decimal notation.</param>
-        /// <param name="s">floating point sort</param>
+        /// Create a floating-point zero of sort s.
+        /// </summary>        
+        /// <param name="s">FloatingPoint sort.</param>   
+        /// <param name="negative">indicates whether the result should be negative.</param>
+        public FPNum MkFPZero(FPSort s, bool negative)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(float v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPNum MkFPNumeral(double v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from an int.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(int v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_uint_int(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(bool sgn, UInt64 sig, Int64 exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_uint64_int64(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(float v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return MkFPNumeral(v, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>
         public FPNum MkFP(double v, FPSort s)
         {
-            Contract.Ensures(Contract.Result<FPNum>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_numeral_double(this.nCtx, v, s.NativeObject));
-        }    
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return MkFPNumeral(v, s);
+        }
 
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from an int.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(int v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return MkFPNumeral(v, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(bool sgn, uint sig, int exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return MkFPNumeral(sgn, sig, exp, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(bool sgn, UInt64 sig, Int64 exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMNum>() != null);
+            return MkFPNumeral(sgn, sig, exp, s);
+        }
+
+        #endregion
+
+        #region Operators
         /// <summary>
         /// Floating-point absolute value
         /// </summary>
-        /// <param name="t">floating point term</param>
+        /// <param name="t">floating-point term</param>
         public FPExpr MkFPAbs(FPExpr t) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3549,7 +3797,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Floating-point negation
         /// </summary>
-        /// <param name="t">floating point term</param>
+        /// <param name="t">floating-point term</param>
         public FPExpr MkFPNeg(FPExpr t) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3560,8 +3808,8 @@ namespace Microsoft.Z3
         /// Floating-point addition
         /// </summary>
         /// <param name="rm">rounding mode term</param>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3572,8 +3820,8 @@ namespace Microsoft.Z3
         /// Floating-point subtraction
         /// </summary>
         /// <param name="rm">rounding mode term</param>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3584,8 +3832,8 @@ namespace Microsoft.Z3
         /// Floating-point multiplication
         /// </summary>
         /// <param name="rm">rounding mode term</param>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3596,8 +3844,8 @@ namespace Microsoft.Z3
         /// Floating-point division
         /// </summary>
         /// <param name="rm">rounding mode term</param>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3611,9 +3859,9 @@ namespace Microsoft.Z3
         /// The result is round((t1 * t2) + t3)
         /// </remarks>
         /// <param name="rm">rounding mode term</param>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
-        /// <param name="t3">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        /// <param name="t3">floating-point term</param>
         public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3624,7 +3872,7 @@ namespace Microsoft.Z3
         /// Floating-point square root
         /// </summary>        
         /// <param name="rm">rounding mode term</param>        
-        /// <param name="t">floating point term</param>        
+        /// <param name="t">floating-point term</param>        
         public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
@@ -3634,33 +3882,53 @@ namespace Microsoft.Z3
         /// <summary>
         /// Floating-point remainder
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public FPExpr MkFPRem(FPExpr t1, FPExpr t2) 
         {
             Contract.Ensures(Contract.Result<FPNum>() != null);
             return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
         }
-   
+
         /// <summary>
-        /// Floating-point equality
-        /// </summary>
-        /// <remarks>
-        /// Note that this is IEEE 754 equality (as opposed to standard =).
-        /// </remarks>
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
-        public BoolExpr MkFPEq(FPExpr t1, FPExpr t2) 
-        {
-            Contract.Ensures(Contract.Result<BoolExpr>() != null);
-            return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
-        }
-   
-        /// <summary>
-        /// Floating-point less than or equal
+        /// Floating-point roundToIntegral. Rounds a floating-point number to 
+        /// the closest integer, again represented as a floating-point number.
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="rm">term of RoundingMode sort</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
+        {            
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Minimum of floating-point numbers.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Maximum of floating-point numbers.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }   
+        
+        /// <summary>
+        /// Floating-point less than or equal.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3668,10 +3936,10 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Floating-point less than
+        /// Floating-point less than.
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public BoolExpr MkFPLt(FPExpr t1, FPExpr t2) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3679,10 +3947,10 @@ namespace Microsoft.Z3
         }
     
         /// <summary>
-        /// Floating-point greater than or equal
+        /// Floating-point greater than or equal.
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3690,10 +3958,10 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Floating-point greater than
+        /// Floating-point greater than.
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
         public BoolExpr MkFPGt(FPExpr t1, FPExpr t2) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3701,9 +3969,23 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Predicate indicating whether t is a normal floating point number
+        /// Floating-point equality.
+        /// </summary>
+        /// <remarks>
+        /// Note that this is IEEE 754 equality (as opposed to standard =).
+        /// </remarks>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a normal floating-point number.
         /// </summary>        
-        /// <param name="t">floating point term</param>        
+        /// <param name="t">floating-point term</param>        
         public BoolExpr MkFPIsNormal(FPExpr t) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3711,9 +3993,9 @@ namespace Microsoft.Z3
         }
    
         /// <summary>
-        /// Predicate indicating whether t is a subnormal floating point number
+        /// Predicate indicating whether t is a subnormal floating-point number.
         /// </summary>        
-        /// <param name="t">floating point term</param>        
+        /// <param name="t">floating-point term</param>        
         public BoolExpr MkFPIsSubnormal(FPExpr t) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3721,29 +4003,29 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Predicate indicating whether t is a floating point number with zero value, i.e., +0 or -0.
+        /// Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
         /// </summary>        
-        /// <param name="t">floating point term</param>        
-        public BoolExpr MkFPIsZero(FPExpr t) 
-        {            
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsZero(FPExpr t)
+        {
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
             return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
         }
 
         /// <summary>
-        /// Predicate indicating whether t is a floating point number representing +Inf or -Inf
+        /// Predicate indicating whether t is a floating-point number representing +oo or -oo.
         /// </summary>        
-        /// <param name="t">floating point term</param>        
-        public BoolExpr MkFPIsInf(FPExpr t) 
-        {            
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsInfinite(FPExpr t)
+        {
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
             return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
         }
 
         /// <summary>
-        /// Predicate indicating whether t is a NaN
+        /// Predicate indicating whether t is a NaN.
         /// </summary>        
-        /// <param name="t">floating point term</param>        
+        /// <param name="t">floating-point term</param>        
         public BoolExpr MkFPIsNaN(FPExpr t) 
         {            
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
@@ -3751,45 +4033,212 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Floating-point minimum
+        /// Predicate indicating whether t is a negative floating-point number.
         /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
-        public FPExpr MkFPMin(FPExpr t1, FPExpr t2) 
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsNegative(FPExpr t)
         {
-            Contract.Ensures(Contract.Result<FPNum>() != null);
-            return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
         }
-   
-        /// <summary>
-        /// Floating-point maximium
-        /// </summary>        
-        /// <param name="t1">floating point term</param>
-        /// <param name="t2">floating point term</param>
-        public FPExpr MkFPMax(FPExpr t1, FPExpr t2) 
-        {
-            Contract.Ensures(Contract.Result<FPNum>() != null);
-            return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
-        }   
 
         /// <summary>
-        /// Conversion of a floating point number to another floating-point sort s.
+        /// Predicate indicating whether t is a positive floating-point number.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsPositive(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
+        }        
+        #endregion
+
+        #region Conversions to FloatingPoint terms
+        /// <summary>
+        /// Create an expression of FloatingPoint sort from three bit-vector expressions.
+        /// </summary>
+        /// <remarks>
+        /// This is the operator named `fp' in the SMT FP theory definition. 
+        /// Note that sgn is required to be a bit-vector of size 1. Significand and exponent 
+        /// are required to be greater than 1 and 2 respectively. The FloatingPoint sort 
+        /// of the resulting expression is automatically determined from the bit-vector sizes
+        /// of the arguments.
+        /// </remarks>
+        /// <param name="sgn">bit-vector term (of size 1) representing the sign.</param>
+        /// <param name="sig">bit-vector term representing the significand.</param>
+        /// <param name="exp">bit-vector term representing the exponent.</param>
+        public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of a bit-vector term bv to a 
+        /// floating-point term of sort s. The bit-vector size of bv (m) must be equal 
+        /// to ebits+sbits of s. The format of the bit-vector is as defined by the 
+        /// IEEE 754-2008 interchange format.
+        /// </remarks>
+        /// <param name="bv">bit-vector value (of size m).</param>
+        /// <param name="s">FloatingPoint sort (ebits+sbits == m)</param>
+        public FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of a floating-point term t to a
+        /// floating-point term of sort s. If necessary, the result will be rounded according
+        /// to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">FloatingPoint term.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a term of real sort into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of term t of real sort into a
+        /// floating-point term of sort s. If necessary, the result will be rounded according
+        /// to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">term of Real sort.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the bit-vector term t into a
+        /// floating-point term of sort s. The bit-vector t is taken to be in signed 
+        /// 2's complement format (when signed==true, otherwise unsigned). If necessary, the 
+        /// result will be rounded according to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">term of bit-vector sort.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        /// <param name="signed">flag indicating whether t is interpreted as signed or unsigned bit-vector.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            if (signed)
+                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+            else
+                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a floating-point number to another FloatingPoint sort s.
         /// </summary>
         /// <remarks>
         /// Produces a term that represents the conversion of a floating-point term t to a different
-        /// floating point sort s. If necessary, rounding according to rm is applied. 
+        /// FloatingPoint sort s. If necessary, rounding according to rm is applied. 
         /// </remarks>
-        /// <param name="s">floating point sort</param>
-        /// <param name="rm">floating point rounding mode term</param>
-        /// <param name="t">floating point term</param>
-        public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) 
+        /// <param name="s">FloatingPoint sort</param>
+        /// <param name="rm">floating-point rounding mode term</param>
+        /// <param name="t">floating-point term</param>
+        public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
         {
-            Contract.Ensures(Contract.Result<FPNum>() != null);
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
             return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
         }
 
         #endregion
 
+        #region Conversions from FloatingPoint terms
+        /// <summary>
+        /// Conversion of a floating-point term into a bit-vector.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
+        /// the result will be rounded according to rounding mode rm.
+        /// </remarks>        
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">FloatingPoint term</param>
+        /// <param name="sz">Size of the resulting bit-vector.</param>
+        /// <param name="signed">Indicates whether the result is a signed or unsigned bit-vector.</param>
+        public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
+        {
+            Contract.Ensures(Contract.Result<BitVecExpr>() != null);
+            if (signed)
+                return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
+            else
+                return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
+        }
+
+        /// <summary>
+        /// Conversion of a floating-point term into a real-numbered term.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// real number. Note that this type of conversion will often result in non-linear 
+        /// constraints over real terms.
+        /// </remarks>        
+        /// <param name="t">FloatingPoint term</param>
+        public RealExpr MkFPToReal(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<RealExpr>() != null);
+            return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
+        }
+        #endregion
+
+        #region Z3-specific extensions
+        /// <summary>
+        /// Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
+        /// </summary>
+        /// <remarks>
+        /// The size of the resulting bit-vector is automatically determined. Note that 
+        /// IEEE 754-2008 allows multiple different representations of NaN. This conversion 
+        /// knows only one NaN and it will always produce the same bit-vector represenatation of 
+        /// that NaN. 
+        /// </remarks>
+        /// <param name="t">FloatingPoint term.</param>
+        public BitVecExpr MkFPToIEEEBV(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BitVecExpr>() != null);
+            return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of sig * 2^exp into a 
+        /// floating-point term of sort s. If necessary, the result will be rounded
+        /// according to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="sig">Significand term of Real sort.</param>
+        /// <param name="exp">Exponent term of Int sort.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public BitVecExpr MkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<BitVecExpr>() != null);
+            return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_real_int(this.nCtx, rm.NativeObject, sig.NativeObject, exp.NativeObject, s.NativeObject));
+        }
+        #endregion
+        #endregion // Floating-point Arithmetic
+
         #region Miscellaneous
         /// <summary>
         /// Wraps an AST.
diff --git a/src/api/dotnet/FPExpr.cs b/src/api/dotnet/FPExpr.cs
index 0bb1e4c09..cbba272d1 100644
--- a/src/api/dotnet/FPExpr.cs
+++ b/src/api/dotnet/FPExpr.cs
@@ -26,7 +26,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {
     /// <summary>
-    /// Floating Point Expressions
+    /// FloatingPoint Expressions
     /// </summary>
     public class FPExpr : Expr
     {
diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index 044598e58..ab57d57c3 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -22,7 +22,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {
     /// <summary>
-    /// Floatiung Point Numerals
+    /// FloatiungPoint Numerals
     /// </summary>
     [ContractVerification(true)]
     public class FPNum : FPExpr
diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs
index b95816023..92fea1ad4 100644
--- a/src/api/dotnet/FPRMExpr.cs
+++ b/src/api/dotnet/FPRMExpr.cs
@@ -26,7 +26,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {
     /// <summary>
-    /// Floating Point Expressions
+    /// FloatingPoint RoundingMode Expressions
     /// </summary>
     public class FPRMExpr : Expr
     {
diff --git a/src/api/dotnet/FPRMNum.cs b/src/api/dotnet/FPRMNum.cs
index eaf105718..7caa56f9f 100644
--- a/src/api/dotnet/FPRMNum.cs
+++ b/src/api/dotnet/FPRMNum.cs
@@ -22,7 +22,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {
     /// <summary>
-    /// Floatiung Point Rounding Mode Numerals
+    /// FloatingPoint RoundingMode Numerals
     /// </summary>
     [ContractVerification(true)]
     public class FPRMNum : FPRMExpr
diff --git a/src/api/dotnet/FPRMSort.cs b/src/api/dotnet/FPRMSort.cs
index 23d454a65..1d8334eb5 100644
--- a/src/api/dotnet/FPRMSort.cs
+++ b/src/api/dotnet/FPRMSort.cs
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Z3 Managed API: Floating Point Rounding Mode Sorts
+    Z3 Managed API: Rounding Mode Sort
 
 Author:
 
@@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {
     /// <summary>
-    ///  A floating point rounding mode sort
+    /// The FloatingPoint RoundingMode sort
     /// </summary>
     public class FPRMSort : Sort
     {
diff --git a/src/api/dotnet/FPSort.cs b/src/api/dotnet/FPSort.cs
index a79557ae6..8d8560e53 100644
--- a/src/api/dotnet/FPSort.cs
+++ b/src/api/dotnet/FPSort.cs
@@ -16,17 +16,26 @@ Author:
 Notes:
     
 --*/
-
 using System;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Z3
 {
     /// <summary>
-    ///  A floating point sort
+    /// FloatingPoint sort
     /// </summary>
     public class FPSort : Sort
     {
+        /// <summary>
+        /// The number of exponent bits.
+        /// </summary>
+        public uint EBits { get { return Native.Z3_mk_fpa_get_ebits(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// The number of significand bits.
+        /// </summary>
+        public uint SBits { get { return Native.Z3_mk_fpa_get_ebits(Context.nCtx, NativeObject); } }
+
         #region Internal
         internal FPSort(Context ctx, IntPtr obj)
             : base(ctx, obj)
@@ -39,5 +48,5 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
         #endregion
-    }
+    }    
 }