diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index 6961b39dd..96e0487de 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -235,7 +235,7 @@ namespace Microsoft.Z3
         public Z3_ast MkReal(string v)
         {
             Debug.Assert(!string.IsNullOrEmpty(v));
-            return Native.Z3_mk_numeral(nCtx, v, MkRealSort());
+            return Native.Z3_mk_numeral(nCtx, v, RealSort);
         }
 
         /// <summary>
@@ -304,10 +304,14 @@ namespace Microsoft.Z3
 
         #region Sort
 
-        public Z3_sort MkIntSort() => Native.Z3_mk_int_sort(nCtx);
-        public Z3_sort MkBoolSort() => Native.Z3_mk_bool_sort(nCtx);
+        /// <summary>
+        /// Sorts return same ptr for subsequent calls
+        /// </summary>
+        public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx);
+        public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx);
+        public Z3_sort RealSort => Native.Z3_mk_real_sort(nCtx);
+
         public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size);
-        public Z3_sort MkRealSort() => Native.Z3_mk_real_sort(nCtx);
 
         public Z3_sort MkListSort(string name, Z3_sort elemSort,
                                     out Z3_func_decl inil, out Z3_func_decl iisnil,
@@ -1086,17 +1090,24 @@ namespace Microsoft.Z3
         /// <returns></returns>
         public Z3_ast[] GetAppArgs(Z3_app app)
         {
-            Debug.Assert(app != IntPtr.Zero);
-
-            var numArgs = Native.Z3_get_app_num_args(nCtx, app);
+            var numArgs = GetNumArgs(app);
             var args = new Z3_ast[numArgs];
             for (uint i = 0; i < numArgs; i++)
             {
-                args[i] = Native.Z3_get_app_arg(nCtx, app, i);
+                args[i] = GetAppArg(app, i);
             }
             return args;
         }
 
+        public uint GetNumArgs(Z3_app app)
+        {
+            Debug.Assert(app != IntPtr.Zero);
+
+            return Native.Z3_get_app_num_args(nCtx, app);
+        }
+
+        internal Z3_ast GetAppArg(Z3_app app, uint i) => Native.Z3_get_app_arg(nCtx, app, i);
+
         /// <summary>
         /// Get App Decl from IntPtr
         /// </summary>
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
index ffd4e0faf..96eb13cd2 100644
--- a/src/api/dotnet/NativeModel.cs
+++ b/src/api/dotnet/NativeModel.cs
@@ -41,7 +41,7 @@ namespace Microsoft.Z3
         /// </summary>
         /// <param name="a">A Constant</param>
         /// <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
-        public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(Context.nCtx, a));
+        public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(ntvContext.nCtx, a));
 
         /// <summary>
         /// Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model. 
@@ -50,10 +50,10 @@ namespace Microsoft.Z3
         /// <returns>An expression if the function has an interpretation in the model, null otherwise.</returns>    
         public Z3_ast ConstFuncInterp(Z3_func_decl f)
         {
-            if (Native.Z3_get_arity(Context.nCtx, f) != 0)
+            if (Native.Z3_get_arity(ntvContext.nCtx, f) != 0)
                 throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
 
-            return Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+            return Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
         }
 
         /// <summary>
@@ -63,11 +63,11 @@ namespace Microsoft.Z3
         /// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns> 
         public NativeFuncInterp FuncInterp(Z3_func_decl f)
         {
-            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f));
+            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ntvContext.nCtx, Native.Z3_get_range(ntvContext.nCtx, f));
 
-            if (Native.Z3_get_arity(Context.nCtx, f) == 0)
+            if (Native.Z3_get_arity(ntvContext.nCtx, f) == 0)
             {
-                IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+                IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
 
                 if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
                 {
@@ -75,10 +75,10 @@ namespace Microsoft.Z3
                         return null;
                     else
                     {
-                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
+                        if (Native.Z3_is_as_array(ntvContext.nCtx, n) == 0)
                             throw new Z3Exception("Argument was not an array constant");
-                        var fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
-                        return new NativeFuncInterp(Context, this, f, fd);
+                        var fd = Native.Z3_get_as_array_func_decl(ntvContext.nCtx, n);
+                        return new NativeFuncInterp(ntvContext, this, f, fd);
                     }
                 }
                 else
@@ -88,11 +88,11 @@ namespace Microsoft.Z3
             }
             else
             {
-                IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f);
+                IntPtr n = Native.Z3_model_get_func_interp(ntvContext.nCtx, NativeObject, f);
                 if (n == IntPtr.Zero)
                     return null;
                 else
-                    return new NativeFuncInterp(Context, this, f, n);
+                    return new NativeFuncInterp(ntvContext, this, f, n);
             }
         }
 
@@ -103,7 +103,7 @@ namespace Microsoft.Z3
         /// </summary>
         public uint NumConsts
         {
-            get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
+            get { return Native.Z3_model_get_num_consts(ntvContext.nCtx, NativeObject); }
         }
 
 
@@ -118,7 +118,7 @@ namespace Microsoft.Z3
                 uint n = NumConsts;
                 Z3_func_decl[] res = new Z3_func_decl[n];
                 for (uint i = 0; i < n; i++)
-                    res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
+                    res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);
                 return res;
             }
         }
@@ -134,24 +134,22 @@ namespace Microsoft.Z3
                 uint nc = NumConsts;
                 for (uint i = 0; i < nc; ++i)
                 {
-                    var f = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
-                    IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f);
+                    var f = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);
+                    IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
                     if (n == IntPtr.Zero) continue;
                     yield return new KeyValuePair<Z3_func_decl, Z3_ast>(f, n);
                 }
             }
         }
 
-
         /// <summary>
         /// The number of function interpretations in the model.
         /// </summary>
         public uint NumFuncs
         {
-            get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
+            get { return Native.Z3_model_get_num_funcs(ntvContext.nCtx, NativeObject); }
         }
 
-
         /// <summary>
         /// The function declarations of the function interpretations in the model.
         /// </summary>
@@ -163,12 +161,11 @@ namespace Microsoft.Z3
                 uint n = NumFuncs;
                 Z3_func_decl[] res = new Z3_func_decl[n];
                 for (uint i = 0; i < n; i++)
-                    res[i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
+                    res[i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i);
                 return res;
             }
         }
 
-
         /// <summary>
         /// All symbols that have an interpretation in the model.
         /// </summary>
@@ -182,9 +179,9 @@ namespace Microsoft.Z3
                 uint n = nFuncs + nConsts;
                 Z3_func_decl[] res = new Z3_func_decl[n];
                 for (uint i = 0; i < nConsts; i++)
-                    res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i);
+                    res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);
                 for (uint i = 0; i < nFuncs; i++)
-                    res[nConsts + i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i);
+                    res[nConsts + i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i);
                 return res;
             }
         }
@@ -200,7 +197,6 @@ namespace Microsoft.Z3
             public ModelEvaluationFailedException() : base() { }
         }
 
-
         /// <summary>
         /// Evaluates the expression <paramref name="t"/> in the current model.
         /// </summary>
@@ -219,7 +215,7 @@ namespace Microsoft.Z3
         {
 
             IntPtr v = IntPtr.Zero;
-            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
+            if (Native.Z3_model_eval(ntvContext.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
                 throw new ModelEvaluationFailedException();
             else
                 return v;
@@ -236,7 +232,7 @@ namespace Microsoft.Z3
         public double Double(Z3_ast t)
         {
             var r = Eval(t, true);
-            return Native.Z3_get_numeral_double(Context.nCtx, r);
+            return Native.Z3_get_numeral_double(ntvContext.nCtx, r);
         }
 
         /// <summary>
@@ -269,33 +265,28 @@ namespace Microsoft.Z3
         {
             var r = Eval(t, true);
             // check that r is a sequence of store over a constant default array.
-            var updates = new List<KeyValuePair<Z3_ast, Z3_ast>>();
+            var updates = new Dictionary<Z3_ast, Z3_ast>();
             result = null;
             while (true)
             {
-                if (Context.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
+                if (ntvContext.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
                     return false;
-                Z3_func_decl f = Context.GetAppDecl(r);
-                var kind = Context.GetDeclKind(f);
+                Z3_func_decl f = ntvContext.GetAppDecl(r);
+                var kind = ntvContext.GetDeclKind(f);
                 if (kind == Z3_decl_kind.Z3_OP_CONST_ARRAY)
                 {
-#if false
-// TODO
                     result = new ArrayValue();
                     result.Else = r;
                     result.Updates = updates.ToArray();
-                    result.Domain = updates.Select((x, y) => x).ToArray();
-                    result.Range = updates.Select((x, y) => y).ToArray();
-#endif
+                    result.Domain = updates.Keys.ToArray();
+                    result.Range = updates.Values.ToArray();
                     return true;
                 }
                 else if (kind == Z3_decl_kind.Z3_OP_STORE)
                 {
-#if false
-                    Debug.Assert(Context.NumArgs(r) == 3);
-                    updates.Add(new KeyValuePair(Context.GetArg(r, 1), Context.GetArg(r, 2)));
-                    r = Context.GetArg(r, 0);
-#endif
+                    Debug.Assert(ntvContext.GetNumArgs(r) == 3);
+                    updates[ntvContext.GetAppArg(r, 1)] = ntvContext.GetAppArg(r, 2);
+                    r = ntvContext.GetAppArg(r, 0);
                 }
                 else
                 {
@@ -308,7 +299,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// The number of uninterpreted sorts that the model has an interpretation for.
         /// </summary>    
-        public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }
+        public uint NumSorts { get { return Native.Z3_model_get_num_sorts(ntvContext.nCtx, NativeObject); } }
 
 
         /// <summary>
@@ -328,7 +319,7 @@ namespace Microsoft.Z3
                 uint n = NumSorts;
                 Z3_sort[] res = new Z3_sort[n];
                 for (uint i = 0; i < n; i++)
-                    res[i] = Native.Z3_model_get_sort(Context.nCtx, NativeObject, i);
+                    res[i] = Native.Z3_model_get_sort(ntvContext.nCtx, NativeObject, i);
                 return res;
             }
         }
@@ -340,16 +331,16 @@ namespace Microsoft.Z3
         /// <returns>A string representation of the model.</returns>
         public override string ToString()
         {
-            return Native.Z3_model_to_string(Context.nCtx, NativeObject);
+            return Native.Z3_model_to_string(ntvContext.nCtx, NativeObject);
         }
 
 
         IntPtr NativeObject;
-        NativeContext Context;
+        NativeContext ntvContext;
 
         internal NativeModel(NativeContext ctx, IntPtr obj)
         {
-            Context = ctx;
+            ntvContext = ctx;
             NativeObject = obj;
             Debug.Assert(ctx != null);
             Native.Z3_model_inc_ref(ctx.nCtx, obj);
@@ -371,7 +362,7 @@ namespace Microsoft.Z3
         {
             if (NativeObject != IntPtr.Zero)
             {
-                Native.Z3_model_dec_ref(Context.nCtx, NativeObject);
+                Native.Z3_model_dec_ref(ntvContext.nCtx, NativeObject);
                 NativeObject = IntPtr.Zero;
             }
             GC.SuppressFinalize(this);
diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs
index 00110d550..40444804a 100644
--- a/src/api/dotnet/NativeSolver.cs
+++ b/src/api/dotnet/NativeSolver.cs
@@ -19,9 +19,9 @@ Notes:
 --*/
 
 using System;
+using System.Diagnostics;
 using System.Collections.Generic;
 using System.Linq;
-using System.Diagnostics;
 
 namespace Microsoft.Z3
 {