diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index 1aca7fe55..a19e0c5af 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -197,6 +197,11 @@ namespace Microsoft.Z3
 
         }
 
+        /// <summary>
+        /// Retrieve statistics as an array of entries
+        /// </summary>
+        /// <param name="stats"></param>
+        /// <returns></returns>
         public Statistics.Entry[] GetStatistics(Z3_stats stats)
         {
             Native.Z3_stats_inc_ref(nCtx, stats);
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
index 9e5cc44a1..417426b3b 100644
--- a/src/api/dotnet/NativeModel.cs
+++ b/src/api/dotnet/NativeModel.cs
@@ -261,6 +261,11 @@ namespace Microsoft.Z3
             public Z3_ast Else;
         }
 
+        /// <summary>
+        /// Convert the interpretation of t into a sequence of array updates
+        /// </summary>
+        /// <param name="t"></param>
+        /// <returns>null if the argument does evaluate to a sequence of stores to an array</returns>
         public ArrayValue TryGetArrayValue(Z3_ast t)
         {
             var r = Eval(t, true);