From 757cf7622d549d5280748464366092aa198a5def Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 Mar 2022 10:59:19 -0800
Subject: [PATCH] sketch ArrayValue, add statistics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/NativeContext.cs | 5 +++++
 src/api/dotnet/NativeModel.cs   | 5 +++++
 2 files changed, 10 insertions(+)

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);