diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index ae10d6740..2ff414f78 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -493,6 +493,9 @@ def get_c_files(path):
 def get_cs_files(path):
     return filter(lambda f: f.endswith('.cs'), os.listdir(path))
 
+def get_java_files(path):
+    return filter(lambda f: f.endswith('.java'), os.listdir(path))
+
 def find_all_deps(name, deps):
     new_deps = []
     for dep in deps:
@@ -932,19 +935,21 @@ class JavaDLLComponent(Component):
     def mk_makefile(self, out):
         if is_java_enabled():
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('%s: %s/Z3Native.java %s$(SO_EXT)\n' % (dllfile, self.to_src_dir, get_component('api_dll').dll_name))
-            if IS_WINDOWS:
-                out.write('\tcd %s && %s Z3Native.java\n' % (unix_path2dos(self.to_src_dir), JAVAC))
-                out.write('\tmove %s\\*.class .\n' % unix_path2dos(self.to_src_dir))
-                out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Z3Native.c\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
-                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) Z3Native$(OBJ_EXT) libz3.lib\n' % dllfile)
-            else:
-                out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC))
-                out.write('\tmv %s/*.class .\n' % self.to_src_dir)
-                out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
-                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile)
-            out.write('%s: %s\n\n' % (self.name, dllfile))
-            # TODO: Compile and package all the .class files.
+            subdir = self.package_name.replace(".","/")
+            out.write('libz3java$(SO_EXT): libz3$(SO_EXT) ../src/api/java/Native.cpp\n')
+            out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Native.cpp\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir))
+            out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) Native$(OBJ_EXT) libz3.lib\n')
+            out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
+            # for java_file in get_java_files(self.src_dir):
+            #     out.write('%s ' % java_file)
+            # for java_file in get_java_files((self.src_dir + "/%s/Enumerations") % subdir):
+            #     out.write('%s ' % java_file)
+            out.write('\n')
+            src_wsub = self.to_src_dir + "/" + subdir;
+            out.write(('\tjavac %s/Enumerations/*.java -d api/java\n' % (src_wsub)).replace("/","\\"))
+            out.write(('\tjavac -cp api/java %s/*.java -d api/java\n' % (src_wsub)).replace("/","\\"))
+            out.write('\tjar cf %s.jar api/java/\n' % self.package_name)
+            out.write('java: %s.jar\n\n' % self.package_name)
     
     def main_component(self):
         return is_java_enabled()
@@ -1847,7 +1852,7 @@ def mk_z3consts_java(api_files):
                     if name not in DeprecatedEnums:
                         efile  = open('%s/%s.java' % (gendir, name), 'w')
                         efile.write('/**\n *  Automatically generated file\n **/\n\n')
-                        efile.write('package %s;\n\n' % java.package_name);
+                        efile.write('package %s.Enumerations;\n\n' % java.package_name);
 
                         efile.write('/**\n')
                         efile.write(' * %s\n' % name)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 1eef11705..10849aede 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -501,7 +501,7 @@ def mk_java():
     except:
         pass # OK if it exists already.
     java_nativef  = '%s/com/Microsoft/Z3/Native.java' % java_dir
-    java_wrapperf = '%s/com/Microsoft/Z3/Native.c' % java_dir 
+    java_wrapperf = '%s/Native.cpp' % java_dir 
     java_native   = open(java_nativef, 'w')
     java_native.write('// Automatically generated file\n')
     java_native.write('package com.Microsoft.Z3;\n')
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 37929e88f..15b6a59db 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -110,7 +110,7 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<Sort[]>() != null);
 
-                var n = DomainSize;
+                uint n = DomainSize;
 
                 Sort[] res = new Sort[n];
                 for (uint i = 0; i < n; i++)
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 6a0b253bb..e648ac80c 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -184,10 +184,10 @@ namespace Microsoft.Z3
         {
             Tactic t = Context.MkTactic("simplify");
             ApplyResult res = t.Apply(this, p);
-            
+
             if (res.NumSubgoals == 0)
-                return Context.MkGoal();
-            else        
+                throw new Z3Exception("No subgoals");
+            else
                 return res.Subgoals[0];
         }
 
diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
index 5529677dd..5c0bc24f8 100644
--- a/src/api/dotnet/Model.cs
+++ b/src/api/dotnet/Model.cs
@@ -165,8 +165,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
 
-                var nFuncs = NumFuncs;
-                var nConsts = NumConsts;
+                uint nFuncs = NumFuncs;
+                uint nConsts = NumConsts;
                 uint n = nFuncs + nConsts;
                 FuncDecl[] res = new FuncDecl[n];
                 for (uint i = 0; i < nConsts; i++)
diff --git a/src/api/java/com/Microsoft/Z3/Native.c b/src/api/java/Native.cpp
similarity index 100%
rename from src/api/java/com/Microsoft/Z3/Native.c
rename to src/api/java/Native.cpp
diff --git a/src/api/java/com/Microsoft/Z3/AST.java b/src/api/java/com/Microsoft/Z3/AST.java
index 069c07a4c..45e631694 100644
--- a/src/api/java/com/Microsoft/Z3/AST.java
+++ b/src/api/java/com/Microsoft/Z3/AST.java
@@ -87,7 +87,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <param name="ctx">A context</param>
          * @return A copy of the AST which is associated with <paramref name="ctx"/>
          **/
-        public AST Translate(Context ctx)
+        public AST Translate(Context ctx) throws Z3Exception
         {
             
             
@@ -157,7 +157,7 @@ import com.Microsoft.Z3.Enumerations.*;
         }
 
     AST(Context ctx) { super(ctx); {  }}
-    AST(Context ctx, long obj) { super(ctx, obj); {  }}
+    AST(Context ctx, long obj) throws Z3Exception { super(ctx, obj); {  }}
 
         class DecRefQueue extends IDecRefQueue
         {
@@ -172,7 +172,7 @@ import com.Microsoft.Z3.Enumerations.*;
             }
         };        
 
-        void IncRef(long o)
+        void IncRef(long o) throws Z3Exception
         {            
             // Console.WriteLine("AST IncRef()");
             if (Context() == null)
@@ -183,7 +183,7 @@ import com.Microsoft.Z3.Enumerations.*;
             super.IncRef(o);
         }
 
-        void DecRef(long o)
+        void DecRef(long o) throws Z3Exception
         {
             // Console.WriteLine("AST DecRef()");
             if (Context() == null)
@@ -194,7 +194,7 @@ import com.Microsoft.Z3.Enumerations.*;
             super.DecRef(o);
         }
 
-        static AST Create(Context ctx, long obj)
+        static AST Create(Context ctx, long obj) throws Z3Exception
         {
             
             
diff --git a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
index b9f5766ce..f98ccbce4 100644
--- a/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
+++ b/src/api/java/com/Microsoft/Z3/AlgebraicNum.java
@@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <param name="precision">the precision of the result</param>
          * @return A numeral Expr of sort Real
          **/
-        public RatNum ToUpper(int precision)
+        public RatNum ToUpper(int precision) throws Z3Exception
         {
             
 
@@ -38,7 +38,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <param name="precision"></param>
          * @return A numeral Expr of sort Real
          **/
-        public RatNum ToLower(int precision)
+        public RatNum ToLower(int precision) throws Z3Exception
         {
             
 
@@ -49,14 +49,14 @@ import com.Microsoft.Z3.Enumerations.*;
          * Returns a string representation in decimal notation.
          * <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
          **/
-        public String ToDecimal(int precision)
+        public String ToDecimal(int precision) throws Z3Exception
         {
             
 
             return Native.getNumeralDecimalString(Context().nCtx(), NativeObject(), precision);
         }
 
-        AlgebraicNum(Context ctx, long obj)
+        AlgebraicNum(Context ctx, long obj) throws Z3Exception
         { super(ctx, obj);
             
         }
diff --git a/src/api/java/com/Microsoft/Z3/ArithExpr.java b/src/api/java/com/Microsoft/Z3/ArithExpr.java
index 8df3bb0a5..fa87bf2f1 100644
--- a/src/api/java/com/Microsoft/Z3/ArithExpr.java
+++ b/src/api/java/com/Microsoft/Z3/ArithExpr.java
@@ -25,7 +25,7 @@ import com.Microsoft.Z3.Enumerations.*;
         { super(ctx);
             
         }
-        ArithExpr(Context ctx, long obj)
+        ArithExpr(Context ctx, long obj) throws Z3Exception
         { super(ctx, obj);
             
         }
diff --git a/src/api/java/com/Microsoft/Z3/BitVecExpr.java b/src/api/java/com/Microsoft/Z3/BitVecExpr.java
index bbb13a873..d7c43918e 100644
--- a/src/api/java/com/Microsoft/Z3/BitVecExpr.java
+++ b/src/api/java/com/Microsoft/Z3/BitVecExpr.java
@@ -23,7 +23,7 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * The size of the sort of a bit-vector term.
          **/
-        public int SortSize()  { return ((BitVecSort)Sort).Size; }
+        public int SortSize()  { return ((BitVecSort)Sort()).Size(); }
 
         /** Constructor for BitVecExpr </summary>
          **/
diff --git a/src/api/java/com/Microsoft/Z3/Constructor.java b/src/api/java/com/Microsoft/Z3/Constructor.java
index d7d534873..bcf5654a4 100644
--- a/src/api/java/com/Microsoft/Z3/Constructor.java
+++ b/src/api/java/com/Microsoft/Z3/Constructor.java
@@ -92,11 +92,11 @@ import com.Microsoft.Z3.Enumerations.*;
 
             if (sortRefs == null) sortRefs = new int[n];
 
-            NativeObject() = Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
-                                                    n,
-                                                    Symbol.ArrayToNative(fieldNames),
-                                                    Sort.ArrayToNative(sorts),
-                                                    sortRefs);
+            setNativeObject(Native.mkConstructor(ctx.nCtx(), name.NativeObject(), recognizer.NativeObject(),
+						 n,
+						 Symbol.ArrayToNative(fieldNames),
+						 Sort.ArrayToNative(sorts),
+						 sortRefs));
 
         }
 
diff --git a/src/api/java/com/Microsoft/Z3/Context.java b/src/api/java/com/Microsoft/Z3/Context.java
index 079bcaf43..8b83271a1 100644
--- a/src/api/java/com/Microsoft/Z3/Context.java
+++ b/src/api/java/com/Microsoft/Z3/Context.java
@@ -42,6 +42,12 @@ import com.Microsoft.Z3.Enumerations.*;
             InitContext();
         }
 
+        private Context(long ctx)
+        {
+	    super();
+	    this.m_ctx = ctx;
+	}
+
         /**
          * Creates a new symbol using an integer.
          * <remarks>
@@ -591,7 +597,7 @@ import com.Microsoft.Z3.Enumerations.*;
             
             
 
-            return MkApp(f);
+            return MkApp(f, null);
         }
 
         /**
@@ -2205,15 +2211,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return Expr.Create(this, Native.mkInt(nCtx(), v, ty.NativeObject()));
         }
 
-        /**
-         * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
-         * It is slightly faster than <code>MakeNumeral</code> since it is not necessary to parse a string.       
-         * <param name="v">Value of the numeral</param>
-         * <param name="ty">Sort of the numeral</param>
-         * @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
          * It is slightly faster than <code>MakeNumeral</code> since it is not necessary to parse a string.       
@@ -2230,15 +2227,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return Expr.Create(this, Native.mkInt64(nCtx(), v, ty.NativeObject()));
         }
 
-        /**
-         * Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
-         * It is slightly faster than <code>MakeNumeral</code> since it is not necessary to parse a string.       
-         * <param name="v">Value of the numeral</param>
-         * <param name="ty">Sort of the numeral</param>
-         * @return A Term with value <paramref name="v"/> and type <paramref name="ty"/>
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create a real from a fraction.
          * <param name="num">numerator of rational.</param>
@@ -2281,13 +2269,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return new RatNum(this, Native.mkInt(nCtx(), v, RealSort().NativeObject()));
         }
 
-        /**
-         * Create a real numeral.
-         * <param name="v">value of the numeral.</param>    
-         * @return A Term with value <paramref name="v"/> and sort Real
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create a real numeral.
          * <param name="v">value of the numeral.</param>    
@@ -2300,13 +2281,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return new RatNum(this, Native.mkInt64(nCtx(), v, RealSort().NativeObject()));
         }
 
-        /**
-         * Create a real numeral.
-         * <param name="v">value of the numeral.</param>    
-         * @return A Term with value <paramref name="v"/> and sort Real
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create an integer numeral.
          * <param name="v">A string representing the Term value in decimal notation.</param>
@@ -2330,13 +2304,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return new IntNum(this, Native.mkInt(nCtx(), v, IntSort().NativeObject()));
         }
 
-        /**
-         * Create an integer numeral.
-         * <param name="v">value of the numeral.</param>    
-         * @return A Term with value <paramref name="v"/> and sort Integer
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create an integer numeral.
          * <param name="v">value of the numeral.</param>    
@@ -2349,13 +2316,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return new IntNum(this, Native.mkInt64(nCtx(), v, IntSort().NativeObject()));
         }
 
-        /**
-         * Create an integer numeral.
-         * <param name="v">value of the numeral.</param>    
-         * @return A Term with value <paramref name="v"/> and sort Integer
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create a bit-vector numeral.
          * <param name="v">A string representing the value in decimal notation.</param>
@@ -2380,13 +2340,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
         }
 
-        /**
-         * Create a bit-vector numeral.
-         * <param name="v">value of the numeral.</param>    
-         * <param name="size">the size of the bit-vector</param>
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
         /**
          * Create a bit-vector numeral.
          * <param name="v">value of the numeral.</param>
@@ -2399,13 +2352,6 @@ import com.Microsoft.Z3.Enumerations.*;
             return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
         }
 
-        /**
-         * Create a bit-vector numeral.
-         * <param name="v">value of the numeral.</param>
-         * <param name="size">the size of the bit-vector</param>
-         **/
-        /* Not translated because it would translate to a function with clashing types. */
-
 
         /**
          * Create a universal Quantifier.
@@ -2551,7 +2497,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <seealso cref="FuncDecl.ToString()"/>
          * <seealso cref="Sort.ToString()"/>
          **/
-        public void setPrintMode(Z3_ast_print_mode value)  { Native.setAstPrintMode(nCtx(), (int)value); }
+        public void setPrintMode(Z3_ast_print_mode value)  { Native.setAstPrintMode(nCtx(), value.toInt()); }
 
         /**
          * Convert a benchmark into an SMT-LIB formatted string.
@@ -3356,12 +3302,12 @@ import com.Microsoft.Z3.Enumerations.*;
          **/
         public String GetParamValue(String id)
         {
-            long res = 0;
-            int r = Native.getParamValue(nCtx(), id, res);
-            if (r == Z3_lbool.Z3_L_FALSE.toInt())
+            String res = new String();
+            boolean r = Native.getParamValue(nCtx(), id, res);
+            if (!r)
                 return null;
             else
-                return Marshal.PtrToStringAnsi(res);
+                return res;
         }
 
 
@@ -3376,7 +3322,7 @@ import com.Microsoft.Z3.Enumerations.*;
 
         void InitContext()
         {
-            PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
+            setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
             m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // keep reference so it doesn't get collected.
             Native.setErrorHandler(m_ctx, m_n_err_handler);
             
@@ -3386,7 +3332,7 @@ import com.Microsoft.Z3.Enumerations.*;
         {
             
 
-            if (!ReferenceEquals(this, other.Context))
+            if (this == other.Context())
                 throw new Z3Exception("Context mismatch");
         }
 
@@ -3402,25 +3348,6 @@ import com.Microsoft.Z3.Enumerations.*;
                     CheckContextMatch(a);
                 }
             }
-        }
-
-        private void ObjectInvariant()
-        {
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
-            
         }
 
         private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
@@ -3473,7 +3400,8 @@ import com.Microsoft.Z3.Enumerations.*;
                 m_ctx = 0;
             }
             else
-                GC.ReRegisterForFinalize(this);
+		/* re-queue the finalizer */
+                new Context(m_ctx);
         }
 
         /**
diff --git a/src/api/java/com/Microsoft/Z3/DatatypeSort.java b/src/api/java/com/Microsoft/Z3/DatatypeSort.java
index 4d2dd8992..536bfa8bb 100644
--- a/src/api/java/com/Microsoft/Z3/DatatypeSort.java
+++ b/src/api/java/com/Microsoft/Z3/DatatypeSort.java
@@ -61,7 +61,7 @@ import com.Microsoft.Z3.Enumerations.*;
                 for (int i = 0; i < n; i++)
                 {
                     FuncDecl fd = new FuncDecl(Context(), Native.getDatatypeSortConstructor(Context().nCtx(), NativeObject(), i));
-                    int ds = fd.DomainSize;
+                    int ds = fd.DomainSize();
                     FuncDecl[] tmp = new FuncDecl[ds];
                     for (int j = 0; j < ds; j++)
                         tmp[j] = new FuncDecl(Context(), Native.getDatatypeSortConstructorAccessor(Context().nCtx(), NativeObject(), i, j));
diff --git a/src/api/java/com/Microsoft/Z3/EnumSort.java b/src/api/java/com/Microsoft/Z3/EnumSort.java
index cfb9d099a..ab0620003 100644
--- a/src/api/java/com/Microsoft/Z3/EnumSort.java
+++ b/src/api/java/com/Microsoft/Z3/EnumSort.java
@@ -68,8 +68,8 @@ import com.Microsoft.Z3.Enumerations.*;
             int n = enumNames.length;
             long[] n_constdecls = new long[n];
             long[] n_testers = new long[n];
-            NativeObject() = Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n,
-                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
+            setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), name.NativeObject(), (int)n,
+						     Symbol.ArrayToNative(enumNames), n_constdecls, n_testers));
             _constdecls = new FuncDecl[n];
             for (int i = 0; i < n; i++)
                 _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
@@ -78,6 +78,6 @@ import com.Microsoft.Z3.Enumerations.*;
                 _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
             _consts = new Expr[n];
             for (int i = 0; i < n; i++)
-                _consts[i] = ctx.MkApp(_constdecls[i]);
+                _consts[i] = ctx.MkApp(_constdecls[i], null);
         }
     };
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
index 66841c073..931d70f62 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_ast_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
index bfbbadd96..37da961d7 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_ast_print_mode.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_ast_print_mode
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
index c9ae9aa35..dd701c1e1 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_decl_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_decl_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
index 0c1c22870..2672c9325 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_error_code.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_error_code
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
index 2d96c6e76..f16fe51ec 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_goal_prec.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_goal_prec
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
index d31f5c238..55d5d7e17 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_lbool.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_lbool
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
index 81b8ef7bd..086622e95 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_param_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_param_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
index c009104ba..021157183 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_parameter_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_parameter_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
index 43f5b2f14..91559a58a 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_sort_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_sort_kind
diff --git a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
index 2f08236de..0866dc786 100644
--- a/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
+++ b/src/api/java/com/Microsoft/Z3/Enumerations/Z3_symbol_kind.java
@@ -2,7 +2,7 @@
  *  Automatically generated file
  **/
 
-package com.Microsoft.Z3;
+package com.Microsoft.Z3.Enumerations;
 
 /**
  * Z3_symbol_kind
diff --git a/src/api/java/com/Microsoft/Z3/Expr.java b/src/api/java/com/Microsoft/Z3/Expr.java
index 0851acf70..9cf25ed11 100644
--- a/src/api/java/com/Microsoft/Z3/Expr.java
+++ b/src/api/java/com/Microsoft/Z3/Expr.java
@@ -21,7 +21,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <param name="p">A set of parameters to configure the simplifier</param>
          * <seealso cref="Context.SimplifyHelp"/>
          **/
-        public Expr Simplify(Params p)
+        public Expr Simplify(Params p) throws Z3Exception
         {
             
 
@@ -54,7 +54,7 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * The arguments of the expression.
          **/
-        public Expr[] Args() 
+        public Expr[] Args() throws Z3Exception
             {
                 
 
@@ -69,7 +69,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * Update the arguments of the expression using the arguments <paramref name="args"/>
          * The number of new arguments should coincide with the current number of arguments.
          **/
-        public void Update(Expr[] args)
+        public void Update(Expr[] args) throws Z3Exception
         {
             
             
@@ -88,7 +88,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * sort of <code>from[i]</code> must be equal to sort of <code>to[i]</code>.
          * </remarks>    
          **/
-        public Expr Substitute(Expr[] from, Expr[] to)
+        public Expr Substitute(Expr[] from, Expr[] to) throws Z3Exception
         {
             
             
@@ -107,7 +107,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * Substitute every occurrence of <code>from</code> in the expression with <code>to</code>.
          * <seealso cref="Substitute(Expr[],Expr[])"/>
          **/
-        public Expr Substitute(Expr from, Expr to)
+        public Expr Substitute(Expr from, Expr to) throws Z3Exception
         {
             
             
@@ -122,7 +122,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * For every <code>i</code> smaller than <code>num_exprs</code>, the variable with de-Bruijn index <code>i</code> is replaced with term <code>to[i]</code>.
          * </remarks>
          **/
-        public Expr SubstituteVars(Expr[] to)
+        public Expr SubstituteVars(Expr[] to) throws Z3Exception
         {
             
             
@@ -137,7 +137,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * <param name="ctx">A context</param>
          * @return A copy of the term which is associated with <paramref name="ctx"/>
          **/
-        public Expr Translate(Context ctx)
+        public Expr Translate(Context ctx) throws Z3Exception
         {
             
             
@@ -1367,7 +1367,7 @@ import com.Microsoft.Z3.Enumerations.*;
          * index.
          * </remarks>
          **/
-        public int Index() 
+        public int Index() throws Z3Exception
             {
                 if (!IsVar())
                     throw new Z3Exception("Term is not a bound variable.");
@@ -1384,9 +1384,9 @@ import com.Microsoft.Z3.Enumerations.*;
         /** 
          * Constructor for Expr 
          **/
-    protected Expr(Context ctx, long obj) { super(ctx, obj); {  }}
+    protected Expr(Context ctx, long obj) throws Z3Exception { super(ctx, obj); {  }}
 
-        void CheckNativeObject(long obj)
+        void CheckNativeObject(long obj) throws Z3Exception
         {
             if (Native.isApp(Context().nCtx(), obj) ^ true &&
                 Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
@@ -1395,7 +1395,7 @@ import com.Microsoft.Z3.Enumerations.*;
             super.CheckNativeObject(obj);
         }
 
-        static Expr Create(Context ctx, FuncDecl f, Expr[] arguments)
+        static Expr Create(Context ctx, FuncDecl f, Expr[] arguments) throws Z3Exception
         {
             
             
@@ -1407,7 +1407,7 @@ import com.Microsoft.Z3.Enumerations.*;
             return Create(ctx, obj);
         }
 
-        static Expr Create(Context ctx, long obj)
+        static Expr Create(Context ctx, long obj) throws Z3Exception
         {
             
             
diff --git a/src/api/java/com/Microsoft/Z3/Fixedpoint.java b/src/api/java/com/Microsoft/Z3/Fixedpoint.java
index 104fd354c..e2cc2a1e9 100644
--- a/src/api/java/com/Microsoft/Z3/Fixedpoint.java
+++ b/src/api/java/com/Microsoft/Z3/Fixedpoint.java
@@ -123,8 +123,8 @@ import com.Microsoft.Z3.Enumerations.*;
             
 
             Context().CheckContextMatch(relations);
-            Z3_lbool r = (Z3_lbool)Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
-                                   AST.ArrayLength(relations), AST.ArrayToNative(relations));
+            Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(Context().nCtx(), NativeObject(),
+									  AST.ArrayLength(relations), AST.ArrayToNative(relations)));
             switch (r)
             {
                 case Z3_L_TRUE: return Status.SATISFIABLE;
@@ -248,10 +248,10 @@ import com.Microsoft.Z3.Enumerations.*;
                 
 
                 ASTVector v = new ASTVector(Context(), Native.fixedpointGetRules(Context().nCtx(), NativeObject()));
-                int n = v.Size;
+                int n = v.Size();
                 BoolExpr[] res = new BoolExpr[n];
                 for (int i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context(), v[i].NativeObject());
+                    res[i] = new BoolExpr(Context(), v.get(i).NativeObject());
                 return res;
             }
 
@@ -263,10 +263,10 @@ import com.Microsoft.Z3.Enumerations.*;
                 
 
                 ASTVector v = new ASTVector(Context(), Native.fixedpointGetAssertions(Context().nCtx(), NativeObject()));
-                int n = v.Size;
+                int n = v.Size();
                 BoolExpr[] res = new BoolExpr[n];
                 for (int i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context(), v[i].NativeObject());
+                    res[i] = new BoolExpr(Context(), v.get(i).NativeObject());
                 return res;
             }
 
diff --git a/src/api/java/com/Microsoft/Z3/FuncDecl.java b/src/api/java/com/Microsoft/Z3/FuncDecl.java
index aa716c028..82cccc36f 100644
--- a/src/api/java/com/Microsoft/Z3/FuncDecl.java
+++ b/src/api/java/com/Microsoft/Z3/FuncDecl.java
@@ -77,7 +77,7 @@ import com.Microsoft.Z3.Enumerations.*;
             {
                 
 
-                var n = DomainSize;
+                int n = DomainSize();
 
                 Sort[] res = new Sort[n];
                 for (int i = 0; i < n; i++)
@@ -171,25 +171,25 @@ import com.Microsoft.Z3.Enumerations.*;
 
             /**The int value of the parameter.</summary>
          **/
-            public int Int () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; }
+            public int Int () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; }
             /**The double value of the parameter.</summary>
          **/
-            public double Double () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; }
+            public double Double () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; }
             /**The Symbol value of the parameter.</summary>
          **/
-            public Symbol Symbol () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; }
+            public Symbol Symbol () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; }
             /**The Sort value of the parameter.</summary>
          **/
-            public Sort Sort () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; }
+            public Sort Sort () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; }
             /**The AST value of the parameter.</summary>
          **/
-            public AST AST () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; }
+            public AST AST () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; }
             /**The FunctionDeclaration value of the parameter.</summary>
          **/
-            public FuncDecl FuncDecl () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; }
+            public FuncDecl FuncDecl () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; }
             /**The rational string value of the parameter.</summary>
          **/
-            public String Rational () { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; }
+            public String Rational () { if (ParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational String"); return r; }
 
             /**
              * The kind of the parameter.
diff --git a/src/api/java/com/Microsoft/Z3/FuncInterp.java b/src/api/java/com/Microsoft/Z3/FuncInterp.java
index 341b82ec5..17ff7d6bd 100644
--- a/src/api/java/com/Microsoft/Z3/FuncInterp.java
+++ b/src/api/java/com/Microsoft/Z3/FuncInterp.java
@@ -59,10 +59,10 @@ import com.Microsoft.Z3.Enumerations.*;
             {
                 int n = NumArgs();
                 String res = "[";
-                Expr[] args = Args;
+                Expr[] args = Args();
                 for (int i = 0; i < n; i++)
                     res += args[i] + ", ";
-                return res + Value + "]";
+                return res + Value() + "]";
             }
 
         Entry(Context ctx, long obj) { super(ctx, obj); {  }}
@@ -135,20 +135,20 @@ import com.Microsoft.Z3.Enumerations.*;
         {
             String res = "";
             res += "[";
-            for (Entry e: Entries)
+            for (Entry e: Entries())
             {
-                int n = e.NumArgs;
+                int n = e.NumArgs();
                 if (n > 1) res += "[";
-                Expr[] args = e.Args;
+                Expr[] args = e.Args();
                 for (int i = 0; i < n; i++)
                 {
                     if (i != 0) res += ", ";
                     res += args[i];
                 }
                 if (n > 1) res += "]";
-                res += " -> " + e.Value + ", ";
+                res += " -> " + e.Value() + ", ";
             }
-            res += "else -> " + Else;
+            res += "else -> " + Else();
             res += "]";
             return res;
         }
diff --git a/src/api/java/com/Microsoft/Z3/Goal.java b/src/api/java/com/Microsoft/Z3/Goal.java
index 9f522a768..9ca138140 100644
--- a/src/api/java/com/Microsoft/Z3/Goal.java
+++ b/src/api/java/com/Microsoft/Z3/Goal.java
@@ -31,21 +31,21 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * Indicates whether the goal is precise.
          **/
-        public boolean IsPrecise()  { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
+        public boolean IsPrecise()  { return Precision() == Z3_goal_prec.Z3_GOAL_PRECISE; }
         /**
          * Indicates whether the goal is an under-approximation.
          **/
-        public boolean IsUnderApproximation()  { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
+        public boolean IsUnderApproximation()  { return Precision() == Z3_goal_prec.Z3_GOAL_UNDER; }
 
         /**
          * Indicates whether the goal is an over-approximation.
          **/
-        public boolean IsOverApproximation()  { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
+        public boolean IsOverApproximation()  { return Precision() == Z3_goal_prec.Z3_GOAL_OVER; }
 
         /**
          * Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
          **/
-        public boolean IsGarbage()  { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
+        public boolean IsGarbage()  { return Precision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
 
         /**
          * Adds the <paramref name="constraints"/> to the given goal. 
@@ -96,7 +96,7 @@ import com.Microsoft.Z3.Enumerations.*;
             {
                 
 
-                int n = Size;
+                int n = Size();
                 BoolExpr[] res = new BoolExpr[n];
                 for (int i = 0; i < n; i++)
                     res[i] = new BoolExpr(Context(), Native.goalFormula(Context().nCtx(), NativeObject(), i));
@@ -132,15 +132,15 @@ import com.Microsoft.Z3.Enumerations.*;
          * Simplifies the goal.
          * <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks>
          **/
-        public Goal Simplify(Params p)
+        public Goal Simplify(Params p) throws Z3Exception
         {
             Tactic t = Context().MkTactic("simplify");
             ApplyResult res = t.Apply(this, p);
             
-            if (res.NumSubgoals == 0)
-                return Context().MkGoal();
+            if (res.NumSubgoals() == 0)
+                throw new Z3Exception("No subgoals");
             else        
-                return res.Subgoals[0];
+                return res.Subgoals()[0];
         }
 
         /**
@@ -152,11 +152,11 @@ import com.Microsoft.Z3.Enumerations.*;
             return Native.goalToString(Context().nCtx(), NativeObject());
         }
 
-    Goal(Context ctx, long obj) { super(ctx, obj); {  }}
+	Goal(Context ctx, long obj) { super(ctx, obj); {  }}
 
         Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
-        { super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false));
-            
+        { 
+	    super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, (unsatCores) ? true : false, (proofs) ? true : false));            
         }
 
         class DecRefQueue extends IDecRefQueue
diff --git a/src/api/java/com/Microsoft/Z3/IDisposable.java b/src/api/java/com/Microsoft/Z3/IDisposable.java
index 03885d1e7..e0cbb84f0 100644
--- a/src/api/java/com/Microsoft/Z3/IDisposable.java
+++ b/src/api/java/com/Microsoft/Z3/IDisposable.java
@@ -21,5 +21,5 @@ package com.Microsoft.Z3;
 
 public class IDisposable
 {
-    public void Dispose() {}
+    public void Dispose() throws Z3Exception {}
 }
diff --git a/src/api/java/com/Microsoft/Z3/IntSymbol.java b/src/api/java/com/Microsoft/Z3/IntSymbol.java
index 1750d87e6..7b917c11d 100644
--- a/src/api/java/com/Microsoft/Z3/IntSymbol.java
+++ b/src/api/java/com/Microsoft/Z3/IntSymbol.java
@@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
 
         void CheckNativeObject(long obj)
         {
-            if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
+            if (Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL.toInt())
                 throw new Z3Exception("Symbol is not of integer kind");
             super.CheckNativeObject(obj);
         }
diff --git a/src/api/java/com/Microsoft/Z3/ListSort.java b/src/api/java/com/Microsoft/Z3/ListSort.java
index 4efee3783..7e7b03f79 100644
--- a/src/api/java/com/Microsoft/Z3/ListSort.java
+++ b/src/api/java/com/Microsoft/Z3/ListSort.java
@@ -110,8 +110,8 @@ import com.Microsoft.Z3.Enumerations.*;
                    ihead = 0,
                    itail = 0;
 
-            NativeObject() = Native.mkListSort(ctx.nCtx(), name.NativeObject(), elemSort.NativeObject(),
-                                                  inil, iisnil, icons, iiscons, ihead, itail);
+            setNativeObject(Native.mkListSort(ctx.nCtx(), name.NativeObject(), elemSort.NativeObject(),
+					      inil, iisnil, icons, iiscons, ihead, itail));
             nilDecl = new FuncDecl(ctx, inil);
             isNilDecl = new FuncDecl(ctx, iisnil);
             consDecl = new FuncDecl(ctx, icons);
diff --git a/src/api/java/com/Microsoft/Z3/Model.java b/src/api/java/com/Microsoft/Z3/Model.java
index c0c0e2852..f17dc1956 100644
--- a/src/api/java/com/Microsoft/Z3/Model.java
+++ b/src/api/java/com/Microsoft/Z3/Model.java
@@ -26,7 +26,7 @@ import com.Microsoft.Z3.Enumerations.*;
             
 
             Context().CheckContextMatch(a);
-            return ConstInterp(a.FuncDecl);
+            return ConstInterp(a.FuncDecl());
         }
 
         /**
@@ -39,7 +39,7 @@ import com.Microsoft.Z3.Enumerations.*;
             
 
             Context().CheckContextMatch(f);
-            if (f.Arity != 0 ||
+            if (f.Arity() != 0 ||
                 Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT.toInt())
                 throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
 
@@ -63,7 +63,7 @@ import com.Microsoft.Z3.Enumerations.*;
 
             Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(Context().nCtx(), Native.getRange(Context().nCtx(), f.NativeObject())));
 
-            if (f.Arity == 0)
+            if (f.Arity() == 0)
             {
                 long n = Native.modelGetConstInterp(Context().nCtx(), NativeObject(), f.NativeObject());
 
@@ -139,8 +139,8 @@ import com.Microsoft.Z3.Enumerations.*;
             {
                 
 
-                var nFuncs = NumFuncs();
-                var nConsts = NumConsts();
+                int nFuncs = NumFuncs();
+                int nConsts = NumConsts();
                 int n = nFuncs + nConsts;
                 FuncDecl[] res = new FuncDecl[n];
                 for (int i = 0; i < nConsts; i++)
@@ -236,10 +236,10 @@ import com.Microsoft.Z3.Enumerations.*;
             
 
             ASTVector nUniv = new ASTVector(Context(), Native.modelGetSortUniverse(Context().nCtx(), NativeObject(), s.NativeObject()));
-            int n = nUniv.Size;
+            int n = nUniv.Size();
             Expr[] res = new Expr[n];
             for (int i = 0; i < n; i++)
-                res[i] = Expr.Create(Context(), nUniv[i].NativeObject());
+                res[i] = Expr.Create(Context(), nUniv.get(i).NativeObject());
             return res;
         }
 
diff --git a/src/api/java/com/Microsoft/Z3/Native.java b/src/api/java/com/Microsoft/Z3/Native.java
index e42d8b7ba..8acf96cbf 100644
--- a/src/api/java/com/Microsoft/Z3/Native.java
+++ b/src/api/java/com/Microsoft/Z3/Native.java
@@ -5,7 +5,7 @@ public final class Native {
   public static class LongPtr { public long value; }
   public static class StringPtr { public String value; }
   public static class errorHandler { public long ptr; }
-  static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0235B918>"); }
+  static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x0256D828>"); }
   public static native long mkConfig();
   public static native void delConfig(long a0);
   public static native void setParamValue(long a0, String a1, String a2);
diff --git a/src/api/java/com/Microsoft/Z3/Params.java b/src/api/java/com/Microsoft/Z3/Params.java
index 1107a80ee..ab6401833 100644
--- a/src/api/java/com/Microsoft/Z3/Params.java
+++ b/src/api/java/com/Microsoft/Z3/Params.java
@@ -26,16 +26,6 @@ import com.Microsoft.Z3.Enumerations.*;
             Native.paramsSetBool(Context().nCtx(), NativeObject(), name.NativeObject(), (value) ? true : false);
         }
 
-        /**
-         * Adds a parameter setting.
-         **/
-        public void Add(Symbol name, int value)
-        {
-            
-
-            Native.paramsSetInt(Context().nCtx(), NativeObject(), name.NativeObject(), value);
-        }
-
         /**
          * Adds a parameter setting.
          **/
@@ -70,7 +60,7 @@ import com.Microsoft.Z3.Enumerations.*;
          **/
         public void Add(String name, int value)
         {
-            Native.paramsSetInt(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
+            Native.paramsSetUint(Context().nCtx(), NativeObject(), Context().MkSymbol(name).NativeObject(), value);
         }
 
         /**
diff --git a/src/api/java/com/Microsoft/Z3/Quantifier.java b/src/api/java/com/Microsoft/Z3/Quantifier.java
index ad05c544b..b841623c2 100644
--- a/src/api/java/com/Microsoft/Z3/Quantifier.java
+++ b/src/api/java/com/Microsoft/Z3/Quantifier.java
@@ -24,7 +24,7 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * Indicates whether the quantifier is existential.
          **/
-        public boolean IsExistential()  { return !IsUniversal; }
+        public boolean IsExistential()  { return !IsUniversal(); }
 
         /**
          * The weight of the quantifier.
@@ -137,21 +137,21 @@ import com.Microsoft.Z3.Enumerations.*;
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject() = Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight,
-                                           AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
-                                           AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
-                                           Symbol.ArrayToNative(names),
-                                           body.NativeObject());
+                setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight,
+						 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+						 AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+						 Symbol.ArrayToNative(names),
+						 body.NativeObject()));
             }
             else
             {
-                NativeObject() = Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, weight,
-                                  AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
-                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
-                                  AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
-                                  AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
-                                  Symbol.ArrayToNative(names),
-                                  body.NativeObject());
+                setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, weight,
+						      AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
+						      AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+						      AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
+						      AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
+						      Symbol.ArrayToNative(names),
+						      body.NativeObject()));
             }
         }
 
@@ -171,19 +171,19 @@ import com.Microsoft.Z3.Enumerations.*;
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject() = Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight,
-                                                 AST.ArrayLength(bound), AST.ArrayToNative(bound),
-                                                 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
-                                                 body.NativeObject());
+                setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight,
+							 AST.ArrayLength(bound), AST.ArrayToNative(bound),
+							 AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+							 body.NativeObject()));
             }
             else
             {
-                NativeObject() = Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, weight,
-                                        AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
-                                        AST.ArrayLength(bound), AST.ArrayToNative(bound),
-                                        AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
-                                        AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
-                                        body.NativeObject());
+                setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, weight,
+							   AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
+							   AST.ArrayLength(bound), AST.ArrayToNative(bound),
+							   AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
+							   AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
+							   body.NativeObject()));
             }
         }
 
@@ -192,7 +192,7 @@ import com.Microsoft.Z3.Enumerations.*;
 
         void CheckNativeObject(long obj)
         {
-            if ((Z3_ast_kind)Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
+            if (Native.getAstKind(Context().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
                 throw new Z3Exception("Underlying object is not a quantifier");
             super.CheckNativeObject(obj);
         }
diff --git a/src/api/java/com/Microsoft/Z3/RatNum.java b/src/api/java/com/Microsoft/Z3/RatNum.java
index ad0982a95..ff0b3d18a 100644
--- a/src/api/java/com/Microsoft/Z3/RatNum.java
+++ b/src/api/java/com/Microsoft/Z3/RatNum.java
@@ -72,7 +72,7 @@ import com.Microsoft.Z3.Enumerations.*;
             return Native.getNumeralString(Context().nCtx(), NativeObject());
         }
 
-        RatNum(Context ctx, long obj)
+        RatNum(Context ctx, long obj) throws Z3Exception
         { super(ctx, obj);
             
         }
diff --git a/src/api/java/com/Microsoft/Z3/RealExpr.java b/src/api/java/com/Microsoft/Z3/RealExpr.java
index 2f06e4643..907148c2a 100644
--- a/src/api/java/com/Microsoft/Z3/RealExpr.java
+++ b/src/api/java/com/Microsoft/Z3/RealExpr.java
@@ -19,13 +19,15 @@ import com.Microsoft.Z3.Enumerations.*;
      **/
     public class RealExpr extends ArithExpr
     {
-        /** Constructor for RealExpr </summary>
-     **/
+        /** 
+	 *  Constructor for RealExpr </summary>
+	**/
         protected RealExpr(Context ctx)
         { super(ctx);
             
         }
-        RealExpr(Context ctx, long obj)
+
+        RealExpr(Context ctx, long obj) throws Z3Exception
         { super(ctx, obj);
             
         }
diff --git a/src/api/java/com/Microsoft/Z3/RelationSort.java b/src/api/java/com/Microsoft/Z3/RelationSort.java
index 85f083b57..564c66eaf 100644
--- a/src/api/java/com/Microsoft/Z3/RelationSort.java
+++ b/src/api/java/com/Microsoft/Z3/RelationSort.java
@@ -31,7 +31,7 @@ import com.Microsoft.Z3.Enumerations.*;
                 if (m_columnSorts != null)
                     return m_columnSorts;
 
-                int n = Arity;
+                int n = Arity();
                 Sort[] res = new Sort[n];
                 for (int i = 0; i < n; i++)
                     res[i] = Sort.Create(Context(), Native.getRelationColumn(Context().nCtx(), NativeObject(), i));
diff --git a/src/api/java/com/Microsoft/Z3/Solver.java b/src/api/java/com/Microsoft/Z3/Solver.java
index 5fda96bb1..1f6f099b3 100644
--- a/src/api/java/com/Microsoft/Z3/Solver.java
+++ b/src/api/java/com/Microsoft/Z3/Solver.java
@@ -99,7 +99,7 @@ import com.Microsoft.Z3.Enumerations.*;
         public int NumAssertions() 
             {
                 ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
-                return ass.Size;
+                return ass.Size();
             }
 
         /**
@@ -110,10 +110,10 @@ import com.Microsoft.Z3.Enumerations.*;
                 
 
                 ASTVector ass = new ASTVector(Context(), Native.solverGetAssertions(Context().nCtx(), NativeObject()));
-                int n = ass.Size;
+                int n = ass.Size();
                 BoolExpr[] res = new BoolExpr[n];
                 for (int i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context(), ass[i].NativeObject());
+                    res[i] = new BoolExpr(Context(), ass.get(i).NativeObject());
                 return res;
             }
 
@@ -185,10 +185,10 @@ import com.Microsoft.Z3.Enumerations.*;
                 
 
                 ASTVector core = new ASTVector(Context(), Native.solverGetUnsatCore(Context().nCtx(), NativeObject()));
-                int n = core.Size;
+                int n = core.Size();
                 Expr[] res = new Expr[n];
                 for (int i = 0; i < n; i++)
-                    res[i] = Expr.Create(Context(), core[i].NativeObject());
+                    res[i] = Expr.Create(Context(), core.get(i).NativeObject());
                 return res;
             }
 
diff --git a/src/api/java/com/Microsoft/Z3/Statistics.java b/src/api/java/com/Microsoft/Z3/Statistics.java
index ec64ee0b3..93cd6e706 100644
--- a/src/api/java/com/Microsoft/Z3/Statistics.java
+++ b/src/api/java/com/Microsoft/Z3/Statistics.java
@@ -25,6 +25,8 @@ import com.Microsoft.Z3.Enumerations.*;
             /**
              * The key of the entry.
              **/
+	    public String Key;
+
             /**
              * The uint-value of the entry.
              **/
@@ -49,10 +51,10 @@ import com.Microsoft.Z3.Enumerations.*;
                 {
                     
 
-                    if (IsUInt)
-                        return m_int.toString();
-                    else if (IsDouble)
-                        return m_double.toString();
+                    if (IsUInt())
+                        return Integer.toString(m_int);
+                    else if (IsDouble())
+                        return Double.toString(m_double);
                     else
                         throw new Z3Exception("Unknown statistical entry type");
                 }
@@ -62,7 +64,7 @@ import com.Microsoft.Z3.Enumerations.*;
              **/
             public String toString()
             {
-                return Key + ": " + Value;
+                return Key + ": " + Value();
             }
 
             private boolean m_is_int = false;
@@ -71,13 +73,13 @@ import com.Microsoft.Z3.Enumerations.*;
             private double m_double = 0.0;
             Entry(String k, int v)
             {
-                Key = k;
+		Key = k;
                 m_is_int = true;
                 m_int = v;
             }
             Entry(String k, double v)
             {
-                Key = k;
+		Key = k;
                 m_is_double = true;
                 m_double = v;
             }
@@ -105,14 +107,14 @@ import com.Microsoft.Z3.Enumerations.*;
                 
                 
 
-                int n = Size;
+                int n = Size();
                 Entry[] res = new Entry[n];
                 for (int i = 0; i < n; i++)
                 {
                     Entry e;
                     String k = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
-                    if (Native.statsIsInt(Context().nCtx(), NativeObject(), i) )
-                        e = new Entry(k, Native.statsGetIntValue(Context().nCtx(), NativeObject(), i));
+                    if (Native.statsIsUint(Context().nCtx(), NativeObject(), i) )
+                        e = new Entry(k, Native.statsGetUintValue(Context().nCtx(), NativeObject(), i));
                     else if (Native.statsIsDouble(Context().nCtx(), NativeObject(), i) )
                         e = new Entry(k, Native.statsGetDoubleValue(Context().nCtx(), NativeObject(), i));
                     else
@@ -129,7 +131,7 @@ import com.Microsoft.Z3.Enumerations.*;
             {
                 
 
-                int n = Size;
+                int n = Size();
                 String[] res = new String[n];
                 for (int i = 0; i < n; i++)
                     res[i] = Native.statsGetKey(Context().nCtx(), NativeObject(), i);
@@ -142,8 +144,8 @@ import com.Microsoft.Z3.Enumerations.*;
          **/
         public Entry get(String key) 
             {
-                int n = Size;
-                Entry[] es = Entries;
+                int n = Size();
+                Entry[] es = Entries();
                 for (int i = 0; i < n; i++)
                     if (es[i].Key == key)
                         return es[i];
diff --git a/src/api/java/com/Microsoft/Z3/Status.java b/src/api/java/com/Microsoft/Z3/Status.java
index 64bd9f767..fdccb7376 100644
--- a/src/api/java/com/Microsoft/Z3/Status.java
+++ b/src/api/java/com/Microsoft/Z3/Status.java
@@ -14,21 +14,29 @@ import com.Microsoft.Z3.Enumerations.*;
   /**
    * Status values.
    **/
-  public class Status
+  public enum Status
   {    
-    /// <summary>
     /// Used to signify an unsatisfiable status.
-    /// </summary>
-public static final int     UNSATISFIABLE  = 1;
+      UNSATISFIABLE (1),
 
-    /// <summary>
     /// Used to signify an unknown status.
-    /// </summary>
-public static final int     UNKNOWN  = 0;
+      UNKNOWN  (0),
 
-    /// <summary>
     /// Used to signify a satisfiable status.
-    /// </summary>
-public static final int     SATISFIABLE  = 1;
+      SATISFIABLE  (1);
+
+    private final int intValue;
+
+    Status (int v) {
+        this.intValue = v;
+    }
+
+    public static final Status fromInt(int v) {
+        for (Status  k: values()) 
+            if (k.intValue == v) return k;
+        return values()[0];
+    }
+
+    public final int toInt() { return this.intValue; }
   }
 
diff --git a/src/api/java/com/Microsoft/Z3/StringSymbol.java b/src/api/java/com/Microsoft/Z3/StringSymbol.java
index 1ff869002..5788c0944 100644
--- a/src/api/java/com/Microsoft/Z3/StringSymbol.java
+++ b/src/api/java/com/Microsoft/Z3/StringSymbol.java
@@ -43,7 +43,7 @@ import com.Microsoft.Z3.Enumerations.*;
 
         void CheckNativeObject(long obj)
         {
-            if ((Z3_symbol_kind)Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
+            if (Native.getSymbolKind(Context().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL.toInt())
                 throw new Z3Exception("Symbol is not of String kind");
 
             super.CheckNativeObject(obj);
diff --git a/src/api/java/com/Microsoft/Z3/Symbol.java b/src/api/java/com/Microsoft/Z3/Symbol.java
index b7653414d..0cd0632de 100644
--- a/src/api/java/com/Microsoft/Z3/Symbol.java
+++ b/src/api/java/com/Microsoft/Z3/Symbol.java
@@ -27,7 +27,7 @@ import com.Microsoft.Z3.Enumerations.*;
          **/
         public boolean IsIntSymbol()
         {
-            return Kind == Z3_symbol_kind.Z3_INT_SYMBOL;
+            return Kind() == Z3_symbol_kind.Z3_INT_SYMBOL;
         }
 
         /**
@@ -35,7 +35,7 @@ import com.Microsoft.Z3.Enumerations.*;
          **/
         public boolean IsStringSymbol()
         {
-            return Kind == Z3_symbol_kind.Z3_STRING_SYMBOL;
+            return Kind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
         }
 
         /**
@@ -44,9 +44,9 @@ import com.Microsoft.Z3.Enumerations.*;
         public String toString()
         {
             if (IsIntSymbol())
-                return ((IntSymbol)this).Int.toString();
+                return Integer.toString(((IntSymbol)this).Int());
             else if (IsStringSymbol())
-                return ((StringSymbol)this).String;
+                return ((StringSymbol)this).String();
             else
                 throw new Z3Exception("Unknown symbol kind encountered");
         }
@@ -54,8 +54,8 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * Symbol constructor
          **/
-    protected Symbol(Context ctx, long obj) { super(ctx, obj); 
-            
+	protected Symbol(Context ctx, long obj) { 
+	    super(ctx, obj);            
         }
 
         static Symbol Create(Context ctx, long obj)
diff --git a/src/api/java/com/Microsoft/Z3/Tactic.java b/src/api/java/com/Microsoft/Z3/Tactic.java
index fd560847a..3ef1ab645 100644
--- a/src/api/java/com/Microsoft/Z3/Tactic.java
+++ b/src/api/java/com/Microsoft/Z3/Tactic.java
@@ -62,7 +62,7 @@ import com.Microsoft.Z3.Enumerations.*;
                 
                 
 
-                return Apply(g);
+                return Apply(g, null);
             }
 
         /**
diff --git a/src/api/java/com/Microsoft/Z3/TupleSort.java b/src/api/java/com/Microsoft/Z3/TupleSort.java
index 0ac03bb88..76a92f6c9 100644
--- a/src/api/java/com/Microsoft/Z3/TupleSort.java
+++ b/src/api/java/com/Microsoft/Z3/TupleSort.java
@@ -51,8 +51,8 @@ import com.Microsoft.Z3.Enumerations.*;
             
 
             long t = 0;
-            NativeObject() = Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields,
-                                                   Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
-                                                   t, new long[numFields]);
+            setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.NativeObject(), numFields,
+					       Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
+					       t, new long[numFields]));
         }
     };
diff --git a/src/api/java/com/Microsoft/Z3/Version.java b/src/api/java/com/Microsoft/Z3/Version.java
index c3fc4268d..e9f883aaa 100644
--- a/src/api/java/com/Microsoft/Z3/Version.java
+++ b/src/api/java/com/Microsoft/Z3/Version.java
@@ -68,6 +68,6 @@ import com.Microsoft.Z3.Enumerations.*;
 
             int major = 0, minor = 0, build = 0, revision = 0;
             Native.getVersion(major, minor, build, revision);
-            return major.toString() + "." + minor.toString() + "." + build.toString() + "." + revision.toString();
+            return Integer.toString(major) + "." + Integer.toString(minor) + "." + Integer.toString(build) + "." + Integer.toString(revision);
         }
     }
diff --git a/src/api/java/com/Microsoft/Z3/Z3Object.java b/src/api/java/com/Microsoft/Z3/Z3Object.java
index d4bdf08f7..1bbdbab8b 100644
--- a/src/api/java/com/Microsoft/Z3/Z3Object.java
+++ b/src/api/java/com/Microsoft/Z3/Z3Object.java
@@ -20,7 +20,7 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * Finalizer.
          **/
-        protected void finalize()
+        protected void finalize() throws Z3Exception
         {
             Dispose();            
         }
@@ -28,7 +28,7 @@ import com.Microsoft.Z3.Enumerations.*;
         /**
          * Disposes of the underlying native Z3 object.
          **/
-        public void Dispose()
+        public void Dispose() throws Z3Exception
         {
             if (m_n_obj != 0)
             {
@@ -65,7 +65,7 @@ import com.Microsoft.Z3.Enumerations.*;
             m_ctx = ctx;
         }
 
-        Z3Object(Context ctx, long obj)
+        Z3Object(Context ctx, long obj) throws Z3Exception
         {
             
 
@@ -75,13 +75,13 @@ import com.Microsoft.Z3.Enumerations.*;
             m_n_obj = obj;
         }
 
-        void IncRef(long o) { }
-        void DecRef(long o) { }
+        void IncRef(long o) throws Z3Exception { }
+        void DecRef(long o) throws Z3Exception { }
 
-        void CheckNativeObject(long obj) { }
+        void CheckNativeObject(long obj) throws Z3Exception { }
 
-                         long NativeObject()  { return m_n_obj; }
-                         void setNativeObject(long value) 
+	long NativeObject()  { return m_n_obj; }
+	void setNativeObject(long value)  throws Z3Exception
             {
                 if (value != 0) { CheckNativeObject(value); IncRef(value); }
                 if (m_n_obj != 0) { DecRef(m_n_obj); }
diff --git a/src/api/java/mk_java.py b/src/api/java/mk_java.py
index fe7f50a25..1c59fc957 100644
--- a/src/api/java/mk_java.py
+++ b/src/api/java/mk_java.py
@@ -163,11 +163,11 @@ def translate(filename):
                 tgt.write(t + " **/\n")
                 in_javadoc = 0
 
-        for i in range(0, len(EXCLUDE_METHODS)):
-            if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]):
-                tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
-                in_unsupported = 1
-                break
+        # for i in range(0, len(EXCLUDE_METHODS)):
+        #     if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]):
+        #         tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
+        #         in_unsupported = 1
+        #         break
                     
 
         if in_unsupported: