Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/java/AST.java

@@ -29,21 +29,14 @@ public class AST extends Z3Object implements Comparable<AST>
      * 
      * @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
+        return
-        {
-            casted = AST.class.cast(o);
-        } catch (ClassCastException e)
-        {
-            return false;
-        }
-
-        return  (this == casted) ||
-                (this != null) &&
-                (casted != null) &&
             (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 Integer.compare(getId(), other.getId());
-            return -1;
-        else if (getId() > other.getId())
-            return +1;
-        else
-            return 0;
     }
 
     /**
@@ -74,14 +63,10 @@ public class AST extends Z3Object implements Comparable<AST>
      * 
      * @return A hash code
      **/
+    @Override
     public int hashCode()
     {
-        int r = 0;
+        return Native.getAstHash(getContext().nCtx(), getNativeObject());
-        try {
-            Native.getAstHash(getContext().nCtx(), getNativeObject());
-        }
-        catch (Z3Exception ex) {}
-        return r;
     }
 
     /**
@@ -103,12 +88,13 @@ 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()));
         }
+    }
 
     /**
      * The kind of the AST.
@@ -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()");

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

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);

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);

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);

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

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

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

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

src/api/java/Constructor.java

@@ -87,11 +87,7 @@ public class Constructor extends Z3Object
     {
         try {
             Native.delConstructor(getContext().nCtx(), getNativeObject());
-        }
+        } finally {
-        catch (Throwable t) {
-            throw t;
-        }
-        finally {
             super.finalize();
         }
     }

src/api/java/ConstructorList.java

@@ -31,11 +31,7 @@ public class ConstructorList extends Z3Object
     {
         try {        
             Native.delConstructorList(getContext().nCtx(), getNativeObject());            
-        }
+        } finally {
-        catch (Throwable t) {
-            throw t;
-        }
-        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)));
     }
 }

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
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
-                : false));
     }
 
     /**
@@ -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
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
-                : false));
     }
 
     /**
@@ -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
+                .getNativeObject(), t2.getNativeObject(), (isSigned)));
-                : false));
     }
 
     /**
@@ -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 #mkArraySort
-     * @see mkStore
+     * @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 #mkArraySort
-     * @see mkSelect
+     * @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 #mkArraySort
-     * @see mkSelect
+     * @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 #mkArraySort
-     * @see mkSelect 
+     * @see #mkSelect
-     * @see mkStore
+     * @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,10 +2639,11 @@ 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);
             }
+        }
         if (last != 0)
         {
             last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
@@ -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()
     {

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)));
 
     }
 };

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));        
     }
 };

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,20 +47,21 @@ 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
+        }
+        else {
             return Expr.create(
                 getContext(),
                 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
                     p.getNativeObject()));
         }
+    }
 
     /**
      * The function declaration of the function that is applied in this
@@ -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));
+        }
         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()));
         }
+    }
 
     /**
      * 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);
     }
 

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

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);

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

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;
-        try {
+        FuncDecl other = (FuncDecl) o;
-            casted = FuncDecl.class.cast(o);
-        } catch (ClassCastException e) {
-            return false;
-        }
 
         return
-	    (this == casted) || 
+            (getContext().nCtx() == other.getContext().nCtx()) &&
-	    (this != null) &&
+            (Native.isEqFuncDecl(
-	    (casted != null) &&
+                getContext().nCtx(),
-	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+                getNativeObject(),
-	    (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+                other.getNativeObject()));
     }
 
-    /**
+    @Override
-     * A hash code.
-     **/
-    public int hashCode()
-    {
-        return super.hashCode();
-    }
-
-    /**
-     * A string representations of the function declaration.
-     **/
     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)
     {

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);

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

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

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));
     }
     
     /** 

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,
+        super(ctx, Native.mkGoal(ctx.nCtx(), (models),
-                (unsatCores) ? true : false, (proofs) ? true : false));
+            (unsatCores), (proofs)));
     }
 
     void incRef(long o)

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

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;
 

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();
-    {
-    }
 }

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;
     }

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

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(),
+        if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
-                t.getNativeObject(), (completion) ? true : false, v) ^ true)
+            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 #getNumSorts
-     * @see getSortUniverse
+     * @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);

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

src/api/java/Optimize.java

@@ -113,6 +113,7 @@ public class Optimize extends Z3Object
 	/**
 	 * Print a string representation of the handle.
 	 **/
+    @Override
     public String toString()
         {
             return getValue().toString();
@@ -183,11 +184,12 @@ public class Optimize extends Z3Object
     public Model getModel()
     {
         long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
-	if (x == 0)
+        if (x == 0) {
             return null;
-	else
+        } else {
             return new Model(getContext(), x);
         }
+    }
 
     /** 
      *  Declare an arithmetical maximization objective.
@@ -238,6 +240,7 @@ 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());
@@ -262,13 +265,14 @@ public class Optimize extends Z3Object
         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);

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

src/api/java/ParamDescrs.java

@@ -81,6 +81,7 @@ public class ParamDescrs extends Z3Object
     /**
      * Retrieves a string representation of the ParamDescrs.
      **/
+    @Override
     public String toString()
     {
         try
@@ -97,12 +98,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);

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

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);

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

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

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);

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

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
+            setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
-                    : false, 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), 
+                (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

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

src/api/java/Solver.java

@@ -57,8 +57,8 @@ public class Solver extends Z3Object
 
     /**
      * The current number of backtracking points (scopes). 
-     * @see pop 
+     * @see #pop
-     * @see push
+     * @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,13 +139,15 @@ 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());
         }
+    }
 
     /** 
      * Assert a constraint into the solver, and track it (in the unsat) core
@@ -194,20 +196,21 @@ public class Solver extends Z3Object
     /**
      * Checks whether the assertions in the solver are consistent or not.
      * Remarks:  
-     * @see getModel
+     * @see #getModel
-     * @see getUnsatCore
+     * @see #getUnsatCore
-     * @see getProof 
+     * @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
+        } else {
             r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
-                    .nCtx(), getNativeObject(), (int) assumptions.length, AST
+                .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 #getModel
-     * @see getUnsatCore
+     * @see #getUnsatCore
-     * @see getProof 
+     * @see #getProof
      **/
     public Status check()
     {
@@ -243,11 +246,12 @@ 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);
         }
+    }
 
     /**
      * The proof of the last {@code Check}.
@@ -261,11 +265,12 @@ 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);
         }
+    }
 
     /**
      * The unsat core of the last {@code Check}.
@@ -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);

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

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 {
+	return  (getContext().nCtx() == other.getContext().nCtx()) &&
-            casted = Sort.class.cast(o);
+	    (Native.isEqSort(
-        } catch (ClassCastException e) {
+            getContext().nCtx(),
-            return false;
+            getNativeObject(),
-        }
+            other.getNativeObject()
-
+        ));
-	return  
-	    (this == casted) || 
-	    (this != null) &&
-	    (casted != null) &&
-	    (getContext().nCtx() == casted.getContext().nCtx()) &&
-	    (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
     /**

src/api/java/Statistics.java

@@ -72,13 +72,14 @@ 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");
             }
+        }
 
         /**
          * The string representation of the Entry.
@@ -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))
+            } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
                 e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
                     getNativeObject(), i));
-            else
+            } 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++)
+        for (int i = 0; i < n; i++) {
-            if (es[i].Key == key)
+            if (es[i].Key.equals(key)) {
                 return es[i];
+            }
+        }
         return null;
     }
 

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)

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

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;
+        if (o == this) return true;
-        try {
+        if (!(o instanceof Symbol)) return false;
-	    casted = Symbol.class.cast(o);
+        Symbol other = (Symbol) o;
-        }
+        return this.getNativeObject() == other.getNativeObject();
-        catch (ClassCastException e) {
-            return false;
-        }
-
-        return this.getNativeObject() == casted.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(
+                return "Z3Exception: Unknown symbol kind encountered.";
-                        "Z3Exception: Unknown symbol kind encountered.");
         } catch (Z3Exception ex)
         {
-            return new String("Z3Exception: " + ex.getMessage());
+            return "Z3Exception: " + ex.getMessage();
         }
     }
 

src/api/java/Z3Object.java

@@ -31,11 +31,7 @@ public class Z3Object extends IDisposable
     {
         try {
             dispose();            
-        }
+        } finally {
-        catch (Throwable t) {
-            throw t;
-        }
-        finally {
             super.finalize();
         }
     }

src/util/hwf.cpp

@@ -29,7 +29,8 @@ Revision History:
 #include<fenv.h>
 #endif
 
-#ifndef _M_IA64
+#if defined(__x86_64__) || defined(_M_X64) ||	\
+    defined(__i386) || defined(_M_IX86)
 #define USE_INTRINSICS
 #endif
 
@@ -47,7 +48,9 @@ Revision History:
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
 #ifdef __clang__
 #undef USE_INTRINSICS
-#else
+#endif
+
+#ifdef USE_INTRINSICS
 #include <emmintrin.h>
 #endif