From 5d1339beec902151e801dba46cac633d201c2d8d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 17 May 2013 13:43:32 +0100
Subject: [PATCH] .NET/Java: API doc update for Context constructor.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/dotnet/Context.cs | 15 +++++++++++++++
 src/api/java/Context.java | 15 +++++++++++++++
 2 files changed, 30 insertions(+)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 35fe6611d..68cca046e 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -44,6 +44,21 @@ namespace Microsoft.Z3
         /// <summary>
         /// Constructor.
         /// </summary>
+        /// <remarks>
+        /// The following parameters can be set:        
+        ///     - proof  (Boolean)           Enable proof generation
+        ///     - debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting 
+        ///     - trace  (Boolean)           Tracing support for VCC
+        ///     - trace_file_name (String)   Trace out file for VCC traces
+        ///     - timeout (unsigned)         default timeout (in milliseconds) used for solvers
+        ///     - well_sorted_check          type checker
+        ///     - auto_config                use heuristics to automatically select solver and configure it
+        ///     - model                      model generation for solvers, this parameter can be overwritten when creating a solver
+        ///     - model_validate             validate models produced by solvers
+        ///     - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
+        /// Note that in previous versions of Z3, this constructor was also used to set global and module parameters. 
+        /// For this purpose we should now use <see cref="Global.SetParameter"/>
+        /// </remarks>
         public Context(Dictionary<string, string> settings)
             : base()
         {
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 5277dab38..6b6c63ac3 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -27,6 +27,21 @@ public class Context extends IDisposable
 
     /**
      * Constructor.
+     * <remarks>
+     * The following parameters can be set:        
+     *     - proof  (Boolean)           Enable proof generation
+     *     - debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting 
+     *     - trace  (Boolean)           Tracing support for VCC
+     *     - trace_file_name (String)   Trace out file for VCC traces
+     *     - timeout (unsigned)         default timeout (in milliseconds) used for solvers
+     *     - well_sorted_check          type checker
+     *     - auto_config                use heuristics to automatically select solver and configure it
+     *     - model                      model generation for solvers, this parameter can be overwritten when creating a solver
+     *     - model_validate             validate models produced by solvers
+     *     - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
+     * Note that in previous versions of Z3, this constructor was also used to set global and 
+     * module parameters. For this purpose we should now use <see cref="Global.setParameter"/>
+     * </remarks>
      **/
     public Context(Map<String, String> settings) throws Z3Exception
     {