diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index e8017e020..f30e67673 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The abstract syntax tree (AST) class.
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index 1672dc14c..720e90a4c 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 public class ASTDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index 51d4e02bb..a2d334b0e 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Map from AST to AST
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 7451e93b3..b93c9f4bd 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Vectors of ASTs.
diff --git a/src/api/java/AlgebraicNum.java b/src/api/java/AlgebraicNum.java
index 2ed2d8315..9aee64e65 100644
--- a/src/api/java/AlgebraicNum.java
+++ b/src/api/java/AlgebraicNum.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter) 
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Algebraic numbers
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index afcc3f0f7..feb8dc5ea 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * ApplyResult objects represent the result of an application of a tactic to a
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index 98d727522..96d18bef1 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ApplyResultDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java
index c15cf212e..c429f2322 100644
--- a/src/api/java/ArithExpr.java
+++ b/src/api/java/ArithExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  * **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Arithmetic expressions (int/real)
diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java
index bcaf5a88f..5e1780539 100644
--- a/src/api/java/ArithSort.java
+++ b/src/api/java/ArithSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * An arithmetic sort, i.e., Int or Real.
diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java
index 7082bc64b..b3bbb8d75 100644
--- a/src/api/java/ArrayExpr.java
+++ b/src/api/java/ArrayExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 
 /**
diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java
index 2b7979468..cd126443c 100644
--- a/src/api/java/ArraySort.java
+++ b/src/api/java/ArraySort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter) 
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Array sorts.
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
index a6232866f..23cb3c6fd 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ASTMapDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index 013cc5351..4496c092e 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ASTVectorDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java
index cd64cfc82..fb0f4d72a 100644
--- a/src/api/java/BitVecExpr.java
+++ b/src/api/java/BitVecExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Bit-vector expressions
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index b1f12fae5..10dad6423 100644
--- a/src/api/java/BitVecNum.java
+++ b/src/api/java/BitVecNum.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 
diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java
index 8ce31e7bb..e8cd0af27 100644
--- a/src/api/java/BitVecSort.java
+++ b/src/api/java/BitVecSort.java
@@ -3,7 +3,7 @@
  * w/ further modifications by:
  * @author Christoph M. Wintersteiger (cwinter)
  **/
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Bit-vector sorts.
diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java
index ddabc81d9..40786f76d 100644
--- a/src/api/java/BoolExpr.java
+++ b/src/api/java/BoolExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Boolean expressions
diff --git a/src/api/java/BoolSort.java b/src/api/java/BoolSort.java
index 501467bfc..03711289a 100644
--- a/src/api/java/BoolSort.java
+++ b/src/api/java/BoolSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A Boolean sort.
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index 146c7daa0..3ddb8664b 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Constructors are used for datatype sorts.
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index a158240eb..857ec3cf0 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Lists of constructors
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index f728f1b25..ef82eba35 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -4,10 +4,10 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.util.*;
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The main interaction with Z3 happens via the Context.
diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java
index c29507163..63cb02f80 100644
--- a/src/api/java/DatatypeExpr.java
+++ b/src/api/java/DatatypeExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Datatype expressions
diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java
index 30e9f9d4c..1ff123706 100644
--- a/src/api/java/DatatypeSort.java
+++ b/src/api/java/DatatypeSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Datatype sorts.
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index 0c4468b9c..8c9eeb16a 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Enumeration sorts.
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 8442acf6a..4bc7f6842 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /* using System; */
 
diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java
index f9f3820af..0183bec60 100644
--- a/src/api/java/FiniteDomainSort.java
+++ b/src/api/java/FiniteDomainSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Finite domain sorts.
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 3ad42c0e9..860629eec 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Object for managing fixedpoints
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index 7ed457bed..3d436eafb 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FixedpointDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 79fc457f8..d64ce3cf9 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Function declarations.
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index 8c25508e7..25d3fe1c8 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A function interpretation is represented as a finite map and an 'else' value.
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index 968a642c8..e41551b66 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FuncInterpDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index 8d76f597c..8d642217f 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FuncInterpEntryDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index f5d853fd5..d4b242a03 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A goal (aka problem). A goal is essentially a set of formulas, that can be
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index ac49d2484..9bd2b79db 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class GoalDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index 1d1ef2c04..e4eec7f4f 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.util.*;
 
diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java
index ffae8ee33..02bbb0ad5 100644
--- a/src/api/java/IDisposable.java
+++ b/src/api/java/IDisposable.java
@@ -17,7 +17,7 @@ Notes:
     
 --*/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 public class IDisposable
 {
diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java
index 4b9df2b99..78cc15f90 100644
--- a/src/api/java/IntExpr.java
+++ b/src/api/java/IntExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Int expressions
diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java
index 7db80c7d9..aecf68ee7 100644
--- a/src/api/java/IntNum.java
+++ b/src/api/java/IntNum.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 
diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java
index c07696216..44e48ccd1 100644
--- a/src/api/java/IntSort.java
+++ b/src/api/java/IntSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * An Integer sort
diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java
index ca5653b4b..3dbdfaf73 100644
--- a/src/api/java/IntSymbol.java
+++ b/src/api/java/IntSymbol.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Numbered symbols
diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java
index e00d185ac..98292b6ae 100644
--- a/src/api/java/ListSort.java
+++ b/src/api/java/ListSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * List sorts.
diff --git a/src/api/java/Log.java b/src/api/java/Log.java
index 388bc836f..bd85d021c 100644
--- a/src/api/java/Log.java
+++ b/src/api/java/Log.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Interaction logging for Z3. <remarks> Note that this is a global, static log
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index e15af9d0f..2616f26be 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A Model contains interpretations (assignments) of constants and functions.
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index 52c035914..89a0bbd78 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ModelDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index ba2ed6e94..11a8ee8b2 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A ParamDescrs describes a set of parameters.
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index 82d76c843..f36d302ba 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ParamDescrsDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index b1bfdd516..33ca34a23 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A ParameterSet represents a configuration in the form of Symbol/value pairs.
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index 88e40fb23..27fa3cadd 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ParamsDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index 017aead97..47f4a7c6a 100644
--- a/src/api/java/Pattern.java
+++ b/src/api/java/Pattern.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Patterns comprise a list of terms. The list should be non-empty. If the list
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index a0fcfd3db..80ac55b70 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Probes are used to inspect a goal (aka problem) and collect information that
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index 2c3cd9783..01d2e3852 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ProbeDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index 2b7eba0d9..a0b5c9e6a 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Quantifier expressions.
diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java
index 7a762b361..045416973 100644
--- a/src/api/java/RatNum.java
+++ b/src/api/java/RatNum.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 /**
diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java
index 9f2590fe1..20d603d9a 100644
--- a/src/api/java/RealExpr.java
+++ b/src/api/java/RealExpr.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Real expressions
diff --git a/src/api/java/RealSort.java b/src/api/java/RealSort.java
index 0b7f600b2..ce7295ead 100644
--- a/src/api/java/RealSort.java
+++ b/src/api/java/RealSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A real sort
diff --git a/src/api/java/RelationSort.java b/src/api/java/RelationSort.java
index 1d0371fd1..2880eadc9 100644
--- a/src/api/java/RelationSort.java
+++ b/src/api/java/RelationSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Relation sorts.
diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java
index c211a597d..ffeebfd3d 100644
--- a/src/api/java/SetSort.java
+++ b/src/api/java/SetSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Set sorts.
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 613479053..703f22be4 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Solvers.
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index 337c41898..11a670732 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class SolverDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 5cb76e17a..9a6f8aa9a 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The Sort class implements type information for ASTs.
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 81a75fd48..07a573940 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Objects of this class track statistical information about solvers.
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index 4337d366d..0bbd7914a 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/src/api/java/StatisticsDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class StatisticsDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/Status.java b/src/api/java/Status.java
index 4f2d44e9d..117618426 100644
--- a/src/api/java/Status.java
+++ b/src/api/java/Status.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Status values.
diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java
index 34e38c3c9..81ada78a4 100644
--- a/src/api/java/StringSymbol.java
+++ b/src/api/java/StringSymbol.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Named symbols
diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java
index 1576e17e1..526960e88 100644
--- a/src/api/java/Symbol.java
+++ b/src/api/java/Symbol.java
@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Symbols are used to name several term and type constructors.
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index 78c19a298..90e728087 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Tactics are the basic building block for creating custom solvers for specific
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 1b3bd5a03..ff0e27b5c 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/src/api/java/TacticDecRefQueue.java
@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class TacticDecRefQueue extends IDecRefQueue
 {
diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java
index d72d0b128..f05885f35 100644
--- a/src/api/java/TupleSort.java
+++ b/src/api/java/TupleSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Tuple sorts.
diff --git a/src/api/java/UninterpretedSort.java b/src/api/java/UninterpretedSort.java
index 4967b73f7..bc062cb50 100644
--- a/src/api/java/UninterpretedSort.java
+++ b/src/api/java/UninterpretedSort.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Uninterpreted Sorts
diff --git a/src/api/java/Version.java b/src/api/java/Version.java
index 7b20a5ff8..51fad896c 100644
--- a/src/api/java/Version.java
+++ b/src/api/java/Version.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Version information. <remarks>Note that this class is static.</remarks>
diff --git a/src/api/java/Z3Exception.java b/src/api/java/Z3Exception.java
index 6de94a5cf..ae7046c90 100644
--- a/src/api/java/Z3Exception.java
+++ b/src/api/java/Z3Exception.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.lang.Exception;
 
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 522423e01..e5e4af3c2 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Internal base class for interfacing with native Z3 objects. Should not be
diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py
index 1c59fc957..87f3e274a 100644
--- a/src/api/java/mk_java.py
+++ b/src/api/java/mk_java.py
@@ -1,11 +1,18 @@
-############################################
+######################################################
 # Copyright (c) 2012 Microsoft Corporation
 # 
 # Auxiliary scripts for generating Java bindings
 # from the managed API.
 #
 # Author: Christoph M. Wintersteiger (cwinter)
-############################################
+######################################################
+
+
+###
+# DO NOT USE THIS SCRIPT! 
+# This script creates a rough draft of a Java API from
+# the managed API, but does not automated the process.
+###
 
 CS="../dotnet/"
 EXT=".cs"