diff --git a/scripts/update_api.py b/scripts/update_api.py
index 0e2219f31..1cccd5d98 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -263,8 +263,10 @@ def param2dotnet(p):
         return "[In] %s[]" % type2dotnet(param_type(p))
     elif k == INOUT_ARRAY:
         return "[In, Out] %s[]" % type2dotnet(param_type(p))
-    elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY:
-        return "[Out] out %s[]" % type2dotnet(param_type(p))
+    elif k == OUT_ARRAY:
+        return "[Out] %s[]" % type2dotnet(param_type(p))
+    elif k == OUT_MANAGED_ARRAY:
+	return "[Out] out %s[]" % type2dotnet(param_type(p))
     else:
         return type2dotnet(param_type(p))
 
@@ -476,7 +478,7 @@ def mk_dotnet_wrappers():
                     dotnet.write('out ');
                 else:
                     dotnet.write('ref ')
-            elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY:
+            elif param_kind(param) == OUT_MANAGED_ARRAY:
                 dotnet.write('out ');
             dotnet.write('a%d' % i)
             i = i + 1
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 3875c0c9f..5b385a872 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -100,10 +100,4 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) {
-        LOG_Z3_get_param_value(c, param_id, param_value);
-        // TODO
-        return Z3_FALSE;
-    }
-
 };
diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs
index 8d478dd85..527b8bc13 100644
--- a/src/api/dotnet/Constructor.cs
+++ b/src/api/dotnet/Constructor.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                 return new FuncDecl(Context, constructor);                
             }
         }
@@ -66,7 +66,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                 return new FuncDecl(Context, tester);                
             }
         }
@@ -82,7 +82,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);                
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);                
                 FuncDecl[] t = new FuncDecl[n];
                 for (uint i = 0; i < n; i++)
                     t[i] = new FuncDecl(Context, accessors[i]); 
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 85280975f..989d1d7d7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -424,7 +424,7 @@ namespace Microsoft.Z3
                 n_constr[i] = cla[i].NativeObject;
             }
             IntPtr[] n_res = new IntPtr[n];
-            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr);
+            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
             DatatypeSort[] res = new DatatypeSort[n];
             for (uint i = 0; i < n; i++)
                 res[i] = new DatatypeSort(this, n_res[i]);
@@ -3569,28 +3569,11 @@ namespace Microsoft.Z3
         /// Only a few configuration parameters are mutable once the context is created.
         /// An exception is thrown when trying to modify an immutable parameter.
         /// </remarks>
-        /// <seealso cref="GetParamValue"/>
         public void UpdateParamValue(string id, string value)
         {
             Native.Z3_update_param_value(nCtx, id, value);
         }
 
-        /// <summary>
-        /// Get a configuration parameter.
-        /// </summary>
-        /// <remarks>
-        /// Returns null if the parameter value does not exist.
-        /// </remarks>
-        /// <seealso cref="UpdateParamValue"/>
-        public string GetParamValue(string id)
-        {
-            IntPtr res = IntPtr.Zero;
-            if (Native.Z3_get_param_value(nCtx, id, out res) == 0)
-                return null;
-            else
-                return Marshal.PtrToStringAnsi(res);
-        }
-
         #endregion
 
         #region Internal
diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs
index 995eeb2bc..aa6dffb45 100644
--- a/src/api/dotnet/Deprecated.cs
+++ b/src/api/dotnet/Deprecated.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Z3
                 IntPtr[] native_core = new IntPtr[assumptions.Length];
                 r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx, 
                                    (uint)assumptions.Length, AST.ArrayToNative(assumptions),
-                                   ref mdl, ref prf, ref core_size, out native_core);
+                                   ref mdl, ref prf, ref core_size, native_core);
 
                 for (uint i = 0; i < core_size; i++)
                     core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs
index db3d5123f..e62043078 100644
--- a/src/api/dotnet/EnumSort.cs
+++ b/src/api/dotnet/EnumSort.cs
@@ -88,7 +88,7 @@ namespace Microsoft.Z3
             IntPtr[] n_constdecls = new IntPtr[n];
             IntPtr[] n_testers = new IntPtr[n];
             NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
-                                                         Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers);
+                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
         }
         #endregion
     };
diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs
index 7d0b6a853..81a0eaf60 100644
--- a/src/api/dotnet/TupleSort.cs
+++ b/src/api/dotnet/TupleSort.cs
@@ -74,10 +74,10 @@ namespace Microsoft.Z3
             Contract.Requires(name != null);
 
             IntPtr t = IntPtr.Zero;
-            IntPtr[] f;
+            IntPtr[] f = new IntPtr[numFields];
             NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
                                                    Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
-                                                   ref t, out f);
+                                                   ref t, f);
         }
         #endregion
     };
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index fa5cd8284..1f5463ec7 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from AST.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    AST.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index e0711363d..6ae84eb41 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ASTDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index dbe7fbd02..6a4e6d56f 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ASTMap.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ASTMap.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 39e32f5d5..07b7dbf56 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ASTVector.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ASTVector.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java
index eaeae933d..340f37f80 100644
--- a/src/api/java/AlgebraicNum.java
+++ b/src/api/java/AlgebraicNum.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from AlgebraicNum.cs
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter) 
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    AlgebraicNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index e6c6b89fd..c550c05ae 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ApplyResult.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ApplyResult.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index 275f4b8f0..78f74d6cc 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ApplyResultDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java
index c429f2322..83ec35d01 100644
--- a/src/api/java/ArithExpr.java
+++ b/src/api/java/ArithExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArithExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- * **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ArithExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java
index 5e1780539..2346d9b74 100644
--- a/src/api/java/ArithSort.java
+++ b/src/api/java/ArithSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArithSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ArithSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java
index b3bbb8d75..2d5a5a273 100644
--- a/src/api/java/ArrayExpr.java
+++ b/src/api/java/ArrayExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArrayExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ArrayExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java
index 2ab8a9750..a371fa3cb 100644
--- a/src/api/java/ArraySort.java
+++ b/src/api/java/ArraySort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArraySort.cs
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter) 
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ArraySort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
index f4c6b2ab5..a4e02d29f 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    AstMapDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index bdabcdcb1..e0c7988a9 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    AstVectorDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java
index 9602ea3a0..24b1cfdf3 100644
--- a/src/api/java/BitVecExpr.java
+++ b/src/api/java/BitVecExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BitVecExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    BitVecExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index 2dd0dd75a..69ac5dadc 100644
--- a/src/api/java/BitVecNum.java
+++ b/src/api/java/BitVecNum.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BitVecNum.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    BitVecNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java
index c2ec4c26e..be406c806 100644
--- a/src/api/java/BitVecSort.java
+++ b/src/api/java/BitVecSort.java
@@ -1,8 +1,20 @@
 /**
- * This file was automatically generated from BitVecSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    BitVecSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
+
 package com.microsoft.z3;
 
 /**
diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java
index 40786f76d..99453496a 100644
--- a/src/api/java/BoolExpr.java
+++ b/src/api/java/BoolExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BoolExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    BoolExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/BoolSort.java b/src/api/java/BoolSort.java
index 03711289a..85ca0a7f7 100644
--- a/src/api/java/BoolSort.java
+++ b/src/api/java/BoolSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BoolSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    BoolSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index 0c53da73c..4813c2b0a 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Constructor.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Constructor.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index a33276ebb..315a2e535 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ConstructorList.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ConstructorList.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 6b6c63ac3..4fbd79be2 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Context.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Context.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
@@ -2904,27 +2915,13 @@ public class Context extends IDisposable
      * configuration parameters can be obtained using the Z3 executable:
      * <code>z3.exe -ini?</code> Only a few configuration parameters are mutable
      * once the context is created. An exception is thrown when trying to modify
-     * an immutable parameter. </remarks> <seealso cref="GetParamValue"/>
+     * an immutable parameter. </remarks> 
      **/
     public void updateParamValue(String id, String value) throws Z3Exception
     {
         Native.updateParamValue(nCtx(), id, value);
     }
 
-    /**
-     * Get a configuration parameter. <remarks> Returns null if the parameter
-     * value does not exist. </remarks> <seealso cref="UpdateParamValue"/>
-     **/
-    public String getParamValue(String id) throws Z3Exception
-    {
-        Native.StringPtr res = new Native.StringPtr();
-        boolean r = Native.getParamValue(nCtx(), id, res);
-        if (!r)
-            return null;
-        else
-            return res.value;
-    }
-
     long m_ctx = 0;
 
     long nCtx()
diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java
index 63cb02f80..806ceacab 100644
--- a/src/api/java/DatatypeExpr.java
+++ b/src/api/java/DatatypeExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from DatatypeExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    DatatypeExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java
index f7b2f7d32..9c339d932 100644
--- a/src/api/java/DatatypeSort.java
+++ b/src/api/java/DatatypeSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from DatatypeSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    DatatypeSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index c0fb6d1d6..9715b9a97 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from EnumSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    EnumSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index f7edc6a2b..3773e749d 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Expr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Expr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java
index a8ba0d8c3..4cb2ab917 100644
--- a/src/api/java/FiniteDomainSort.java
+++ b/src/api/java/FiniteDomainSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FiniteDomainSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FiniteDomainSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index ee570da41..f7d2bc7b7 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Fixedpoint.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Fixedpoint.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index e52389b85..2ea40dd2c 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FixedpointDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index ada44bbd7..573ebd102 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FuncDecl.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FuncDecl.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index b7fa118e9..243ade71f 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FuncInterp.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FuncInterp.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index e2814a9b8..8bdad4ad5 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FuncInterpDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index 61488ec74..494c2695c 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    FuncInterpEntryDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Global.java b/src/api/java/Global.java
index 33a828fb8..b97e48721 100644
--- a/src/api/java/Global.java
+++ b/src/api/java/Global.java
@@ -1,7 +1,19 @@
 /**
- * Global.java
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Global.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index c486a57b3..aba8b0149 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Goal.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Goal.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index 0c7b8f5d9..45992170f 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    GoalDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index ddb679910..2190f8e4d 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IDecRefQueue.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java
index 78cc15f90..2e90c3cbf 100644
--- a/src/api/java/IntExpr.java
+++ b/src/api/java/IntExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IntExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java
index ebf237a2e..0fdcf1aa6 100644
--- a/src/api/java/IntNum.java
+++ b/src/api/java/IntNum.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntNum.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IntNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java
index 44e48ccd1..bcfc730c4 100644
--- a/src/api/java/IntSort.java
+++ b/src/api/java/IntSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IntSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java
index 113b507c3..b0f1af685 100644
--- a/src/api/java/IntSymbol.java
+++ b/src/api/java/IntSymbol.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntSymbol.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    IntSymbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 067871324..3e9996b3e 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -1,6 +1,20 @@
 /**
- * 
- */
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+   InterpolationContext.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
 package com.microsoft.z3;
 
 import java.util.Map;
diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java
index af1645187..52cb1a179 100644
--- a/src/api/java/ListSort.java
+++ b/src/api/java/ListSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ListSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ListSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Log.java b/src/api/java/Log.java
index 99581cedb..254da1bc6 100644
--- a/src/api/java/Log.java
+++ b/src/api/java/Log.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Log.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Log.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 32247eb4a..11eed201e 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Model.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Model.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index a0542714e..1200b29be 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ModelDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 3b3e76e51..4afae9f76 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ParamDescrs.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ParamDescrs.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index 70806041d..a29565e8e 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ParamDescrsDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index cf3d8c759..bbe6d66cf 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -1,8 +1,20 @@
 /**
- * This file was automatically generated from Params.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Params.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index 361fdf133..7d71feb8f 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ParamDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index cd9340c9d..797b387d0 100644
--- a/src/api/java/Pattern.java
+++ b/src/api/java/Pattern.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Pattern.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Pattern.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index b68b0266f..17ad81b5c 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Probe.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Probe.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index 0ae0b0e8e..fda5d37b4 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    ProbeDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index 78a0fc03f..e9aeefcca 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Quantifier.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Quantifier.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java
index e1cb5b346..f937ea593 100644
--- a/src/api/java/RatNum.java
+++ b/src/api/java/RatNum.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RatNum.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    RatNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java
index 20d603d9a..6188e2999 100644
--- a/src/api/java/RealExpr.java
+++ b/src/api/java/RealExpr.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RealExpr.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    RealExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/RealSort.java b/src/api/java/RealSort.java
index ce7295ead..d76823a0d 100644
--- a/src/api/java/RealSort.java
+++ b/src/api/java/RealSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RealSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    RealSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java
index bdc4d7804..77f6c595b 100644
--- a/src/api/java/RelationSort.java
+++ b/src/api/java/RelationSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RelationSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    RelationSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java
index a94a34b26..69126933a 100644
--- a/src/api/java/SetSort.java
+++ b/src/api/java/SetSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from SetSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    SetSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 3827de07a..e129189f9 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Solver.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Solver.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index 1c715716a..993c99621 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    SolverDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 381b9b0ae..7bcc7ce7e 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Sort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Sort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index c36020bd6..315feeaa2 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Statistics.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Statistics.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index d16bf3710..db3e32c86 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/src/api/java/StatisticsDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    StatisticsDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Status.java b/src/api/java/Status.java
index e37631070..a08f47909 100644
--- a/src/api/java/Status.java
+++ b/src/api/java/Status.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Status.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Status.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java
index 951051aa0..09273c946 100644
--- a/src/api/java/StringSymbol.java
+++ b/src/api/java/StringSymbol.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from StringSymbol.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    StringSymbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java
index 177409ec8..856c9b57e 100644
--- a/src/api/java/Symbol.java
+++ b/src/api/java/Symbol.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Symbol.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Symbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index e62096715..6573a1407 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Tactic.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Tactic.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 50fba156e..5557d03b8 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/src/api/java/TacticDecRefQueue.java
@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    TacticDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java
index 554581d0f..523f8d676 100644
--- a/src/api/java/TupleSort.java
+++ b/src/api/java/TupleSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from TupleSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    TupleSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/UninterpretedSort.java b/src/api/java/UninterpretedSort.java
index 51df17543..07e4707f5 100644
--- a/src/api/java/UninterpretedSort.java
+++ b/src/api/java/UninterpretedSort.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from UninterpretedSort.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    UninterpretedSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Version.java b/src/api/java/Version.java
index b96fb50f9..3f019390b 100644
--- a/src/api/java/Version.java
+++ b/src/api/java/Version.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Version.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Version.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Z3Exception.java b/src/api/java/Z3Exception.java
index 24dc586d4..2522db627 100644
--- a/src/api/java/Z3Exception.java
+++ b/src/api/java/Z3Exception.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Z3Exception.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Z3Exception.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 6c2c11e25..03cfcd625 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Z3Object.cs 
- * w/ further modifications by:
- * @author Christoph M. Wintersteiger (cwinter)
- **/
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    Z3Object.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index 22da27e03..e01b78238 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -4,7 +4,7 @@ class Z3Exception(Exception):
     def __init__(self, value):
         self.value = value
     def __str__(self):
-        return repr(self.value)
+        return str(self.value)
 
 class ContextObj(ctypes.c_void_p):
   def __init__(self, context): self._as_parameter_ = context
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b493a6f1c..258c7de9a 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1479,15 +1479,6 @@ extern "C" {
     */
     void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
 
-    /**
-       \brief Return the value of a context parameter.
-      
-       \sa Z3_global_param_get
-
-       def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
-    */
-    Z3_bool_opt Z3_API Z3_get_param_value(__in Z3_context c, __in Z3_string param_id, __out_opt Z3_string_ptr param_value);
-
 #ifdef CorML4
     /**
        \brief Interrupt the execution of a Z3 procedure.
diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index df26422c8..5466df069 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -314,8 +314,8 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete
     symbol name;
     switch (k) {
     case OP_FLOAT_REM: name = "remainder";  break;
-    case OP_FLOAT_MIN: name = "min";   break;
-    case OP_FLOAT_MAX: name = "max";   break;
+    case OP_FLOAT_MIN: name = "fp.min";   break;
+    case OP_FLOAT_MAX: name = "fp.max";   break;
     default:
         UNREACHABLE();
         break;
@@ -581,8 +581,9 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
     op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
 
-    op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
-    op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
+    // Disabled min/max, clashes with user-defined min/max functions
+    // op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
+    // op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
 
     op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
 
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index d1184fbc8..71b251610 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -92,7 +92,7 @@ void context_params::set(char const * param, char const * value) {
         strm << "unknown parameter '" << p << "'\n";
         strm << "Legal parameters are:\n";
         d.display(strm, 2, false, false);
-        throw default_exception(strm.str());
+        throw default_exception(strm.str());        
     }
 }
 
diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp
index 41a61bf73..9a6868ff1 100644
--- a/src/smt/arith_eq_solver.cpp
+++ b/src/smt/arith_eq_solver.cpp
@@ -604,7 +604,9 @@ bool arith_eq_solver::solve_integer_equations_gcd(
                 }
                 SASSERT(g == r0[i]);
             }
-            SASSERT(abs(r0[i]).is_one());
+            if (!abs(r0[i]).is_one()) {
+                return false;
+            }
             live.erase(live.begin()+live_pos);
             for (j = 0; j < live.size(); ++j) {
                 row& r = rows[live[j]];
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d3dc8a492..8e91029a3 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -71,7 +71,7 @@ namespace smt {
 
     protected:
         ast_manager &               m_manager;
-        smt_params &          m_fparams;
+        smt_params &                m_fparams;
         params_ref                  m_params;
         setup                       m_setup;
         volatile bool               m_cancel_flag;
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index e9b0e069a..b76fb6c74 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -453,9 +453,9 @@ namespace smt {
 	 instantiated.
        */
         virtual void add(quantifier * q) {
-	  if (m_fparams->m_mbqi && mbqi_enabled(q)) {
-	    m_model_finder->register_quantifier(q);
-	  }
+            if (m_fparams->m_mbqi && mbqi_enabled(q)) {
+                m_model_finder->register_quantifier(q);
+            }
         }
 
         virtual void del(quantifier * q) {
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 197f65c10..69f596c5d 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -230,6 +230,42 @@ public:
         }
     }
 
+    void validate_type(symbol const& name, char const* value, param_descrs const& d) {
+        param_kind k = d.get_kind(name);
+        std::stringstream strm;
+        char const* _value = value;
+        switch (k) {
+        case CPK_UINT:
+            for (; *value; ++value) {
+                if (!('0' <= *value && *value <= '9')) {
+                    strm << "Expected values for parameter " << name 
+                         << " is an unsigned integer. It was given argument '" << _value << "'";
+                    throw default_exception(strm.str());                    
+                }
+            }
+            break;
+        case CPK_DOUBLE:
+            for (; *value; ++value) {
+                if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') {
+                    strm << "Expected values for parameter " << name 
+                         << " is a double. It was given argument '" << _value << "'";
+                    throw default_exception(strm.str());                                        
+                }
+            }
+            break;
+
+        case CPK_BOOL:
+            if (strcmp(value, "true") != 0 && strcmp(value, "false") != 0) {
+                strm << "Expected values for parameter " << name 
+                     << " are 'true' or 'false'. It was given argument '" << value << "'";
+                throw default_exception(strm.str());
+            }
+            break;
+        default:
+            break;
+        }
+    }
+
 
     void set(param_descrs const & d, symbol const & param_name, char const * value, symbol const & mod_name) {
         param_kind k = d.get_kind(param_name);
@@ -292,11 +328,13 @@ public:
                 symbol m, p;
                 normalize(name, m, p);
                 if (m == symbol::null) {
+                    validate_type(p, value, get_param_descrs());
                     set(get_param_descrs(), p, value, m);
                 }
                 else {
                     param_descrs * d;
                     if (get_module_param_descrs().find(m, d)) {
+                        validate_type(p, value, *d);
                         set(*d, p, value, m);
                     }
                     else {