diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 4be02ce30..e84dc8c81 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -28,23 +28,16 @@ public class AST extends Z3Object implements Comparable<AST>
      * Object comparison.
      * 
      * @param o another AST
-     **/    
+     **/
+    @Override
     public boolean equals(Object o)
     {
-        AST casted = null;
+        if (o == this) return true;
+        if (!(o instanceof AST)) return false;
+        AST casted = (AST) o;
 
-        try
-        {
-            casted = AST.class.cast(o);
-        } catch (ClassCastException e)
-        {
-            return false;
-        }
-
-        return  (this == casted) ||
-                (this != null) &&
-                (casted != null) &&
-                (getContext().nCtx() == casted.getContext().nCtx()) &&
+        return
+            (getContext().nCtx() == casted.getContext().nCtx()) &&
                 (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
@@ -56,17 +49,13 @@ public class AST extends Z3Object implements Comparable<AST>
      * positive if after else zero.
      * @throws Z3Exception on error
      **/
+    @Override
     public int compareTo(AST other)
     {
-        if (other == null)
+        if (other == null) {
             return 1;
-
-        if (getId() < other.getId())
-            return -1;
-        else if (getId() > other.getId())
-            return +1;
-        else
-            return 0;
+        }
+        return Integer.compare(getId(), other.getId());
     }
 
     /**
@@ -74,14 +63,10 @@ public class AST extends Z3Object implements Comparable<AST>
      * 
      * @return A hash code
      **/
+    @Override
     public int hashCode()
     {
-        int r = 0;
-        try {
-            Native.getAstHash(getContext().nCtx(), getNativeObject());
-        }
-        catch (Z3Exception ex) {}
-        return r;
+        return Native.getAstHash(getContext().nCtx(), getNativeObject());
     }
 
     /**
@@ -103,11 +88,12 @@ public class AST extends Z3Object implements Comparable<AST>
     public AST translate(Context ctx)
     {
 
-        if (getContext() == ctx)
+        if (getContext() == ctx) {
             return this;
-        else
+        } else {
             return new AST(ctx, Native.translate(getContext().nCtx(),
-                    getNativeObject(), ctx.nCtx()));
+                getNativeObject(), ctx.nCtx()));
+        }
     }
 
     /**
@@ -188,6 +174,7 @@ public class AST extends Z3Object implements Comparable<AST>
     /**
      * A string representation of the AST.
      **/
+    @Override
     public String toString()
     {
         try
@@ -217,6 +204,7 @@ public class AST extends Z3Object implements Comparable<AST>
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         // Console.WriteLine("AST IncRef()");
@@ -226,6 +214,7 @@ public class AST extends Z3Object implements Comparable<AST>
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         // Console.WriteLine("AST DecRef()");
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index a8ee83e57..32f6a5d0e 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -29,6 +29,7 @@ class ASTDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ASTDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index afeb868ca..7bc485bf5 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -101,6 +101,7 @@ class ASTMap extends Z3Object
     /**
      * Retrieves a string representation of the map.
      **/
+    @Override
     public String toString()
     {
         try
@@ -122,12 +123,14 @@ class ASTMap extends Z3Object
         super(ctx, Native.mkAstMap(ctx.nCtx()));
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getASTMapDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getASTMapDRQ().add(o);
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 5b57db9d9..ab99e2aee 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -87,6 +87,7 @@ public class ASTVector extends Z3Object
     /**
      * Retrieves a string representation of the vector.
      **/
+    @Override
     public String toString()
     {
         try
@@ -108,12 +109,14 @@ public class ASTVector extends Z3Object
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getASTVectorDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getASTVectorDRQ().add(o);
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index 2812efd70..84c63e966 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -63,6 +63,7 @@ public class ApplyResult extends Z3Object
     /**
      * A string representation of the ApplyResult.
      **/
+    @Override
     public String toString()
     {
         try
@@ -79,12 +80,14 @@ public class ApplyResult extends Z3Object
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getApplyResultDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getApplyResultDRQ().add(o);
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index 4cdf312fe..63f315ecd 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -29,6 +29,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
index 2106ff0c2..1598f75e7 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -29,6 +29,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index 698e9e06b..a63d808d3 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -29,6 +29,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index 08da40256..5a62f8087 100644
--- a/src/api/java/BitVecNum.java
+++ b/src/api/java/BitVecNum.java
@@ -32,8 +32,9 @@ public class BitVecNum extends BitVecExpr
     public int getInt()
     {
         Native.IntPtr res = new Native.IntPtr();
-        if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
             throw new Z3Exception("Numeral is not an int");
+        }
         return res.value;
     }
 
@@ -45,8 +46,9 @@ public class BitVecNum extends BitVecExpr
     public long getLong()
     {
         Native.LongPtr res = new Native.LongPtr();
-        if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
             throw new Z3Exception("Numeral is not a long");
+        }
         return res.value;
     }
 
@@ -61,6 +63,7 @@ public class BitVecNum extends BitVecExpr
     /**
      * Returns a string representation of the numeral.
      **/
+    @Override
     public String toString()
     {
         try
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index 26b33ed35..a6c2856d4 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -87,11 +87,7 @@ public class Constructor extends Z3Object
     {
         try {
             Native.delConstructor(getContext().nCtx(), getNativeObject());
-        }
-        catch (Throwable t) {
-            throw t;
-        }
-        finally {
+        } finally {
             super.finalize();
         }
     }
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index 82b119513..fe3fae1ac 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -31,11 +31,7 @@ public class ConstructorList extends Z3Object
     {
         try {        
             Native.delConstructorList(getContext().nCtx(), getNativeObject());            
-        }
-        catch (Throwable t) {
-            throw t;
-        }
-        finally {
+        } finally {
             super.finalize();
         }
     }
@@ -50,7 +46,7 @@ public class ConstructorList extends Z3Object
         super(ctx);
 
         setNativeObject(Native.mkConstructorList(getContext().nCtx(),
-                (int) constructors.length,
+                constructors.length,
                 Constructor.arrayToNative(constructors)));
     }
 }
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 40b597be4..9fa17fcd4 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -110,8 +110,9 @@ public class Context extends IDisposable
      **/
     public BoolSort getBoolSort()
     {
-        if (m_boolSort == null)
+        if (m_boolSort == null) {
             m_boolSort = new BoolSort(this);
+        }
         return m_boolSort;
     }
 
@@ -120,8 +121,9 @@ public class Context extends IDisposable
      **/
     public IntSort getIntSort()
     {
-        if (m_intSort == null)
+        if (m_intSort == null) {
             m_intSort = new IntSort(this);
+        }
         return m_intSort;
     }
 
@@ -130,8 +132,9 @@ public class Context extends IDisposable
      **/
     public RealSort getRealSort()
     {
-        if (m_realSort == null)
+        if (m_realSort == null) {
             m_realSort = new RealSort(this);
+        }
         return m_realSort;
     }
 
@@ -148,8 +151,9 @@ public class Context extends IDisposable
      **/
     public SeqSort getStringSort()
     {
-        if (m_stringSort == null)
+        if (m_stringSort == null) {
             m_stringSort = mkStringSort();
+        }
         return m_stringSort;
     }
 
@@ -322,13 +326,6 @@ public class Context extends IDisposable
 
     /**
      * Create a datatype constructor. 
-     * @param name  
-     * @param recognizer  
-     * @param fieldNames  
-     * @param sorts  
-     * @param sortRefs 
-     * 
-     * @return
      **/
     public Constructor mkConstructor(String name, String recognizer,
             String[] fieldNames, Sort[] sorts, int[] sortRefs)
@@ -369,7 +366,7 @@ public class Context extends IDisposable
            
     {
         checkContextMatch(names);
-        int n = (int) names.length;
+        int n = names.length;
         ConstructorList[] cla = new ConstructorList[n];
         long[] n_constr = new long[n];
         for (int i = 0; i < n; i++)
@@ -391,10 +388,6 @@ public class Context extends IDisposable
 
     /**
      * Create mutually recursive data-types. 
-     * @param names  
-     * @param c 
-     * 
-     * @return
      **/
     public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
            
@@ -406,7 +399,7 @@ public class Context extends IDisposable
      * Update a datatype field at expression t with value v.
      * The function performs a record update at t. The field
      * that is passed in as argument is updated with value v,
-     * the remainig fields of t are unchanged.    
+     * the remaining fields of t are unchanged.
      **/
     public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
         throws Z3Exception
@@ -502,8 +495,8 @@ public class Context extends IDisposable
     /**
      * Creates a fresh constant function declaration with a name prefixed with
      * {@code prefix"}. 
-     * @see mkFuncDecl(String,Sort,Sort)
-     * @see mkFuncDecl(String,Sort[],Sort)
+     * @see #mkFuncDecl(String,Sort,Sort)
+     * @see #mkFuncDecl(String,Sort[],Sort)
      **/
     public FuncDecl mkFreshConstDecl(String prefix, Sort range)
            
@@ -1519,7 +1512,7 @@ public class Context extends IDisposable
     {
         checkContextMatch(t);
         return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
-                (signed) ? true : false));
+            (signed)));
     }
 
     /**
@@ -1533,8 +1526,7 @@ public class Context extends IDisposable
         checkContextMatch(t1);
         checkContextMatch(t2);
         return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
-                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
-                : false));
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
     }
 
     /**
@@ -1576,8 +1568,7 @@ public class Context extends IDisposable
         checkContextMatch(t1);
         checkContextMatch(t2);
         return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
-                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
-                : false));
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
     }
 
     /**
@@ -1617,8 +1608,7 @@ public class Context extends IDisposable
         checkContextMatch(t1);
         checkContextMatch(t2);
         return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
-                .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
-                : false));
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
     }
 
     /**
@@ -1662,8 +1652,8 @@ public class Context extends IDisposable
      * {@code [domain -> range]}, and {@code i} must have the sort
      * {@code domain}. The sort of the result is {@code range}.
      * 
-     * @see mkArraySort
-     * @see mkStore
+     * @see #mkArraySort
+     * @see #mkStore
 
      **/
     public Expr mkSelect(ArrayExpr a, Expr i)
@@ -1688,8 +1678,8 @@ public class Context extends IDisposable
      * {@code select}) on all indices except for {@code i}, where it
      * maps to {@code v} (and the {@code select} of {@code a}
      * with respect to {@code i} may be a different value). 
-     * @see mkArraySort 
-     * @see mkSelect
+     * @see #mkArraySort
+     * @see #mkSelect
 
      **/
     public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
@@ -1706,8 +1696,8 @@ public class Context extends IDisposable
      * Remarks:  The resulting term is an array, such
      * that a {@code select} on an arbitrary index produces the value
      * {@code v}. 
-     * @see mkArraySort
-     * @see mkSelect
+     * @see #mkArraySort
+     * @see #mkSelect
      * 
      **/
     public ArrayExpr mkConstArray(Sort domain, Expr v)
@@ -1720,15 +1710,15 @@ public class Context extends IDisposable
 
     /**
      * Maps f on the argument arrays.
-     * Remarks:  Eeach element of
+     * Remarks:  Each element of
      * {@code args} must be of an array sort
      * {@code [domain_i -> range_i]}. The function declaration
      * {@code f} must have type {@code  range_1 .. range_n -> range}.
      * {@code v} must have sort range. The sort of the result is
      * {@code [domain_i -> range]}. 
-     * @see mkArraySort
-     * @see mkSelect 
-     * @see mkStore
+     * @see #mkArraySort
+     * @see #mkSelect
+     * @see #mkStore
 
      **/
     public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
@@ -2121,12 +2111,13 @@ public class Context extends IDisposable
      * 
      * @return A Term with value {@code num}/{@code den}
      *         and sort Real 
-     * @see mkNumeral(String,Sort)
+     * @see #mkNumeral(String,Sort)
      **/
     public RatNum mkReal(int num, int den)
     {
-        if (den == 0)
+        if (den == 0) {
             throw new Z3Exception("Denominator is zero");
+        }
 
         return new RatNum(this, Native.mkReal(nCtx(), num, den));
     }
@@ -2256,7 +2247,7 @@ public class Context extends IDisposable
      * 'names' of the bound variables, and {@code body} is the body
      * of the quantifier. Quantifiers are associated with weights indicating the
      * importance of using the quantifier during instantiation.
-     * Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
+     * Note that the bound variables are de-Bruijn indices created using {@link #mkBound}.
      * Z3 applies the convention that the last element in {@code names} and 
      * {@code sorts} refers to the variable with index 0, the second to last element 
      * of {@code names} and {@code sorts} refers to the variable 
@@ -2286,7 +2277,7 @@ public class Context extends IDisposable
 
     /**
      * Creates an existential quantifier using de-Brujin indexed variables. 
-     * @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
+     * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
                                int weight, Pattern[] patterns, Expr[] noPatterns,
@@ -2383,7 +2374,7 @@ public class Context extends IDisposable
     {
 
         return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
-                attributes, (int) assumptions.length,
+                attributes, assumptions.length,
                 AST.arrayToNative(assumptions), formula.getNativeObject());
     }
 
@@ -2413,7 +2404,7 @@ public class Context extends IDisposable
 
     /**
      * Parse the given file using the SMT-LIB parser. 
-     * @see parseSMTLIBString
+     * @see #parseSMTLIBString
      **/
     public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
             Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
@@ -2527,7 +2518,7 @@ public class Context extends IDisposable
 
     /**
      * Parse the given string using the SMT-LIB2 parser. 
-     * @see parseSMTLIBString
+     * @see #parseSMTLIBString
      * 
      * @return A conjunction of assertions in the scope (up to push/pop) at the
      *         end of the string.
@@ -2541,8 +2532,9 @@ public class Context extends IDisposable
         int cs = Sort.arrayLength(sorts);
         int cdn = Symbol.arrayLength(declNames);
         int cd = AST.arrayLength(decls);
-        if (csn != cs || cdn != cd)
+        if (csn != cs || cdn != cd) {
             throw new Z3Exception("Argument size mismatch");
+        }
         return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
                 str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
                 AST.arrayToNative(sorts), AST.arrayLength(decls),
@@ -2551,13 +2543,12 @@ public class Context extends IDisposable
 
     /**
      * Parse the given file using the SMT-LIB2 parser. 
-     * @see parseSMTLIB2String
+     * @see #parseSMTLIB2String
      **/
     public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
             Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
            
     {
-
         int csn = Symbol.arrayLength(sortNames);
         int cs = Sort.arrayLength(sorts);
         int cdn = Symbol.arrayLength(declNames);
@@ -2648,9 +2639,10 @@ public class Context extends IDisposable
         if (ts != null && ts.length > 0)
         {
             last = ts[ts.length - 1].getNativeObject();
-            for (int i = ts.length - 2; i >= 0; i--)
+            for (int i = ts.length - 2; i >= 0; i--) {
                 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
-                        last);
+                    last);
+            }
         }
         if (last != 0)
         {
@@ -2664,7 +2656,7 @@ public class Context extends IDisposable
 
     /**
      * Create a tactic that applies {@code t1} to a Goal and then
-     * {@code t2"/> to every subgoal produced by <paramref name="t1}.
+     * {@code t2} to every subgoal produced by {@code t1}
      * 
      * Remarks:  Shorthand for {@code AndThen}. 
      **/
@@ -2999,7 +2991,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a new (incremental) solver. 
-     * @see mkSolver(Symbol)
+     * @see #mkSolver(Symbol)
      **/
     public Solver mkSolver(String logic)
     {
@@ -3839,7 +3831,7 @@ public class Context extends IDisposable
      * that is returned must be handled externally and through native calls (see
      * e.g., 
      * @see Native#incRef 
-     * @see wrapAST 
+     * @see #wrapAST
      * @param a The AST to unwrap.
      **/
     public long unwrapAST(AST a)
@@ -3878,7 +3870,7 @@ public class Context extends IDisposable
     }
 
     protected long m_ctx = 0;
-    protected static Object creation_lock = new Object();
+    protected static final Object creation_lock = new Object();
 
     long nCtx()
     {
@@ -4049,7 +4041,7 @@ public class Context extends IDisposable
         m_Params_DRQ.clear(this);
         m_Probe_DRQ.clear(this);
         m_Solver_DRQ.clear(this);
-	m_Optimize_DRQ.clear(this);
+        m_Optimize_DRQ.clear(this);
         m_Statistics_DRQ.clear(this);
         m_Tactic_DRQ.clear(this);
         m_Fixedpoint_DRQ.clear(this);
diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java
index d7896b15f..644d434d3 100644
--- a/src/api/java/DatatypeSort.java
+++ b/src/api/java/DatatypeSort.java
@@ -101,7 +101,7 @@ public class DatatypeSort extends Sort
            
     {
         super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
-                (int) constructors.length, arrayToNative(constructors)));
+                constructors.length, arrayToNative(constructors)));
 
     }
 };
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index da471f5ea..bb60eef56 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -98,7 +98,7 @@ public class EnumSort extends Sort
         long[] n_constdecls = new long[n];
         long[] n_testers = new long[n];
         setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
-                name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
+                name.getNativeObject(), n, Symbol.arrayToNative(enumNames),
                 n_constdecls, n_testers));        
     }
 };
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index e03d5b1c9..b24d3ac62 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -33,7 +33,6 @@ public class Expr extends AST
      * Returns a simplified version of the expression
      * @return Expr
      * @throws Z3Exception on error
-     * @return an Expr
      **/
     public Expr simplify()
     {
@@ -48,19 +47,20 @@ public class Expr extends AST
      * @see Context#SimplifyHelp
      * @return an Expr
      * @throws Z3Exception on error
-     * @return an Expr
      **/
     public Expr simplify(Params p)
     {
 
-        if (p == null)
+        if (p == null) {
             return Expr.create(getContext(),
-                    Native.simplify(getContext().nCtx(), getNativeObject()));
-        else
+                Native.simplify(getContext().nCtx(), getNativeObject()));
+        }
+        else {
             return Expr.create(
-                    getContext(),
-                    Native.simplifyEx(getContext().nCtx(), getNativeObject(),
-                            p.getNativeObject()));
+                getContext(),
+                Native.simplifyEx(getContext().nCtx(), getNativeObject(),
+                    p.getNativeObject()));
+        }
     }
 
     /**
@@ -106,9 +106,10 @@ public class Expr extends AST
     {
         int n = getNumArgs();
         Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
+        for (int i = 0; i < n; i++) {
             res[i] = Expr.create(getContext(),
-                    Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
+                Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
+        }
         return res;
     }
 
@@ -122,10 +123,11 @@ public class Expr extends AST
     public void update(Expr[] args)
     {
         getContext().checkContextMatch(args);
-        if (isApp() && args.length != getNumArgs())
+        if (isApp() && args.length != getNumArgs()) {
             throw new Z3Exception("Number of arguments does not match");
+        }
         setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
-                (int) args.length, Expr.arrayToNative(args)));
+                args.length, Expr.arrayToNative(args)));
     }
 
     /**
@@ -144,10 +146,11 @@ public class Expr extends AST
     {
         getContext().checkContextMatch(from);
         getContext().checkContextMatch(to);
-        if (from.length != to.length)
+        if (from.length != to.length) {
             throw new Z3Exception("Argument sizes do not match");
+        }
         return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
-                getNativeObject(), (int) from.length, Expr.arrayToNative(from),
+                getNativeObject(), from.length, Expr.arrayToNative(from),
                 Expr.arrayToNative(to)));
     }
 
@@ -160,7 +163,6 @@ public class Expr extends AST
      **/
     public Expr substitute(Expr from, Expr to)
     {
-
         return substitute(new Expr[] { from }, new Expr[] { to });
     }
 
@@ -179,7 +181,7 @@ public class Expr extends AST
 
         getContext().checkContextMatch(to);
         return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
-                getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
+                getNativeObject(), to.length, Expr.arrayToNative(to)));
     }
 
     /**
@@ -189,23 +191,23 @@ public class Expr extends AST
      * 
      * @return A copy of the term which is associated with {@code ctx}
      * @throws Z3Exception on error
-     * @return an Expr
      **/
     public Expr translate(Context ctx)
     {
-
-        if (getContext() == ctx)
+        if (getContext() == ctx) {
             return this;
-        else
+        } else {
             return Expr.create(
-                    ctx,
-                    Native.translate(getContext().nCtx(), getNativeObject(),
-                            ctx.nCtx()));
+                ctx,
+                Native.translate(getContext().nCtx(), getNativeObject(),
+                    ctx.nCtx()));
+        }
     }
 
     /**
      * Returns a string representation of the expression.
      **/
+    @Override
     public String toString()
     {
         return super.toString();
@@ -224,9 +226,8 @@ public class Expr extends AST
     /**
      * Indicates whether the term is well-sorted.
      * 
-     * @return True if the term is well-sorted, false otherwise.
      * @throws Z3Exception on error
-     * @return a boolean
+     * @return True if the term is well-sorted, false otherwise.
      **/
     public boolean isWellSorted()
     {
@@ -2038,7 +2039,7 @@ public class Expr extends AST
      * identity, but in the context of a register machine allows for terms of
      * kind {@code isRelationUnion} to perform destructive updates to
      * the first argument.
-     * @see isRelationUnion 
+     * @see #isRelationUnion
      * @throws Z3Exception on error
      * @return a boolean
      **/
@@ -2117,12 +2118,14 @@ public class Expr extends AST
         }
     }
 
+    @Override
     void checkNativeObject(long obj)
     {
         if (!Native.isApp(getContext().nCtx(), obj) && 
             Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
-            Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
+            Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
             throw new Z3Exception("Underlying object is not a term");
+        }
         super.checkNativeObject(obj);
     }
 
@@ -2186,10 +2189,10 @@ public class Expr extends AST
             return new FPRMExpr(ctx, obj);
         case Z3_FINITE_DOMAIN_SORT:
             return new FiniteDomainExpr(ctx, obj);
-	case Z3_SEQ_SORT:
-	    return new SeqExpr(ctx, obj);
-	case Z3_RE_SORT:
-	    return new ReExpr(ctx, obj);
+        case Z3_SEQ_SORT:
+            return new SeqExpr(ctx, obj);
+        case Z3_RE_SORT:
+            return new ReExpr(ctx, obj);
         default: ;
         }
 
diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java
index 79845c700..e53ed22b2 100644
--- a/src/api/java/FiniteDomainNum.java
+++ b/src/api/java/FiniteDomainNum.java
@@ -36,8 +36,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
     public int getInt()
     {
         Native.IntPtr res = new Native.IntPtr();
-        if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
             throw new Z3Exception("Numeral is not an int");
+        }
         return res.value;
     }
 
@@ -47,8 +48,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
     public long getInt64()
     {
         Native.LongPtr res = new Native.LongPtr();
-        if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
             throw new Z3Exception("Numeral is not an int64");
+        }
         return res.value;
     }
 
@@ -63,6 +65,7 @@ public class FiniteDomainNum extends FiniteDomainExpr
     /**
      * Returns a string representation of the numeral.
      **/
+    @Override
     public String toString()
     {
         try
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 0bdbfb571..14fb3a44a 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -164,7 +164,7 @@ public class Fixedpoint extends Z3Object
 
     /**
      * Creates a backtracking point. 
-     * @see pop
+     * @see #pop
      **/
     public void push()
     {
@@ -176,7 +176,7 @@ public class Fixedpoint extends Z3Object
      * Remarks: Note that an exception is thrown if {@code pop} 
      * is called without a corresponding {@code push}
      *  
-     * @see push
+     * @see #push
      **/
     public void pop()
     {
@@ -252,6 +252,7 @@ public class Fixedpoint extends Z3Object
     /**
      * Retrieve internal string representation of fixedpoint object.
      **/
+    @Override
     public String toString()
     {
         try
@@ -353,12 +354,14 @@ public class Fixedpoint extends Z3Object
         super(ctx, Native.mkFixedpoint(ctx.nCtx()));
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getFixedpointDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getFixedpointDRQ().add(o);
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index da2af3a41..e65538a30 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -29,6 +29,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index bc2baab91..301978c44 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -29,35 +29,22 @@ public class FuncDecl extends AST
     /**
      * Object comparison.
      **/
+    @Override
     public boolean equals(Object o)
     {
-        FuncDecl casted = null;
+        if (o == this) return true;
+        if (!(o instanceof FuncDecl)) return false;
+        FuncDecl other = (FuncDecl) o;
 
-        try {
-            casted = FuncDecl.class.cast(o);
-        } catch (ClassCastException e) {
-            return false;
-        }
-
-	return  
-	    (this == casted) || 
-	    (this != null) &&
-	    (casted != null) &&
-	    (getContext().nCtx() == casted.getContext().nCtx()) &&
-	    (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+        return
+            (getContext().nCtx() == other.getContext().nCtx()) &&
+            (Native.isEqFuncDecl(
+                getContext().nCtx(),
+                getNativeObject(),
+                other.getNativeObject()));
     }
 
-    /**
-     * A hash code.
-     **/
-    public int hashCode()
-    {
-        return super.hashCode();
-    }
-
-    /**
-     * A string representations of the function declaration.
-     **/
+    @Override
     public String toString()
     {
         try
@@ -72,6 +59,7 @@ public class FuncDecl extends AST
     /**
      * Returns a unique identifier for the function declaration.
      **/
+    @Override
     public int getId()
     {
         return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
@@ -87,7 +75,7 @@ public class FuncDecl extends AST
 
     /**
      * The size of the domain of the function declaration 
-     * @see getArity
+     * @see #getArity
      **/
     public int getDomainSize()
     {
@@ -370,9 +358,6 @@ public class FuncDecl extends AST
 
     /**
      * Create expression that applies function to arguments. 
-     * @param args 
-     * 
-     * @return
      **/
     public Expr apply(Expr ... args)
     {
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index 59a8a0398..72f6bb25d 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -70,6 +70,7 @@ public class FuncInterp extends Z3Object
         /**
          * A string representation of the function entry.
          **/
+        @Override
         public String toString()
         {
             try
@@ -82,7 +83,7 @@ public class FuncInterp extends Z3Object
                 return res + getValue() + "]";
             } catch (Z3Exception e)
             {
-                return new String("Z3Exception: " + e.getMessage());
+                return "Z3Exception: " + e.getMessage();
             }
         }
 
@@ -91,18 +92,20 @@ public class FuncInterp extends Z3Object
             super(ctx, obj);
         }
 
+        @Override
         void incRef(long o)
         {
             getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
             super.incRef(o);
         }
 
+        @Override
         void decRef(long o)
         {
             getContext().getFuncEntryDRQ().add(o);
             super.decRef(o);
         }
-    };
+    }
 
     /**
      * The number of entries in the function interpretation.
@@ -183,7 +186,7 @@ public class FuncInterp extends Z3Object
             return res;
         } catch (Z3Exception e)
         {
-            return new String("Z3Exception: " + e.getMessage());
+            return "Z3Exception: " + e.getMessage();
         }
     }
 
@@ -192,12 +195,14 @@ public class FuncInterp extends Z3Object
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getFuncInterpDRQ().add(o);
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index 56660d2f9..c888e9e3d 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -29,6 +29,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index 406c0b33a..7dfdaa27d 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -29,6 +29,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Global.java b/src/api/java/Global.java
index 67a051792..fb2bdf916 100644
--- a/src/api/java/Global.java
+++ b/src/api/java/Global.java
@@ -57,17 +57,18 @@ public final class Global
     public static String getParameter(String id)
     {
         Native.StringPtr res = new Native.StringPtr();
-        if (!Native.globalParamGet(id, res))
+        if (!Native.globalParamGet(id, res)) {
             return null;
-        else
+        } else {
             return res.value;
+        }
     }    
     
     /**
      * Restore the value of all global (and module) parameters.
      * Remarks: 
      * This command will not affect already created objects (such as tactics and solvers)
-     * @see setParameter
+     * @see #setParameter
      **/
     public static void resetParameters()
     {
@@ -83,7 +84,7 @@ public final class Global
     public static void ToggleWarningMessages(boolean enabled)
            
     {
-        Native.toggleWarningMessages((enabled) ? true : false);
+        Native.toggleWarningMessages((enabled));
     }
     
     /** 
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index 41d4e27ac..46b04f6bf 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -246,8 +246,8 @@ public class Goal extends Z3Object
     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),
+            (unsatCores), (proofs)));
     }
 
     void incRef(long o)
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index dd9d69414..be921241b 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -29,6 +29,7 @@ class GoalDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class GoalDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index 823288a20..1a99a3d92 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -21,7 +21,7 @@ import java.util.LinkedList;
 
 public abstract class IDecRefQueue
 {
-    protected Object m_lock = new Object();
+    protected final Object m_lock = new Object();
     protected LinkedList<Long> m_queue = new LinkedList<Long>();
     protected int m_move_limit;
 
diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java
index c3855c428..dae8a7262 100644
--- a/src/api/java/IDisposable.java
+++ b/src/api/java/IDisposable.java
@@ -19,9 +19,7 @@ Notes:
 
 package com.microsoft.z3;
 
-public class IDisposable
+public abstract class IDisposable
 {
-    public void dispose()
-    {
-    }
+    public abstract void dispose();
 }
diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java
index 4078b3db3..71d878311 100644
--- a/src/api/java/IntNum.java
+++ b/src/api/java/IntNum.java
@@ -36,7 +36,7 @@ public class IntNum extends IntExpr
     public int getInt()
     {
         Native.IntPtr res = new Native.IntPtr();
-        if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res))
             throw new Z3Exception("Numeral is not an int");
         return res.value;
     }
@@ -47,7 +47,7 @@ public class IntNum extends IntExpr
     public long getInt64()
     {
         Native.LongPtr res = new Native.LongPtr();
-        if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
+        if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res))
             throw new Z3Exception("Numeral is not an int64");
         return res.value;
     }
diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java
index db99e6840..fab242d28 100644
--- a/src/api/java/IntSymbol.java
+++ b/src/api/java/IntSymbol.java
@@ -46,6 +46,7 @@ public class IntSymbol extends Symbol
         super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
     }
 
+    @Override
     void checkNativeObject(long obj)
     {
         if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 17e5de2a2..0695d7cf1 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -92,7 +92,7 @@ public class Model extends Z3Object
                     return null;
                 else
                 {
-                    if (Native.isAsArray(getContext().nCtx(), n) ^ true)
+                    if (!Native.isAsArray(getContext().nCtx(), n))
                         throw new Z3Exception(
                                 "Argument was not an array constant");
                     long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
@@ -212,8 +212,8 @@ public class Model extends Z3Object
     public Expr eval(Expr t, boolean completion)
     {
         Native.LongPtr v = new Native.LongPtr();
-        if (Native.modelEval(getContext().nCtx(), getNativeObject(),
-                t.getNativeObject(), (completion) ? true : false, v) ^ true)
+        if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
+            t.getNativeObject(), (completion), v))
             throw new ModelEvaluationFailedException();
         else
             return Expr.create(getContext(), v.value);
@@ -244,8 +244,8 @@ public class Model extends Z3Object
      * in a formula. The interpretation for a sort is a finite set of distinct
      * values. We say this finite set is the "universe" of the sort. 
      * 
-     * @see getNumSorts
-     * @see getSortUniverse
+     * @see #getNumSorts
+     * @see #getSortUniverse
      * 
      * @throws Z3Exception
      **/
@@ -282,6 +282,7 @@ public class Model extends Z3Object
      * 
      * @return A string representation of the model.
      **/
+    @Override
     public String toString()
     {
         try
@@ -298,12 +299,14 @@ public class Model extends Z3Object
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getModelDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getModelDRQ().add(o);
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index c954a1fa8..b97add310 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -29,6 +29,7 @@ class ModelDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ModelDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index f12bb7e06..5dfe8fcf4 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -32,7 +32,7 @@ public class Optimize extends Z3Object
      **/
     public String getHelp()
     {
-	return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
+        return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
     }
 
     /**
@@ -42,7 +42,7 @@ public class Optimize extends Z3Object
      **/
     public void setParameters(Params value)
     {
-	Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
+        Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
     }
 
     /**
@@ -50,7 +50,7 @@ public class Optimize extends Z3Object
      **/
     public ParamDescrs getParameterDescriptions()
     {
-	return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject())); 
+        return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
     }
 
     /**
@@ -112,8 +112,9 @@ public class Optimize extends Z3Object
 
 	/**
 	 * Print a string representation of the handle.
-	 **/        	   	
-        public String toString() 
+	 **/
+    @Override
+    public String toString()
         {
             return getValue().toString();
         }
@@ -128,9 +129,9 @@ public class Optimize extends Z3Object
 
     public Handle AssertSoft(BoolExpr constraint, int weight, String group)
     {
-	getContext().checkContextMatch(constraint);
-	Symbol s = getContext().mkSymbol(group);
-	return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
+        getContext().checkContextMatch(constraint);
+        Symbol s = getContext().mkSymbol(group);
+        return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
     }
     
 
@@ -142,15 +143,15 @@ public class Optimize extends Z3Object
 
     public Status Check()
     {
-	Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
-	switch (r) {
-	case Z3_L_TRUE:
-	    return Status.SATISFIABLE;
-	case Z3_L_FALSE:
-	    return Status.UNSATISFIABLE;
-	default:
-	    return Status.UNKNOWN;
-	}
+        Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
+        switch (r) {
+            case Z3_L_TRUE:
+                return Status.SATISFIABLE;
+            case Z3_L_FALSE:
+                return Status.UNSATISFIABLE;
+            default:
+                return Status.UNKNOWN;
+        }
     }
     
     /**
@@ -158,7 +159,7 @@ public class Optimize extends Z3Object
      **/
     public void Push()
     {
-	Native.optimizePush(getContext().nCtx(), getNativeObject());
+        Native.optimizePush(getContext().nCtx(), getNativeObject());
     }
 
 
@@ -170,7 +171,7 @@ public class Optimize extends Z3Object
      
     public void Pop()
     {
-	Native.optimizePop(getContext().nCtx(), getNativeObject());
+        Native.optimizePop(getContext().nCtx(), getNativeObject());
     }
 
 
@@ -182,11 +183,12 @@ public class Optimize extends Z3Object
      **/
     public Model getModel()
     {
-	long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
-	if (x == 0)
-	    return null;
-	else
-	    return new Model(getContext(), x);
+        long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
+        if (x == 0) {
+            return null;
+        } else {
+            return new Model(getContext(), x);
+        }
     }
 
     /** 
@@ -196,7 +198,7 @@ public class Optimize extends Z3Object
      **/        	
     public Handle MkMaximize(ArithExpr e)
     {
-	return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
     
     /**
@@ -205,7 +207,7 @@ public class Optimize extends Z3Object
      **/        	
     public Handle MkMinimize(ArithExpr e)
     {
-	return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
     
     /**
@@ -213,7 +215,7 @@ public class Optimize extends Z3Object
      **/        	
     private ArithExpr GetLower(int index)
     {
-	return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
+        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
     }
     
     
@@ -222,7 +224,7 @@ public class Optimize extends Z3Object
      **/        	
     private ArithExpr GetUpper(int index)
     {
-	return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
+        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
@@ -237,10 +239,11 @@ public class Optimize extends Z3Object
     
     /**
      *  Print the context to a String (SMT-LIB parseable benchmark).
-     **/        	
+     **/
+    @Override
     public String toString()
     {
-	return Native.optimizeToString(getContext().nCtx(), getNativeObject());
+        return Native.optimizeToString(getContext().nCtx(), getNativeObject());
     }
     
     /**
@@ -248,27 +251,28 @@ public class Optimize extends Z3Object
      **/
     public Statistics getStatistics()
     {
-	return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
+        return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
     }
 
 
     Optimize(Context ctx, long obj) throws Z3Exception
     {
-	super(ctx, obj);
+        super(ctx, obj);
     }
 
     Optimize(Context ctx) throws Z3Exception
     {
-	super(ctx, Native.mkOptimize(ctx.nCtx()));
+        super(ctx, Native.mkOptimize(ctx.nCtx()));
     }
 
-    
+    @Override
     void incRef(long o)
     {
         getContext().getOptimizeDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getOptimizeDRQ().add(o);
diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java
index c9bc251e1..795a8a399 100644
--- a/src/api/java/OptimizeDecRefQueue.java
+++ b/src/api/java/OptimizeDecRefQueue.java
@@ -29,6 +29,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 514c65b46..9c6fbd0dc 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -72,6 +72,7 @@ public class ParamDescrs extends Z3Object
     /**
      * Retrieves a string representation of the ParamDescrs.
      **/
+    @Override
     public String toString()
     {
         try
@@ -88,12 +89,14 @@ public class ParamDescrs extends Z3Object
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getParamDescrsDRQ().add(o);
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index 95a92475e..e3515bff6 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -29,6 +29,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index c241ac8aa..25d009b12 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -29,7 +29,7 @@ public class Params extends Z3Object
     public void add(Symbol name, boolean value)
     {
         Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
-                name.getNativeObject(), (value) ? true : false);
+                name.getNativeObject(), (value));
     }
 
     /**
@@ -112,6 +112,7 @@ public class Params extends Z3Object
     /**
      * A string representation of the parameter set.
      **/
+    @Override
     public String toString()
     {
         try
@@ -128,12 +129,14 @@ public class Params extends Z3Object
         super(ctx, Native.mkParams(ctx.nCtx()));
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getParamsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getParamsDRQ().add(o);
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index 7b9f34c00..f989f8015 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -29,6 +29,7 @@ class ParamsDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ParamsDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index d51315abf..eb12b6448 100644
--- a/src/api/java/Pattern.java
+++ b/src/api/java/Pattern.java
@@ -50,6 +50,7 @@ public class Pattern extends AST
     /**
      * A string representation of the pattern.
      **/
+    @Override
     public String toString()
     {
         try
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index 625b41e09..bcaa76ce6 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -51,12 +51,14 @@ public class Probe extends Z3Object
         super(ctx, Native.mkProbe(ctx.nCtx(), name));
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getProbeDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getProbeDRQ().add(o);
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index e271bd949..368bd5bba 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -29,6 +29,7 @@ class ProbeDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -40,6 +41,7 @@ class ProbeDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index 08df1c1f5..1b425d3e4 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -163,15 +163,14 @@ public class Quantifier extends BoolExpr
 
         if (noPatterns == null && quantifierID == null && skolemID == null)
         {
-            setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
-                    : false, weight, AST.arrayLength(patterns), AST
+            setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
                     .arrayToNative(patterns), AST.arrayLength(sorts), AST
                     .arrayToNative(sorts), Symbol.arrayToNative(names), body
                     .getNativeObject()));
         } else
         {
-            setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), 
-            (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), 
+            setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
+                (isForall), weight, AST.getNativeObject(quantifierID),
              AST.getNativeObject(skolemID), 
              AST.arrayLength(patterns), AST.arrayToNative(patterns), 
              AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), 
@@ -195,13 +194,13 @@ public class Quantifier extends BoolExpr
         if (noPatterns == null && quantifierID == null && skolemID == null)
         {
             setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
-                    (isForall) ? true : false, weight, AST.arrayLength(bound),
+                isForall, weight, AST.arrayLength(bound),
                     AST.arrayToNative(bound), AST.arrayLength(patterns),
                     AST.arrayToNative(patterns), body.getNativeObject()));
         } else
         {
             setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
-                    (isForall) ? true : false, weight,
+                isForall, weight,
                     AST.getNativeObject(quantifierID),
                     AST.getNativeObject(skolemID), AST.arrayLength(bound),
                     AST.arrayToNative(bound), AST.arrayLength(patterns),
@@ -215,6 +214,7 @@ public class Quantifier extends BoolExpr
         super(ctx, obj);
     }
 
+    @Override
     void checkNativeObject(long obj)
     {
         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java
index 8fd815742..f44823a2b 100644
--- a/src/api/java/RatNum.java
+++ b/src/api/java/RatNum.java
@@ -74,6 +74,7 @@ public class RatNum extends RealExpr
     /**
      * Returns a string representation of the numeral.
      **/
+    @Override
     public String toString()
     {
         try
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 231326107..ea76637c8 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -57,8 +57,8 @@ public class Solver extends Z3Object
 
     /**
      * The current number of backtracking points (scopes). 
-     * @see pop 
-     * @see push
+     * @see #pop
+     * @see #push
      **/
     public int getNumScopes()
     {
@@ -68,7 +68,7 @@ public class Solver extends Z3Object
 
     /**
      * Creates a backtracking point. 
-     * @see pop
+     * @see #pop
      **/
     public void push()
     {
@@ -89,7 +89,7 @@ public class Solver extends Z3Object
      * Remarks: Note that
      * an exception is thrown if {@code n} is not smaller than
      * {@code NumScopes} 
-     * @see push
+     * @see #push
      **/
     public void pop(int n)
     {
@@ -139,12 +139,14 @@ public class Solver extends Z3Object
     {
         getContext().checkContextMatch(constraints);
         getContext().checkContextMatch(ps);
-        if (constraints.length != ps.length)
+        if (constraints.length != ps.length) {
             throw new Z3Exception("Argument size mismatch");
+        }
 
-        for (int i = 0; i < constraints.length; i++)
+        for (int i = 0; i < constraints.length; i++) {
             Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
-                    constraints[i].getNativeObject(), ps[i].getNativeObject());
+                constraints[i].getNativeObject(), ps[i].getNativeObject());
+        }
     }
 
     /** 
@@ -194,20 +196,21 @@ public class Solver extends Z3Object
     /**
      * Checks whether the assertions in the solver are consistent or not.
      * Remarks:  
-     * @see getModel
-     * @see getUnsatCore
-     * @see getProof 
+     * @see #getModel
+     * @see #getUnsatCore
+     * @see #getProof
      **/
     public Status check(Expr... assumptions)
     {
         Z3_lbool r;
-        if (assumptions == null)
+        if (assumptions == null) {
             r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
-                    getNativeObject()));
-        else
+                getNativeObject()));
+        } else {
             r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
-                    .nCtx(), getNativeObject(), (int) assumptions.length, AST
-                    .arrayToNative(assumptions)));
+                .nCtx(), getNativeObject(), assumptions.length, AST
+                .arrayToNative(assumptions)));
+        }
         switch (r)
         {
         case Z3_L_TRUE:
@@ -222,9 +225,9 @@ public class Solver extends Z3Object
     /**
      * Checks whether the assertions in the solver are consistent or not.
      * Remarks:  
-     * @see getModel
-     * @see getUnsatCore
-     * @see getProof 
+     * @see #getModel
+     * @see #getUnsatCore
+     * @see #getProof
      **/
     public Status check()
     {
@@ -243,10 +246,11 @@ public class Solver extends Z3Object
     public Model getModel()
     {
         long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
-        if (x == 0)
+        if (x == 0) {
             return null;
-        else
+        } else {
             return new Model(getContext(), x);
+        }
     }
 
     /**
@@ -261,10 +265,11 @@ public class Solver extends Z3Object
     public Expr getProof()
     {
         long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
-        if (x == 0)
+        if (x == 0) {
             return null;
-        else
+        } else {
             return Expr.create(getContext(), x);
+        }
     }
 
     /**
@@ -315,6 +320,7 @@ public class Solver extends Z3Object
     /**
      * A string representation of the solver.
      **/
+    @Override
     public String toString()
     {
         try
@@ -332,12 +338,14 @@ public class Solver extends Z3Object
         super(ctx, obj);
     }
 
+    @Override
     void incRef(long o)
     {
         getContext().getSolverDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
+    @Override
     void decRef(long o)
     {
         getContext().getSolverDRQ().add(o);
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index cbe5bbc3b..f4d5fb139 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -26,6 +26,7 @@ class SolverDecRefQueue extends IDecRefQueue
         super(move_limit);
     }
 
+    @Override
     protected void incRef(Context ctx, long obj)
     {
         try
@@ -37,6 +38,7 @@ class SolverDecRefQueue extends IDecRefQueue
         }
     }
 
+    @Override
     protected void decRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 1481a44e2..e30e0b8b3 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -27,25 +27,20 @@ public class Sort extends AST
 {
     /**
      * Equality operator for objects of type Sort. 
-     * @param o
-     * @return
      **/
+    @Override
     public boolean equals(Object o)
     {
-        Sort casted = null;
+        if (o == this) return true;
+        if (!(o instanceof Sort)) return false;
+        Sort other = (Sort) o;
 
-        try {
-            casted = Sort.class.cast(o);
-        } catch (ClassCastException e) {
-            return false;
-        }
-
-	return  
-	    (this == casted) || 
-	    (this != null) &&
-	    (casted != null) &&
-	    (getContext().nCtx() == casted.getContext().nCtx()) &&
-	    (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+	return  (getContext().nCtx() == other.getContext().nCtx()) &&
+	    (Native.isEqSort(
+            getContext().nCtx(),
+            getNativeObject(),
+            other.getNativeObject()
+        ));
     }
 
     /**
@@ -141,10 +136,10 @@ public class Sort extends AST
             return new FPSort(ctx, obj);
         case Z3_ROUNDING_MODE_SORT:
             return new FPRMSort(ctx, obj);
-	case Z3_SEQ_SORT:
-	    return new SeqSort(ctx, obj);
-	case Z3_RE_SORT:
-	    return new ReSort(ctx, obj);
+        case Z3_SEQ_SORT:
+            return new SeqSort(ctx, obj);
+        case Z3_RE_SORT:
+            return new ReSort(ctx, obj);
         default:
             throw new Z3Exception("Unknown sort kind");
         }
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index de5a52ebb..5af0cf863 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -72,12 +72,13 @@ public class Statistics extends Z3Object
          **/
         public String getValueString()
         {
-            if (isUInt())
+            if (isUInt()) {
                 return Integer.toString(m_int);
-            else if (isDouble())
+            } else if (isDouble()) {
                 return Double.toString(m_double);
-            else
+            } else {
                 throw new Z3Exception("Unknown statistical entry type");
+            }
         }
 
         /**
@@ -90,7 +91,7 @@ public class Statistics extends Z3Object
                 return Key + ": " + getValueString();
             } catch (Z3Exception e)
             {
-                return new String("Z3Exception: " + e.getMessage());
+                return "Z3Exception: " + e.getMessage();
             }
         }
 
@@ -150,14 +151,15 @@ public class Statistics extends Z3Object
         {
             Entry e;
             String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
-            if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i))
+            if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) {
                 e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
-                        getNativeObject(), i));
-            else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i))
+                    getNativeObject(), i));
+            } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
                 e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
-                        getNativeObject(), i));
-            else
+                    getNativeObject(), i));
+            } else {
                 throw new Z3Exception("Unknown data entry value");
+            }
             res[i] = e;
         }
         return res;
@@ -186,9 +188,11 @@ public class Statistics extends Z3Object
     {
         int n = size();
         Entry[] es = getEntries();
-        for (int i = 0; i < n; i++)
-            if (es[i].Key == key)
+        for (int i = 0; i < n; i++) {
+            if (es[i].Key.equals(key)) {
                 return es[i];
+            }
+        }
         return null;
     }
 
diff --git a/src/api/java/Status.java b/src/api/java/Status.java
index a08f47909..c1f534d6a 100644
--- a/src/api/java/Status.java
+++ b/src/api/java/Status.java
@@ -38,7 +38,7 @@ public enum Status
         this.intValue = v;
     }
 
-    public static final Status fromInt(int v)
+    public static Status fromInt(int v)
     {
         for (Status k : values())
             if (k.intValue == v)
diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java
index efbd3a9d2..8470e1cd4 100644
--- a/src/api/java/StringSymbol.java
+++ b/src/api/java/StringSymbol.java
@@ -44,6 +44,7 @@ public class StringSymbol extends Symbol
         super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
     }
 
+    @Override
     void checkNativeObject(long obj)
     {
         if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java
index 44c08e572..beeaebb69 100644
--- a/src/api/java/Symbol.java
+++ b/src/api/java/Symbol.java
@@ -49,22 +49,19 @@ public class Symbol extends Z3Object
         return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
     }
 
+    @Override
     public boolean equals(Object o)
     {
-        Symbol casted = null;
-        try {
-	    casted = Symbol.class.cast(o);
-        }
-        catch (ClassCastException e) {
-            return false;
-        }
-
-        return this.getNativeObject() == casted.getNativeObject();
+        if (o == this) return true;
+        if (!(o instanceof Symbol)) return false;
+        Symbol other = (Symbol) o;
+        return this.getNativeObject() == other.getNativeObject();
     }
 
     /**
      * A string representation of the symbol.
      **/
+    @Override
     public String toString()
     {
         try
@@ -74,11 +71,10 @@ public class Symbol extends Z3Object
             else if (isStringSymbol())
                 return ((StringSymbol) this).getString();
             else
-                return new String(
-                        "Z3Exception: Unknown symbol kind encountered.");
+                return "Z3Exception: Unknown symbol kind encountered.";
         } catch (Z3Exception ex)
         {
-            return new String("Z3Exception: " + ex.getMessage());
+            return "Z3Exception: " + ex.getMessage();
         }
     }
 
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 574a2820c..dc1feecbf 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -31,11 +31,7 @@ public class Z3Object extends IDisposable
     {
         try {
             dispose();            
-        }
-        catch (Throwable t) {
-            throw t;
-        }
-        finally {
+        } finally {
             super.finalize();
         }
     }