diff --git a/scripts/update_api.py b/scripts/update_api.py
index bb5935a1e..6e7b6d5f7 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -99,7 +99,7 @@ else:
      if s != None:
         enc = sys.stdout.encoding
         if enc != None: return s.decode(enc)
-        else: return s
+        else: return s.decode('ascii')
      else:
         return ""
 
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 25c399d68..d56ba4af1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2613,8 +2613,13 @@ namespace Microsoft.Z3
         /// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
         /// with the sorts of the bound variables, <paramref name="names"/> is an array with the
         /// 'names' of the bound variables, and <paramref name="body"/> is the body of the
-        /// quantifier. Quantifiers are associated with weights indicating
-        /// the importance of using the quantifier during instantiation.
+        /// quantifier. Quantifiers are associated with weights indicating the importance of 
+        /// using the quantifier during instantiation.
+        /// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>. 
+        /// Z3 applies the convention that the last element in <paramref name="names"/> and 
+        /// <paramref name="sorts"/> refers to the variable with index 0, the second to last element 
+        /// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable 
+        /// with index 1, etc. 
         /// </remarks>
         /// <param name="sorts">the sorts of the bound variables.</param>
         /// <param name="names">names of the bound variables</param>
@@ -2644,6 +2649,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a universal Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates a universal quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2659,7 +2669,10 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
-        /// <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
+        /// <remarks>
+        /// Creates an existential quantifier using de-Brujin indexed variables. 
+        /// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
+        /// </remarks>
         public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(sorts != null);
@@ -2678,6 +2691,11 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an existential Quantifier.
         /// </summary>
+        /// <remarks>
+        /// Creates an existential quantifier using a list of constants that will 
+        /// form the set of bound variables. 
+        /// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
+        /// </remarks>
         public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2693,6 +2711,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
@@ -2716,6 +2735,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create a Quantifier.
         /// </summary>
+        /// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
         public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
         {
             Contract.Requires(body != null);
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 0f9a85799..4d8484ced 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -433,8 +433,8 @@ public class Context extends IDisposable
     /**
      * Creates a fresh function declaration with a name prefixed with
      * {@code prefix}. 
-     * @see mkFuncDecl(String,Sort,Sort)
-     * @see mkFuncDecl(String,Sort[],Sort)
+     * @see #mkFuncDecl(String,Sort,Sort)
+     * @see #mkFuncDecl(String,Sort[],Sort)
      **/
     public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
            
@@ -1722,9 +1722,9 @@ public class Context extends IDisposable
      **/
     public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
     {
-	checkContextMatch(arg1);
-	checkContextMatch(arg2);
-	return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
+    checkContextMatch(arg1);
+    checkContextMatch(arg2);
+    return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
     }
 
 
@@ -2025,6 +2025,7 @@ public class Context extends IDisposable
 
     /**
      * Create a universal Quantifier.
+     *
      * @param sorts the sorts of the bound variables. 
      * @param names names of the bound variables 
      * @param body the body of the quantifier. 
@@ -2034,17 +2035,22 @@ public class Context extends IDisposable
      * @param quantifierID optional symbol to track quantifier. 
      * @param skolemID optional symbol to track skolem constants.
      * 
-     * Remarks:  Creates a forall formula, where
-     * {@code weight"/> is the weight, <paramref name="patterns} is
+     * @return Creates a forall formula, where
+     * {@code weight} is the weight, {@code patterns} is
      * an array of patterns, {@code sorts} is an array with the sorts
      * of the bound variables, {@code names} is an array with the
      * 'names' of the bound variables, and {@code body} is the body
      * of the quantifier. Quantifiers are associated with weights indicating the
      * importance of using the quantifier during instantiation.
+     * Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
+     * Z3 applies the convention that the last element in {@code names} and 
+     * {@code sorts} refers to the variable with index 0, the second to last element 
+     * of {@code names} and {@code sorts} refers to the variable 
+     * with index 1, etc. 
      **/
     public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
-            int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                               int weight, Pattern[] patterns, Expr[] noPatterns,
+                               Symbol quantifierID, Symbol skolemID)
     {
 
         return new Quantifier(this, true, sorts, names, body, weight, patterns,
@@ -2052,11 +2058,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a universal Quantifier.
+     * Creates a universal quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
-            Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
-            Symbol skolemID)
+                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+                               Symbol skolemID)
     {
 
         return new Quantifier(this, true, boundConstants, body, weight,
@@ -2064,12 +2071,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier. 
+     * Creates an existential quantifier using de-Brujin indexed variables. 
      * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
-            int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                               int weight, Pattern[] patterns, Expr[] noPatterns,
+                               Symbol quantifierID, Symbol skolemID)
     {
 
         return new Quantifier(this, false, sorts, names, body, weight,
@@ -2077,11 +2084,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create an existential Quantifier.
+     * Creates an existential quantifier using a list of constants that will form the set of bound variables. 
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
-            Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
-            Symbol skolemID)
+                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+                               Symbol skolemID)
     {
 
         return new Quantifier(this, false, boundConstants, body, weight,
@@ -2090,11 +2098,12 @@ public class Context extends IDisposable
 
     /**
      * Create a Quantifier.
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
-            Symbol[] names, Expr body, int weight, Pattern[] patterns,
-            Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
-           
+                                   Symbol[] names, Expr body, int weight, Pattern[] patterns,
+                                   Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+        
     {
 
         if (universal)
@@ -2106,11 +2115,12 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a Quantifier.
+     * Create a Quantifier
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
-            Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID)
+                                   Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
+                                   Symbol quantifierID, Symbol skolemID)
     {
 
         if (universal)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 214d8b687..444c025e6 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -4862,7 +4862,7 @@ class Goal(Z3PPObject):
         elif sz == 1:
             return self.get(0)
         else:
-            return And([ self.get(i) for i in range(len(self)) ])
+            return And([ self.get(i) for i in range(len(self)) ], self.ctx)
 
 #########################################
 #
diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index 5116046dd..2a242865e 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3printer.py
@@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
 def obj_to_string(a):
     out = io.StringIO()
     _PP(out, _Formatter(a))
-    return out.getvalue()
+    r = out.getvalue()
+    if sys.version < '3':
+        return r
+    else:
+        enc = sys.stdout.encoding
+        if enc != None: return r.decode(enc)
+        return r
 
 _html_out = None