diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 47294244a..41ac1fa31 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -302,11 +302,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>
+        /// Create a new finite domain sort.	    
+	    /// <returns>The result is a sort</returns>
         /// </summary>
+        /// <param name="name">The name used to identify the sort</param>
+        /// <param name="size">The size of the sort</param>
         public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
         {
             Contract.Requires(name != null);
@@ -317,13 +317,13 @@ 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>.
+        /// Create a new finite domain sort.	    
+	    /// <returns>The result is a sort</returns>
+	    /// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>, 
+	    /// and the elements range from 0 to <tt>size-1</tt>.
         /// </summary>
+        /// <param name="name">The name used to identify the sort</param>
+        /// <param name="size">The size of the sort</param>
         public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
         {
             Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);
diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs
index 707264c82..787c9b788 100644
--- a/src/api/dotnet/Global.cs
+++ b/src/api/dotnet/Global.cs
@@ -43,7 +43,7 @@ namespace Microsoft.Z3
         /// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
         /// Thus, the following parameter names are considered equivalent: "pp.decimal-precision"  and "PP.DECIMAL_PRECISION".
         /// This function can be used to set parameters for a specific Z3 module.
-        /// This can be done by using <module-name>.<parameter-name>.
+        /// This can be done by using [module-name].[parameter-name].
         /// For example:
         /// Z3_global_param_set('pp.decimal', 'true')
         /// will set the parameter "decimal" in the module "pp" to true.
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 555a2466f..9de515e86 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -132,7 +132,8 @@ namespace Microsoft.Z3
         /// <remarks>
         /// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
         /// Both APIs can be used in the same solver. The unsat core will contain a combination
-        /// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
+        /// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/> 
+        /// and the Boolean literals
         /// provided using <see cref="Check"/> with assumptions.
         /// </remarks>        
         public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
@@ -156,7 +157,8 @@ namespace Microsoft.Z3
         /// <remarks>
         /// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
         /// Both APIs can be used in the same solver. The unsat core will contain a combination
-        /// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
+        /// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/> 
+        /// and the Boolean literals
         /// provided using <see cref="Check"/> with assumptions.
         /// </remarks>        
         public void AssertAndTrack(BoolExpr constraint, BoolExpr p)