From 7bbabcdf6dadcc133044f7b36e0647583ec63796 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Aug 2013 14:47:48 -0700
Subject: [PATCH] updated documentation for finite domain sizes

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

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 68cca046e..ae8b233d1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -303,6 +303,9 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create a new finite domain sort.
+	/// <param name="name">The name used to identify the sort</param>
+	/// <param size="size">The size of the sort</param>
+	/// <returns>The result is a sort</returns>
         /// </summary>
         public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
         {
@@ -315,6 +318,11 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create a new finite domain sort.
+	/// <param name="name">The name used to identify the sort</param>
+	/// <param size="size">The size of the sort</param>
+	/// <returns>The result is a sort</returns>
+	/// Elements of the sort are created using <seealso cref="MkNumeral"/>, 
+	/// and the elements range from 0 to <tt>size-1</tt>.
         /// </summary>
         public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
         {
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 458e2f53f..2b8c74e65 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1721,6 +1721,8 @@ extern "C" {
        To create constants that belong to the finite domain, 
        use the APIs for creating numerals and pass a numeric
        constant together with the sort returned by this call.
+       The numeric constant should be between 0 and the less 
+       than the size of the domain.
 
        \sa Z3_get_finite_domain_sort_size