diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index db3cd30b2..75393378b 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -839,7 +839,7 @@ namespace test_mapi
             // Error handling test.
             try
             {
-                Expr plus_ri = ctx.MkAdd(ctx.MkInt(1), ctx.MkReal(2));
+                IntExpr i = ctx.MkInt("1/2");
                 throw new TestFailedException(); // unreachable
             }
             catch (Z3Exception)
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 3e438d69d..ff36b4553 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -113,7 +113,6 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<BoolSort>() != null);
-
                 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
             }
         }
@@ -134,7 +133,14 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieves the Real sort of the context.
         /// </summary>
-        public RealSort RealSort { get { Contract.Ensures(Contract.Result<RealSort>() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } }
+        public RealSort RealSort
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<RealSort>() != null); 
+                if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
+            }
+        }
 
         /// <summary>
         /// Create a new Boolean sort.
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index dade77eb1..9f5c04f0b 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -1532,8 +1532,7 @@ namespace Microsoft.Z3
                 {
                     case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
                     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_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
+                    case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);                    
                 }
             }
 
@@ -1544,8 +1543,7 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
                 case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
                 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
-                case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
-                case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
+                case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);                
             }
 
             return new Expr(ctx, obj);