From 97c7ce63b535337fcd5c195ea2720546477c972e Mon Sep 17 00:00:00 2001
From: John Fleisher <john.fleisher@gmail.com>
Date: Mon, 7 Mar 2022 15:55:30 -0500
Subject: [PATCH] Clean up build warnings (#5884)

* Clean up warnings in compile for documentation notes

* remove snk from local build

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/NativeContext.cs | 19 ++++++++++---------
 src/api/dotnet/NativeModel.cs   |  4 +++-
 2 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index 840c5b864..f8513a7e6 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -308,25 +308,25 @@ namespace Microsoft.Z3
         /// Integer Sort
         /// </summary>
         public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx);
+
         /// <summary>
-        /// Boolean Sort
+        /// Returns the "singleton" BoolSort for this NativeContext
         /// </summary>
         public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx);
+
         /// <summary>
-        /// Real Sort
+        /// Returns the "singleton" RealSort for this NativeContext
         /// </summary>
         public Z3_sort RealSort => Native.Z3_mk_real_sort(nCtx);
 
+
         /// <summary>
-        /// Bit-vector sort
+        /// Returns the BvSort for size in this NativeContext
         /// </summary>
-        /// <param name="size"></param>
-        /// <returns></returns>
         public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size);
 
         /// <summary>
-        /// Given an elemSort create a List of elemSort 
-        /// The function returns the list sort, constructors, accessors and recognizers
+        /// returns ListSort
         /// </summary>
         /// <param name="name"></param>
         /// <param name="elemSort"></param>
@@ -436,7 +436,7 @@ namespace Microsoft.Z3
 
         #region Symbol
         /// <summary>
-        /// Create a symbol from a string
+        /// Return a ptr to symbol for string
         /// </summary>
         /// <param name="name"></param>
         /// <returns></returns>
@@ -809,6 +809,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
+        /// Same as MkForAll but defaults to "forall" = false
         /// Create an existential Quantifier.
         /// </summary>
         /// <param name="sorts"></param>
@@ -1142,7 +1143,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Retrieve number of arguments to a function application
+        /// Return number of arguments for app
         /// </summary>
         /// <param name="app"></param>
         /// <returns></returns>
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
index eb6037199..3b9eb0950 100644
--- a/src/api/dotnet/NativeModel.cs
+++ b/src/api/dotnet/NativeModel.cs
@@ -251,12 +251,14 @@ namespace Microsoft.Z3
             public Z3_ast Else;
 
             /// <summary>
+            /// Domain for array
             /// Updates.Keys
             /// </summary>
             public Z3_ast[] Domain;
 
             /// <summary>
-            /// Updates.Range
+            /// Range for array
+            /// Updates.Values
             /// </summary>
             public Z3_ast[] Range;
         }