diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index b03cfd28c..0c33d6793 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -2084,25 +2084,26 @@ namespace test_mapi
 
             FPRMExpr rm = (FPRMExpr)ctx.MkConst(ctx.MkSymbol("rm"), rm_sort);
             BitVecExpr x = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkBitVecSort(64));
-            FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);
-            RealExpr real_val = ctx.MkReal(42);
-            BitVecExpr bv_val = ctx.MkBV(42, 64);
+            FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort);            
             FPExpr fp_val = ctx.MkFP(42, double_sort);
 
-            BoolExpr c1 = ctx.MkEq(x, ctx.MkFPToIEEEBV(fp_val));
-            BoolExpr c2 = ctx.MkEq(x, ctx.MkBV(42, 64));
-            BoolExpr c3 = ctx.MkEq(fp_val, ctx.MkFPToFP(rm, real_val, double_sort));
-            BoolExpr c4 = ctx.MkAnd(c1, c2);
-            Console.WriteLine("c3 = " + c3);
+            BoolExpr c1 = ctx.MkEq(y, fp_val);
+            BoolExpr c2 = ctx.MkEq(x, ctx.MkFPToBV(rm, y, 64, false));
+            BoolExpr c3 = ctx.MkEq(x, ctx.MkBV(42, 64));
+            BoolExpr c4 = ctx.MkEq(ctx.MkNumeral(42, ctx.RealSort), ctx.MkFPToReal(fp_val));
+            BoolExpr c5 = ctx.MkAnd(c1, c2, c3, c4);
+            Console.WriteLine("c5 = " + c5);
 
             /* Generic solver */
             Solver s = ctx.MkSolver();
-            s.Assert(c3);
+            s.Assert(c5);
+            
+            Console.WriteLine(s);
 
             if (s.Check() != Status.SATISFIABLE)
                 throw new TestFailedException();
 
-            Console.WriteLine("OK, model: ", s.Model.ToString());
+            Console.WriteLine("OK, model: {0}", s.Model.ToString());
         }
 
         static void Main(string[] args)
diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs
index 7bc4f6dfb..d3b31a325 100644
--- a/src/api/dotnet/AST.cs
+++ b/src/api/dotnet/AST.cs
@@ -227,10 +227,8 @@ namespace Microsoft.Z3
         internal override void IncRef(IntPtr o)
         {            
             // Console.WriteLine("AST IncRef()");
-            if (Context == null)
-                throw new Z3Exception("inc() called on null context");
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("inc() called on null AST");
+            if (Context == null || o == IntPtr.Zero)
+                return;
             Context.AST_DRQ.IncAndClear(Context, o);
             base.IncRef(o);
         }
@@ -238,10 +236,8 @@ namespace Microsoft.Z3
         internal override void DecRef(IntPtr o)
         {
             // Console.WriteLine("AST DecRef()");
-            if (Context == null)
-                throw new Z3Exception("dec() called on null context");
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("dec() called on null AST");
+            if (Context == null || o == IntPtr.Zero)
+                return;
             Context.AST_DRQ.Add(o);
             base.DecRef(o);
         }
diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs
index bdfa7a3f0..7858ff3e1 100644
--- a/src/api/dotnet/ArithExpr.cs
+++ b/src/api/dotnet/ArithExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArithExpr </summary>
-        internal protected ArithExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArithExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/ArrayExpr.cs b/src/api/dotnet/ArrayExpr.cs
index 915bfd0f1..e14bb1083 100644
--- a/src/api/dotnet/ArrayExpr.cs
+++ b/src/api/dotnet/ArrayExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArrayExpr </summary>
-        internal protected ArrayExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArrayExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/BitVecExpr.cs b/src/api/dotnet/BitVecExpr.cs
index a146e7a19..b019f8845 100644
--- a/src/api/dotnet/BitVecExpr.cs
+++ b/src/api/dotnet/BitVecExpr.cs
@@ -41,7 +41,6 @@ namespace Microsoft.Z3
 
         #region Internal
         /// <summary> Constructor for BitVecExpr </summary>
-        internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }
diff --git a/src/api/dotnet/BoolExpr.cs b/src/api/dotnet/BoolExpr.cs
index cbe3b1868..a9a15e4dc 100644
--- a/src/api/dotnet/BoolExpr.cs
+++ b/src/api/dotnet/BoolExpr.cs
@@ -32,8 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for BoolExpr </summary>
-        internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> Constructor for BoolExpr </summary>
         internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }
diff --git a/src/api/dotnet/DatatypeExpr.cs b/src/api/dotnet/DatatypeExpr.cs
index 93cea54f5..ba3a9d478 100644
--- a/src/api/dotnet/DatatypeExpr.cs
+++ b/src/api/dotnet/DatatypeExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for DatatypeExpr </summary>
-        internal protected DatatypeExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal DatatypeExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs
index e62043078..f7ba98222 100644
--- a/src/api/dotnet/EnumSort.cs
+++ b/src/api/dotnet/EnumSort.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 5f0c4218c..97e57b920 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -1759,10 +1759,6 @@ namespace Microsoft.Z3
         /// <summary> 
         /// Constructor for Expr 
         /// </summary>
-        internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> 
-        /// Constructor for Expr 
-        /// </summary>
         internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG
diff --git a/src/api/dotnet/FPExpr.cs b/src/api/dotnet/FPExpr.cs
index bbd557017..85fdf2603 100644
--- a/src/api/dotnet/FPExpr.cs
+++ b/src/api/dotnet/FPExpr.cs
@@ -42,11 +42,6 @@ namespace Microsoft.Z3
 
         #region Internal
         /// <summary> Constructor for FPExpr </summary>
-        internal protected FPExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal FPExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs
index 92fea1ad4..896c3e6b9 100644
--- a/src/api/dotnet/FPRMExpr.cs
+++ b/src/api/dotnet/FPRMExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for FPRMExpr </summary>
-        internal protected FPRMExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal FPRMExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/IntExpr.cs b/src/api/dotnet/IntExpr.cs
index 58bf1b973..622be7bd5 100644
--- a/src/api/dotnet/IntExpr.cs
+++ b/src/api/dotnet/IntExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for IntExpr </summary>
-        internal protected IntExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal IntExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/ListSort.cs b/src/api/dotnet/ListSort.cs
index 7dbafb385..e860e4d4b 100644
--- a/src/api/dotnet/ListSort.cs
+++ b/src/api/dotnet/ListSort.cs
@@ -113,9 +113,9 @@ namespace Microsoft.Z3
             }
         }
 
-        #region Internal        
+        #region Internal
         internal ListSort(Context ctx, Symbol name, Sort elemSort)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);
diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs
index f59d0bda2..38e435309 100644
--- a/src/api/dotnet/Quantifier.cs
+++ b/src/api/dotnet/Quantifier.cs
@@ -160,7 +160,7 @@ namespace Microsoft.Z3
         #region Internal
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(sorts != null);
@@ -203,7 +203,7 @@ namespace Microsoft.Z3
 
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(body != null);
diff --git a/src/api/dotnet/RealExpr.cs b/src/api/dotnet/RealExpr.cs
index 26adc1fc6..8ee8c8e76 100644
--- a/src/api/dotnet/RealExpr.cs
+++ b/src/api/dotnet/RealExpr.cs
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for RealExpr </summary>
-        internal protected RealExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal RealExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {
diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs
index 9dc23ea09..412398ddd 100644
--- a/src/api/dotnet/Sort.cs
+++ b/src/api/dotnet/Sort.cs
@@ -116,8 +116,7 @@ namespace Microsoft.Z3
         #region Internal
         /// <summary>
         /// Sort constructor
-        /// </summary>
-        internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
+        /// </summary>        
         internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG
@@ -146,6 +145,8 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
                 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
                 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
+                case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
+                case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
                 default:
                     throw new Z3Exception("Unknown sort kind");
             }
diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs
index 81a0eaf60..ea99f3855 100644
--- a/src/api/dotnet/TupleSort.cs
+++ b/src/api/dotnet/TupleSort.cs
@@ -68,7 +68,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);