diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs
index 403d18736..93d283771 100644
--- a/src/api/dotnet/Constructor.cs
+++ b/src/api/dotnet/Constructor.cs
@@ -33,7 +33,11 @@ namespace Microsoft.Z3
         /// </summary>
         public uint NumFields
         {
-            get { init();  return n; }
+            get
+            {
+                init();
+                return n;
+            }
         }
 
         /// <summary>
@@ -41,9 +45,12 @@ namespace Microsoft.Z3
         /// </summary>
         public FuncDecl ConstructorDecl
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                init();  return m_constructorDecl; }
+                init();
+                return m_constructorDecl;
+            }
         }
 
         /// <summary>
@@ -51,9 +58,12 @@ namespace Microsoft.Z3
         /// </summary>
         public FuncDecl TesterDecl
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                init();  return m_testerDecl; }
+                init();
+                return m_testerDecl;
+            }
         }
 
         /// <summary>
@@ -61,10 +71,13 @@ namespace Microsoft.Z3
         /// </summary>
         public FuncDecl[] AccessorDecls
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-                init();  return m_accessorDecls; }
-        }        
+                init(); 
+                return m_accessorDecls;
+            }
+        }
 
         /// <summary>
         /// Destructor.
@@ -79,10 +92,10 @@ namespace Microsoft.Z3
         [ContractInvariantMethod]
         private void ObjectInvariant()
         {
-            Contract.Invariant(m_testerDecl  == null || m_constructorDecl != null);
+            Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
             Contract.Invariant(m_testerDecl == null || m_accessorDecls != null);
         }
-        
+
         #endregion
 
         #region Internal
@@ -105,7 +118,7 @@ namespace Microsoft.Z3
                 throw new Z3Exception("Number of field names does not match number of sorts");
             if (sortRefs != null && sortRefs.Length != n)
                 throw new Z3Exception("Number of field names does not match number of sort refs");
-            
+
             if (sortRefs == null) sortRefs = new uint[n];
 
             NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
@@ -116,7 +129,7 @@ namespace Microsoft.Z3
 
         }
 
-        private void init() 
+        private void init()
         {
             Contract.Ensures(m_constructorDecl != null);
             Contract.Ensures(m_testerDecl != null);
@@ -146,7 +159,7 @@ namespace Microsoft.Z3
         /// Destructor.
         /// </summary>
         ~ConstructorList()
-        {         
+        {
             Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
         }
 
@@ -164,7 +177,7 @@ namespace Microsoft.Z3
             Contract.Requires(constructors != null);
 
             NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
-        }        
+        }
         #endregion
     }
 }
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 428381ae8..c559e61e9 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -48,9 +48,11 @@ namespace Microsoft.Z3
         /// </summary>
         public FuncDecl FuncDecl
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject)); }
+                return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
+            }
         }
 
         /// <summary>
@@ -74,7 +76,7 @@ namespace Microsoft.Z3
         /// The arguments of the expression.
         /// </summary>        
         public Expr[] Args
-        {            
+        {
             get
             {
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
@@ -176,7 +178,7 @@ namespace Microsoft.Z3
         public override string ToString()
         {
             return base.ToString();
-        }        
+        }
 
         /// <summary>
         /// Indicates whether the term is a numeral
@@ -200,9 +202,11 @@ namespace Microsoft.Z3
         /// </summary>
         public Sort Sort
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<Sort>() != null);
-                return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject)); }
+                return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
+            }
         }
 
         #region Constants
@@ -243,7 +247,7 @@ namespace Microsoft.Z3
         {
             get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
         }
-        #endregion        
+        #endregion
 
         #region Term Kind Tests
 
@@ -1471,12 +1475,16 @@ namespace Microsoft.Z3
         #endregion
 
         #region Internal
-        /// <summary> Constructor for Expr </summary>
+        /// <summary> 
+        /// Constructor for Expr 
+        /// </summary>
         internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> Constructor for Expr </summary>
+        /// <summary> 
+        /// Constructor for Expr 
+        /// </summary>
         internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
-        #if DEBUG
+#if DEBUG
         [Pure]
         internal override void CheckNativeObject(IntPtr obj)
         {
@@ -1486,7 +1494,7 @@ namespace Microsoft.Z3
                 throw new Z3Exception("Underlying object is not a term");
             base.CheckNativeObject(obj);
         }
-        #endif
+#endif
 
         [Pure]
         internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
@@ -1495,11 +1503,11 @@ namespace Microsoft.Z3
             Contract.Requires(f != null);
             Contract.Ensures(Contract.Result<Expr>() != null);
 
-            IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject, 
-                                          AST.ArrayLength(arguments), 
+            IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
+                                          AST.ArrayLength(arguments),
                                           AST.ArrayToNative(arguments));
             return Create(ctx, obj);
-        }        
+        }
 
         [Pure]
         new internal static Expr Create(Context ctx, IntPtr obj)
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index aca013318..c19a7cb04 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -264,7 +264,8 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
-        public BoolExpr[] Rules {
+        public BoolExpr[] Rules
+        {
             get
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
@@ -281,7 +282,8 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieve set of assertions added to fixedpoint context.
         /// </summary>                
-        public BoolExpr[] Assertions {
+        public BoolExpr[] Assertions
+        {
             get
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index b1599bbf4..ef64ce767 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -124,9 +124,11 @@ namespace Microsoft.Z3
         /// </summary>
         public Sort Range
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<Sort>() != null);
-                return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject)); }
+                return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
+            }
         }
 
         /// <summary>
@@ -142,9 +144,11 @@ namespace Microsoft.Z3
         /// </summary>
         public Symbol Name
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<Symbol>() != null);
-                return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject)); }
+                return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
+            }
         }
 
         /// <summary>
@@ -280,9 +284,10 @@ namespace Microsoft.Z3
         }
 
         #region Internal
-        internal FuncDecl(Context ctx, IntPtr obj) : base(ctx, obj) 
-        { 
-            Contract.Requires(ctx != null); 
+        internal FuncDecl(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
         }
 
         internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
@@ -293,7 +298,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);
             Contract.Requires(range != null);
-        }        
+        }
 
         internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
             : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix,
@@ -304,14 +309,14 @@ namespace Microsoft.Z3
             Contract.Requires(range != null);
         }
 
-        #if DEBUG
+#if DEBUG
         internal override void CheckNativeObject(IntPtr obj)
         {
             if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_FUNC_DECL_AST)
                 throw new Z3Exception("Underlying object is not a function declaration");
             base.CheckNativeObject(obj);
         }
-        #endif
+#endif
         #endregion
 
         /// <summary>
@@ -319,12 +324,14 @@ namespace Microsoft.Z3
         /// </summary>
         /// <param name="args"></param>
         /// <returns></returns>
-        public Expr this[params Expr[] args] { 
-            get {
+        public Expr this[params Expr[] args]
+        {
+            get
+            {
                 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
 
-                return Apply(args); 
-            } 
+                return Apply(args);
+            }
         }
 
         /// <summary>