diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index af8662700..64e4015e0 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -2169,8 +2169,8 @@ class JavaExample
         FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */
         FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */
         System.out.println("x=" + x.toString()  + 
-        				   "; y=" + y.toString() + 
-        				   "; z=" + z.toString());
+                           "; y=" + y.toString() + 
+                           "; z=" + z.toString());
         
         BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z));
         check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE);
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 94baea35a..3c3a960df 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -4399,16 +4399,16 @@ namespace Microsoft.Z3
         readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
         readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
         readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
-        readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue();
-        readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue();
+        readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
+        readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
         readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
         readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
-        readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue();
-        readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue();
-        readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue();
+        readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
+        readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
+        readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
         readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
         readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
-        readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue();
+        readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
         readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
 
         internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 0cdfd025c..fdb1643a5 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -29,7 +29,7 @@ public class AST extends Z3Object
     /**
      * Object comparison.
      * 
-	 * @param o another AST
+     * @param o another AST
      **/    
     public boolean equals(Object o)
     {
@@ -48,7 +48,7 @@ public class AST extends Z3Object
 
     /**
      * Object Comparison. 
-	 * @param other Another AST
+     * @param other Another AST
      * 
      * @return Negative if the object should be sorted before {@code other}, 
      * positive if after else zero.
@@ -102,7 +102,7 @@ public class AST extends Z3Object
 
     /**
      * Translates (copies) the AST to the Context {@code ctx}. 
-	 * @param ctx A context
+     * @param ctx A context
      * 
      * @return A copy of the AST which is associated with {@code ctx}
      * @throws Z3Exception on error
@@ -130,7 +130,7 @@ public class AST extends Z3Object
     /**
      * Indicates whether the AST is an Expr
      * @throws Z3Exception on error
-	 * @throws Z3Exception on error
+     * @throws Z3Exception on error
      **/
     public boolean isExpr() throws Z3Exception
     {
@@ -148,7 +148,7 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is an application
-	 * @return a boolean
+     * @return a boolean
      * @throws Z3Exception on error
      **/
     public boolean isApp() throws Z3Exception
@@ -158,7 +158,7 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is a BoundVariable.
-	 * @return a boolean
+     * @return a boolean
      * @throws Z3Exception on error
      **/
     public boolean isVar() throws Z3Exception
@@ -168,7 +168,7 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is a Quantifier
-	 * @return a boolean
+     * @return a boolean
      * @throws Z3Exception on error
      **/
     public boolean isQuantifier() throws Z3Exception
@@ -228,7 +228,7 @@ public class AST extends Z3Object
     {
         // Console.WriteLine("AST IncRef()");
         if (getContext() == null || o == 0)
-			return;
+            return;
         getContext().ast_DRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
@@ -237,7 +237,7 @@ public class AST extends Z3Object
     {
         // Console.WriteLine("AST DecRef()");
         if (getContext() == null || o == 0)
-			return;
+            return;
         getContext().ast_DRQ().add(o);
         super.decRef(o);
     }
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index 6ae84eb41..a8ee83e57 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ASTDecRefQueue extends IDecRefQueue
 {
+    public ASTDecRefQueue() 
+    {
+        super();
+    }
+
+    public ASTDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index 3d63939ca..96ddfbf76 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -24,7 +24,7 @@ class ASTMap extends Z3Object
 {
     /**
      * Checks whether the map contains the key {@code k}. 
-	 * @param k An AST
+     * @param k An AST
      * 
      * @return True if {@code k} is a key in the map, false
      *         otherwise.
@@ -40,7 +40,7 @@ class ASTMap extends Z3Object
      * Finds the value associated with the key {@code k}. 
      * Remarks: This function signs an error when {@code k} is not a key in
      * the map. 
-	 * @param k An AST
+     * @param k An AST
      * 
      * @throws Z3Exception
      **/
@@ -52,8 +52,8 @@ class ASTMap extends Z3Object
 
     /**
      * Stores or replaces a new key/value pair in the map. 
-	 * @param k The key AST
-	 * @param v The value AST
+     * @param k The key AST
+     * @param v The value AST
      **/
     public void insert(AST k, AST v) throws Z3Exception
     {
@@ -64,7 +64,7 @@ class ASTMap extends Z3Object
 
     /**
      * Erases the key {@code k} from the map. 
-	 * @param k An AST
+     * @param k An AST
      **/
     public void erase(AST k) throws Z3Exception
     {
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index d4df02244..30c96e2e7 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -34,7 +34,7 @@ class ASTVector extends Z3Object
      * Retrieves the i-th object in the vector.
      * Remarks: May throw an {@code IndexOutOfBoundsException} when 
      * {@code i} is out of range. 
-	 * @param i Index
+     * @param i Index
      * 
      * @return An AST
      * @throws Z3Exception
@@ -54,7 +54,7 @@ class ASTVector extends Z3Object
 
     /**
      * Resize the vector to {@code newSize}. 
-	 * @param newSize The new size of the vector.
+     * @param newSize The new size of the vector.
      **/
     public void resize(int newSize) throws Z3Exception
     {
@@ -64,7 +64,7 @@ class ASTVector extends Z3Object
     /**
      * Add the AST {@code a} to the back of the vector. The size is
      * increased by 1. 
-	 * @param a An AST
+     * @param a An AST
      **/
     public void push(AST a) throws Z3Exception
     {
@@ -73,7 +73,7 @@ class ASTVector extends Z3Object
 
     /**
      * Translates all ASTs in the vector to {@code ctx}. 
-	 * @param ctx A context
+     * @param ctx A context
      * 
      * @return A new ASTVector
      * @throws Z3Exception
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index 78f74d6cc..4cdf312fe 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ApplyResultDecRefQueue extends IDecRefQueue
 {
+    public ApplyResultDecRefQueue() 
+    {
+        super();
+    }
+
+    public ApplyResultDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java
index 996b98afc..240518134 100644
--- a/src/api/java/ArithExpr.java
+++ b/src/api/java/ArithExpr.java
@@ -22,11 +22,11 @@ package com.microsoft.z3;
  **/
 public class ArithExpr extends Expr
 {
-	/**
-	 * Constructor for ArithExpr
-	 **/
-	ArithExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for ArithExpr
+     **/
+    ArithExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/ArithSort.java b/src/api/java/ArithSort.java
index 2346d9b74..848d23554 100644
--- a/src/api/java/ArithSort.java
+++ b/src/api/java/ArithSort.java
@@ -22,8 +22,8 @@ package com.microsoft.z3;
  **/
 public class ArithSort extends Sort
 {
-	ArithSort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    ArithSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 };
diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java
index 154a56af4..4e6d9ed4d 100644
--- a/src/api/java/ArrayExpr.java
+++ b/src/api/java/ArrayExpr.java
@@ -23,11 +23,11 @@ package com.microsoft.z3;
  **/
 public class ArrayExpr extends Expr
 {
-	/**
-	 * Constructor for ArrayExpr
-	 **/
-	ArrayExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for ArrayExpr
+     **/
+    ArrayExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java
index ab545b7c1..a5b52a8f5 100644
--- a/src/api/java/ArraySort.java
+++ b/src/api/java/ArraySort.java
@@ -22,38 +22,38 @@ package com.microsoft.z3;
  **/
 public class ArraySort extends Sort
 {
-	/**
-	 * The domain of the array sort.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 * @return a sort
-	 **/
-	public Sort getDomain() throws Z3Exception
-	{
-		return Sort.create(getContext(),
-				Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
-	}
+    /**
+     * The domain of the array sort.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     * @return a sort
+     **/
+    public Sort getDomain() throws Z3Exception
+    {
+        return Sort.create(getContext(),
+                Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
+    }
 
-	/**
-	 * The range of the array sort.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 * @return a sort
-	 **/
-	public Sort getRange() throws Z3Exception
-	{
-		return Sort.create(getContext(),
-				Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
-	}
+    /**
+     * The range of the array sort.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     * @return a sort
+     **/
+    public Sort getRange() throws Z3Exception
+    {
+        return Sort.create(getContext(),
+                Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
+    }
 
-	ArraySort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    ArraySort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	ArraySort(Context ctx, Sort domain, Sort range) throws Z3Exception
-	{
-		super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
-				range.getNativeObject()));
-	}
+    ArraySort(Context ctx, Sort domain, Sort range) throws Z3Exception
+    {
+        super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
+                range.getNativeObject()));
+    }
 };
diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java
index a4e02d29f..2106ff0c2 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ASTMapDecRefQueue extends IDecRefQueue
 {
+    public ASTMapDecRefQueue() 
+    {
+        super();
+    }
+
+    public ASTMapDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index e0c7988a9..698e9e06b 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ASTVectorDecRefQueue extends IDecRefQueue
 {
+    public ASTVectorDecRefQueue() 
+    {
+        super();
+    }
+
+    public ASTVectorDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java
index 69a97de40..926a26b25 100644
--- a/src/api/java/BitVecExpr.java
+++ b/src/api/java/BitVecExpr.java
@@ -23,22 +23,22 @@ package com.microsoft.z3;
 public class BitVecExpr extends Expr
 {
 
-	/**
-	 * The size of the sort of a bit-vector term.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getSortSize() throws Z3Exception
-	{
-		return ((BitVecSort) getSort()).getSize();
-	}
+    /**
+     * The size of the sort of a bit-vector term.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getSortSize() throws Z3Exception
+    {
+        return ((BitVecSort) getSort()).getSize();
+    }
 
-	/**
-	 * Constructor for BitVecExpr
-	 **/
-	BitVecExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for BitVecExpr
+     **/
+    BitVecExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/BitVecSort.java b/src/api/java/BitVecSort.java
index 69d74151c..7fd644acb 100644
--- a/src/api/java/BitVecSort.java
+++ b/src/api/java/BitVecSort.java
@@ -22,18 +22,18 @@ package com.microsoft.z3;
  **/
 public class BitVecSort extends Sort
 {
-	/**
-	 * The size of the bit-vector sort.
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getSize() throws Z3Exception
-	{
-		return Native.getBvSortSize(getContext().nCtx(), getNativeObject());
-	}
+    /**
+     * The size of the bit-vector sort.
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getSize() throws Z3Exception
+    {
+        return Native.getBvSortSize(getContext().nCtx(), getNativeObject());
+    }
 
-	BitVecSort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    BitVecSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 };
diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java
index ea3cdbfb4..6709e2ae9 100644
--- a/src/api/java/BoolExpr.java
+++ b/src/api/java/BoolExpr.java
@@ -22,21 +22,21 @@ package com.microsoft.z3;
  **/
 public class BoolExpr extends Expr
 {
-	/**
-	 * Constructor for BoolExpr
-	 **/
-	protected BoolExpr(Context ctx)
-	{
-		super(ctx);
-	}
+    /**
+     * Constructor for BoolExpr
+     **/
+    protected BoolExpr(Context ctx)
+    {
+        super(ctx);
+    }
 
-	/**
-	 * Constructor for BoolExpr
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 **/
-	BoolExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for BoolExpr
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     **/
+    BoolExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index a5440092c..95e7799e1 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -22,53 +22,53 @@ package com.microsoft.z3;
  **/
 public class Constructor extends Z3Object
 {
-	/**
-	 * The number of fields of the constructor.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getNumFields() throws Z3Exception
-	{	
-		return n;
-	}
+    /**
+     * The number of fields of the constructor.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getNumFields() throws Z3Exception
+    {    
+        return n;
+    }
 
-	/**
-	 * The function declaration of the constructor.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl ConstructorDecl() throws Z3Exception
-	{
-	    Native.LongPtr constructor = new Native.LongPtr();
-	    Native.LongPtr tester = new Native.LongPtr();
-	    long[] accessors = new long[n];
+    /**
+     * The function declaration of the constructor.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl ConstructorDecl() throws Z3Exception
+    {
+        Native.LongPtr constructor = new Native.LongPtr();
+        Native.LongPtr tester = new Native.LongPtr();
+        long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
         return new FuncDecl(getContext(), constructor.value);         
-	}
+    }
 
-	/**
-	 * The function declaration of the tester.
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl getTesterDecl() throws Z3Exception
-	{
-	    Native.LongPtr constructor = new Native.LongPtr();
+    /**
+     * The function declaration of the tester.
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl getTesterDecl() throws Z3Exception
+    {
+        Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
         long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
         return new FuncDecl(getContext(), tester.value);
-	}
+    }
 
-	/**
-	 * The function declarations of the accessors
-	 * @throws Z3Exception 
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[] getAccessorDecls() throws Z3Exception
-	{
-	    Native.LongPtr constructor = new Native.LongPtr();
+    /**
+     * The function declarations of the accessors
+     * @throws Z3Exception 
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[] getAccessorDecls() throws Z3Exception
+    {
+        Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
         long[] accessors = new long[n];
         Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
@@ -76,40 +76,40 @@ public class Constructor extends Z3Object
         for (int i = 0; i < n; i++)
             t[i] = new FuncDecl(getContext(), accessors[i]); 
         return t;
-	}
+    }
 
-	/**
-	 * Destructor.
-	 * @throws Z3Exception on error
-	 **/
-	protected void finalize() throws Z3Exception
-	{
-		Native.delConstructor(getContext().nCtx(), getNativeObject());
-	}
+    /**
+     * Destructor.
+     * @throws Z3Exception on error
+     **/
+    protected void finalize() throws Z3Exception
+    {
+        Native.delConstructor(getContext().nCtx(), getNativeObject());
+    }
 
-	private int n = 0;
+    private int n = 0;
 
-	Constructor(Context ctx, Symbol name, Symbol recognizer,
-			Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
-			throws Z3Exception
-	{
-		super(ctx);
+    Constructor(Context ctx, Symbol name, Symbol recognizer,
+            Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
+            throws Z3Exception
+    {
+        super(ctx);
 
-		n = AST.arrayLength(fieldNames);
+        n = AST.arrayLength(fieldNames);
 
-		if (n != AST.arrayLength(sorts))
-			throw new Z3Exception(
-					"Number of field names does not match number of sorts");
-		if (sortRefs != null && sortRefs.length != n)
-			throw new Z3Exception(
-					"Number of field names does not match number of sort refs");
+        if (n != AST.arrayLength(sorts))
+            throw new Z3Exception(
+                    "Number of field names does not match number of sorts");
+        if (sortRefs != null && sortRefs.length != n)
+            throw new Z3Exception(
+                    "Number of field names does not match number of sort refs");
 
-		if (sortRefs == null)
-			sortRefs = new int[n];
+        if (sortRefs == null)
+            sortRefs = new int[n];
 
-		setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
-				recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
-				Sort.arrayToNative(sorts), sortRefs));
+        setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
+                recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
+                Sort.arrayToNative(sorts), sortRefs));
 
-	}
+    }
 }
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index b38678b8a..0cff4cfa4 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -22,26 +22,26 @@ package com.microsoft.z3;
  **/
 public class ConstructorList extends Z3Object
 {
-	/**
-	 * Destructor.
-	 * @throws Z3Exception on error
-	 **/
-	protected void finalize() throws Z3Exception
-	{
-		Native.delConstructorList(getContext().nCtx(), getNativeObject());
-	}
+    /**
+     * Destructor.
+     * @throws Z3Exception on error
+     **/
+    protected void finalize() throws Z3Exception
+    {
+        Native.delConstructorList(getContext().nCtx(), getNativeObject());
+    }
 
-	ConstructorList(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    ConstructorList(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	ConstructorList(Context ctx, Constructor[] constructors) throws Z3Exception
-	{
-		super(ctx);
+    ConstructorList(Context ctx, Constructor[] constructors) throws Z3Exception
+    {
+        super(ctx);
 
-		setNativeObject(Native.mkConstructorList(getContext().nCtx(),
-				(int) constructors.length,
-				Constructor.arrayToNative(constructors)));
-	}
+        setNativeObject(Native.mkConstructorList(getContext().nCtx(),
+                (int) constructors.length,
+                Constructor.arrayToNative(constructors)));
+    }
 }
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 294826f55..42fd0f7e1 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -261,12 +261,12 @@ public class Context extends IDisposable
 
     /**
      * Create a datatype constructor. 
-	 * @param name constructor name 
-	 * @param recognizer name of recognizer function. 
-	 * @param fieldNames names of the constructor fields. 
-	 * @param sorts field sorts, 0 if the field sort refers to a recursive sort. 
-	 * @param sortRefs reference to datatype sort that is an argument to the 
-	 * constructor; if the corresponding sort reference is 0, then the value in sort_refs should be
+     * @param name constructor name 
+     * @param recognizer name of recognizer function. 
+     * @param fieldNames names of the constructor fields. 
+     * @param sorts field sorts, 0 if the field sort refers to a recursive sort. 
+     * @param sortRefs reference to datatype sort that is an argument to the 
+     * constructor; if the corresponding sort reference is 0, then the value in sort_refs should be
      * an index referring to one of the recursive datatypes that is
      * declared.
      **/
@@ -281,11 +281,11 @@ public class Context extends IDisposable
 
     /**
      * Create a datatype constructor. 
-	 * @param name  
-	 * @param recognizer  
-	 * @param fieldNames  
-	 * @param sorts  
-	 * @param sortRefs 
+     * @param name  
+     * @param recognizer  
+     * @param fieldNames  
+     * @param sorts  
+     * @param sortRefs 
      * 
      * @return
      **/
@@ -321,8 +321,8 @@ public class Context extends IDisposable
 
     /**
      * Create mutually recursive datatypes. 
-	 * @param names names of datatype sorts 
-	 * @param c list of constructors, one list per sort.
+     * @param names names of datatype sorts 
+     * @param c list of constructors, one list per sort.
      **/
     public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
             throws Z3Exception
@@ -350,8 +350,8 @@ public class Context extends IDisposable
 
     /**
      * Create mutually recursive data-types. 
-	 * @param names  
-	 * @param c 
+     * @param names  
+     * @param c 
      * 
      * @return
      **/
@@ -412,7 +412,7 @@ public class Context extends IDisposable
     /**
      * Creates a fresh function declaration with a name prefixed with
      * {@code prefix}. 
-	 * @see mkFuncDecl(String,Sort,Sort)
+     * @see mkFuncDecl(String,Sort,Sort)
      * @see mkFuncDecl(String,Sort[],Sort)
      **/
     public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
@@ -457,8 +457,8 @@ public class Context extends IDisposable
 
     /**
      * Creates a new bound variable. 
-	 * @param index The de-Bruijn index of the variable 
-	 * @param ty The sort of the variable
+     * @param index The de-Bruijn index of the variable 
+     * @param ty The sort of the variable
      **/
     public Expr mkBound(int index, Sort ty) throws Z3Exception
     {
@@ -516,7 +516,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a fresh constant from the FuncDecl {@code f}. 
-	 * @param f A decl of a 0-arity function
+     * @param f A decl of a 0-arity function
      **/
     public Expr mkConst(FuncDecl f) throws Z3Exception
     {
@@ -654,9 +654,9 @@ public class Context extends IDisposable
     /**
      * Create an expression representing an if-then-else:
      * {@code ite(t1, t2, t3)}. 
-	 * @param t1 An expression with Boolean sort 
-	 * @param t2 An expression  
-	 * @param t3 An expression with the same sort as {@code t2}
+     * @param t1 An expression with Boolean sort 
+     * @param t2 An expression  
+     * @param t3 An expression with the same sort as {@code t2}
      **/
     public Expr mkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception
     {
@@ -773,7 +773,7 @@ public class Context extends IDisposable
 
     /**
      * Create an expression representing {@code t1 mod t2}.
-	 * Remarks: The
+     * Remarks: The
      * arguments must have int type.
      **/
     public IntExpr mkMod(IntExpr t1, IntExpr t2) throws Z3Exception
@@ -786,7 +786,7 @@ public class Context extends IDisposable
 
     /**
      * Create an expression representing {@code t1 rem t2}.
-	 * Remarks: The
+     * Remarks: The
      * arguments must have int type.
      **/
     public IntExpr mkRem(IntExpr t1, IntExpr t2) throws Z3Exception
@@ -856,7 +856,7 @@ public class Context extends IDisposable
 
     /**
      * Coerce an integer to a real.
-	 * Remarks:  There is also a converse operation
+     * Remarks:  There is also a converse operation
      * exposed. It follows the semantics prescribed by the SMT-LIB standard.
      * 
      * You can take the floor of a real by creating an auxiliary integer Term
@@ -873,7 +873,7 @@ public class Context extends IDisposable
 
     /**
      * Coerce a real to an integer.
-	 * Remarks:  The semantics of this function
+     * Remarks:  The semantics of this function
      * follows the SMT-LIB standard for the function to_int. The argument must
      * be of real sort. 
      **/
@@ -894,7 +894,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise negation.
-	 * Remarks: The argument must have a bit-vector
+     * Remarks: The argument must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVNot(BitVecExpr t) throws Z3Exception
@@ -906,7 +906,7 @@ public class Context extends IDisposable
     /**
      * Take conjunction of bits in a vector, return vector of length 1.
      * 
-	 * Remarks: The argument must have a bit-vector sort.
+     * Remarks: The argument must have a bit-vector sort.
      **/
     public BitVecExpr mkBVRedAND(BitVecExpr t) throws Z3Exception
     {
@@ -918,7 +918,7 @@ public class Context extends IDisposable
     /**
      * Take disjunction of bits in a vector, return vector of length 1.
      * 
-	 * Remarks: The argument must have a bit-vector sort.
+     * Remarks: The argument must have a bit-vector sort.
      **/
     public BitVecExpr mkBVRedOR(BitVecExpr t) throws Z3Exception
     {
@@ -929,7 +929,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise conjunction.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -942,7 +942,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise disjunction.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -955,7 +955,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise XOR.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -968,7 +968,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise NAND.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -981,7 +981,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise NOR.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -994,7 +994,7 @@ public class Context extends IDisposable
 
     /**
      * Bitwise XNOR.
-	 * Remarks: The arguments must have a bit-vector
+     * Remarks: The arguments must have a bit-vector
      * sort.
      **/
     public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1007,7 +1007,7 @@ public class Context extends IDisposable
 
     /**
      * Standard two's complement unary minus.
-	 * Remarks: The arguments must have a
+     * Remarks: The arguments must have a
      * bit-vector sort.
      **/
     public BitVecExpr mkBVNeg(BitVecExpr t) throws Z3Exception
@@ -1018,7 +1018,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement addition.
-	 * Remarks: The arguments must have the same
+     * Remarks: The arguments must have the same
      * bit-vector sort.
      **/
     public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1031,7 +1031,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement subtraction.
-	 * Remarks: The arguments must have the same
+     * Remarks: The arguments must have the same
      * bit-vector sort.
      **/
     public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1044,7 +1044,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement multiplication.
-	 * Remarks: The arguments must have the
+     * Remarks: The arguments must have the
      * same bit-vector sort.
      **/
     public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1057,7 +1057,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned division.
-	 * Remarks:  It is defined as the floor of
+     * Remarks:  It is defined as the floor of
      * {@code t1/t2} if \c t2 is different from zero. If {@code t2} is
      * zero, then the result is undefined. The arguments must have the same
      * bit-vector sort. 
@@ -1072,7 +1072,7 @@ public class Context extends IDisposable
 
     /**
      * Signed division.
-	 * Remarks:  It is defined in the following way:
+     * Remarks:  It is defined in the following way:
      * 
      * - The \c floor of {@code t1/t2} if \c t2 is different from zero, and
      * {@code t1*t2 >= 0}.
@@ -1093,7 +1093,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned remainder.
-	 * Remarks:  It is defined as
+     * Remarks:  It is defined as
      * {@code t1 - (t1 /u t2) * t2}, where {@code /u} represents
      * unsigned division. If {@code t2} is zero, then the result is
      * undefined. The arguments must have the same bit-vector sort. 
@@ -1108,7 +1108,7 @@ public class Context extends IDisposable
 
     /**
      * Signed remainder.
-	 * Remarks:  It is defined as
+     * Remarks:  It is defined as
      * {@code t1 - (t1 /s t2) * t2}, where {@code /s} represents
      * signed division. The most significant bit (sign) of the result is equal
      * to the most significant bit of \c t1.
@@ -1126,7 +1126,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement signed remainder (sign follows divisor).
-	 * Remarks:  If
+     * Remarks:  If
      * {@code t2} is zero, then the result is undefined. The arguments must
      * have the same bit-vector sort. 
      **/
@@ -1140,7 +1140,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned less-than
-	 * Remarks:  The arguments must have the same bit-vector
+     * Remarks:  The arguments must have the same bit-vector
      * sort. 
      **/
     public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1153,7 +1153,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement signed less-than
-	 * Remarks:  The arguments must have the
+     * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
     public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1166,7 +1166,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned less-than or equal to.
-	 * Remarks:  The arguments must have the
+     * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
     public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1179,7 +1179,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement signed less-than or equal to.
-	 * Remarks:  The arguments
+     * Remarks:  The arguments
      * must have the same bit-vector sort. 
      **/
     public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1192,7 +1192,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned greater than or equal to.
-	 * Remarks:  The arguments must have the
+     * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
     public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1205,7 +1205,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement signed greater than or equal to.
-	 * Remarks:  The arguments
+     * Remarks:  The arguments
      * must have the same bit-vector sort. 
      **/
     public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1218,7 +1218,7 @@ public class Context extends IDisposable
 
     /**
      * Unsigned greater-than.
-	 * Remarks:  The arguments must have the same
+     * Remarks:  The arguments must have the same
      * bit-vector sort. 
      **/
     public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1231,7 +1231,7 @@ public class Context extends IDisposable
 
     /**
      * Two's complement signed greater-than.
-	 * Remarks:  The arguments must have
+     * Remarks:  The arguments must have
      * the same bit-vector sort. 
      **/
     public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
@@ -1244,7 +1244,7 @@ public class Context extends IDisposable
 
     /**
      * Bit-vector concatenation.
-	 * Remarks:  The arguments must have a bit-vector
+     * Remarks:  The arguments must have a bit-vector
      * sort. 
      * 
      * @return The result is a bit-vector of size {@code n1+n2}, where
@@ -1262,7 +1262,7 @@ public class Context extends IDisposable
 
     /**
      * Bit-vector extraction.
-	 * Remarks:  Extract the bits {@code high}
+     * Remarks:  Extract the bits {@code high}
      * down to {@code low} from a bitvector of size {@code m} to
      * yield a new bitvector of size {@code n}, where
      * {@code n = high - low + 1}. The argument {@code t} must
@@ -1278,7 +1278,7 @@ public class Context extends IDisposable
 
     /**
      * Bit-vector sign extension.
-	 * Remarks:  Sign-extends the given bit-vector to
+     * Remarks:  Sign-extends the given bit-vector to
      * the (signed) equivalent bitvector of size {@code m+i}, where \c m is
      * the size of the given bit-vector. The argument {@code t} must
      * have a bit-vector sort. 
@@ -1292,7 +1292,7 @@ public class Context extends IDisposable
 
     /**
      * Bit-vector zero extension.
-	 * Remarks:  Extend the given bit-vector with
+     * Remarks:  Extend the given bit-vector with
      * zeros to the (unsigned) equivalent bitvector of size {@code m+i},
      * where \c m is the size of the given bit-vector. The argument {@code t}
      * must have a bit-vector sort. 
@@ -1306,7 +1306,7 @@ public class Context extends IDisposable
 
     /**
      * Bit-vector repetition.
-	 * Remarks:  The argument {@code t} must
+     * Remarks:  The argument {@code t} must
      * have a bit-vector sort. 
      **/
     public BitVecExpr mkRepeat(int i, BitVecExpr t) throws Z3Exception
@@ -1318,7 +1318,7 @@ public class Context extends IDisposable
 
     /**
      * Shift left.
-	 * Remarks:  It is equivalent to multiplication by
+     * Remarks:  It is equivalent to multiplication by
      * {@code 2^x} where \c x is the value of {@code t2}.
      * 
      * NB. The semantics of shift operations varies between environments. This
@@ -1337,7 +1337,7 @@ public class Context extends IDisposable
 
     /**
      * Logical shift right
-	 * Remarks:  It is equivalent to unsigned division by
+     * Remarks:  It is equivalent to unsigned division by
      * {@code 2^x} where \c x is the value of {@code t2}.
      * 
      * NB. The semantics of shift operations varies between environments. This
@@ -1356,7 +1356,7 @@ public class Context extends IDisposable
 
     /**
      * Arithmetic shift right
-	 * Remarks:  It is like logical shift right except
+     * Remarks:  It is like logical shift right except
      * that the most significant bits of the result always copy the most
      * significant bit of the second argument.
      * 
@@ -1376,7 +1376,7 @@ public class Context extends IDisposable
 
     /**
      * Rotate Left.
-	 * Remarks:  Rotate bits of \c t to the left \c i times. The
+     * Remarks:  Rotate bits of \c t to the left \c i times. The
      * argument {@code t} must have a bit-vector sort. 
      **/
     public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t) throws Z3Exception
@@ -1388,7 +1388,7 @@ public class Context extends IDisposable
 
     /**
      * Rotate Right.
-	 * Remarks:  Rotate bits of \c t to the right \c i times. The
+     * Remarks:  Rotate bits of \c t to the right \c i times. The
      * argument {@code t} must have a bit-vector sort. 
      **/
     public BitVecExpr mkBVRotateRight(int i, BitVecExpr t) throws Z3Exception
@@ -1400,7 +1400,7 @@ public class Context extends IDisposable
 
     /**
      * Rotate Left.
-	 * Remarks:  Rotate bits of {@code t1} to the left
+     * Remarks:  Rotate bits of {@code t1} to the left
      * {@code t2} times. The arguments must have the same bit-vector
      * sort. 
      **/
@@ -1415,7 +1415,7 @@ public class Context extends IDisposable
 
     /**
      * Rotate Right.
-	 * Remarks:  Rotate bits of {@code t1} to the
+     * Remarks:  Rotate bits of {@code t1} to the
      * right{@code t2} times. The arguments must have the same
      * bit-vector sort. 
      **/
@@ -1431,7 +1431,7 @@ public class Context extends IDisposable
     /**
      * Create an {@code n} bit bit-vector from the integer argument
      * {@code t}.
-	 * Remarks:  NB. This function is essentially treated
+     * Remarks:  NB. This function is essentially treated
      * as uninterpreted. So you cannot expect Z3 to precisely reflect the
      * semantics of this function when solving constraints with this function.
      * 
@@ -1468,7 +1468,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise addition does not
      * overflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2,
             boolean isSigned) throws Z3Exception
@@ -1483,7 +1483,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise addition does not
      * underflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
             throws Z3Exception
@@ -1497,7 +1497,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise subtraction does not
      * overflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
             throws Z3Exception
@@ -1511,7 +1511,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise subtraction does not
      * underflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2,
             boolean isSigned) throws Z3Exception
@@ -1526,7 +1526,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise signed division does not
      * overflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
             throws Z3Exception
@@ -1540,7 +1540,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise negation does not
      * overflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVNegNoOverflow(BitVecExpr t) throws Z3Exception
     {
@@ -1552,7 +1552,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise multiplication does not
      * overflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2,
             boolean isSigned) throws Z3Exception
@@ -1567,7 +1567,7 @@ public class Context extends IDisposable
     /**
      * Create a predicate that checks that the bit-wise multiplication does not
      * underflow. 
-	 * Remarks:  The arguments must be of bit-vector sort. 
+     * Remarks:  The arguments must be of bit-vector sort. 
      **/
     public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
             throws Z3Exception
@@ -1598,15 +1598,15 @@ public class Context extends IDisposable
 
     /**
      * Array read.
-	 * Remarks:  The argument {@code a} is the array and
+     * Remarks:  The argument {@code a} is the array and
      * {@code i} is the index of the array that gets read.
      * 
      * The node {@code a} must have an array sort
      * {@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) throws Z3Exception
@@ -1621,7 +1621,7 @@ public class Context extends IDisposable
 
     /**
      * Array update.
-	 * Remarks:  The node {@code a} must have an array sort
+     * Remarks:  The node {@code a} must have an array sort
      * {@code [domain -> range]}, {@code i} must have sort
      * {@code domain}, {@code v} must have sort range. The sort of the
      * result is {@code [domain -> range]}. The semantics of this function
@@ -1631,8 +1631,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) throws Z3Exception
@@ -1646,11 +1646,11 @@ public class Context extends IDisposable
 
     /**
      * Create a constant array.
-	 * Remarks:  The resulting term is an array, such
+     * 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) throws Z3Exception
@@ -1663,15 +1663,15 @@ public class Context extends IDisposable
 
     /**
      * Maps f on the argument arrays.
-	 * Remarks:  Eeach element of
+     * Remarks:  Eeach 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) throws Z3Exception
@@ -1685,7 +1685,7 @@ public class Context extends IDisposable
 
     /**
      * Access the array default value.
-	 * Remarks:  Produces the default range
+     * Remarks:  Produces the default range
      * value, for arrays that can be represented as finite maps with a default
      * range value. 
      **/
@@ -1826,10 +1826,10 @@ public class Context extends IDisposable
 
     /**
      * Create a Term of a given sort. 
-	 * @param v A string representing the term value in decimal notation. If the given sort is a real, then the
+     * @param v A string representing the term value in decimal notation. If the given sort is a real, then the
      * Term can be a rational, that is, a string of the form
      * {@code [num]* / [num]*}.
-	 * @param ty The sort of the
+     * @param ty The sort of the
      * numeral. In the current implementation, the given sort can be an int,
      * real, or bit-vectors of arbitrary size.
      * 
@@ -1847,8 +1847,8 @@ public class Context extends IDisposable
      * numerals that fit in a machine integer. It is slightly faster than
      * {@code MakeNumeral} since it is not necessary to parse a string.
      * 
-	 * @param v Value of the numeral 
-	 * @param ty Sort of the numeral
+     * @param v Value of the numeral 
+     * @param ty Sort of the numeral
      * 
      * @return A Term with value {@code v} and type {@code ty}
      **/
@@ -1863,8 +1863,8 @@ public class Context extends IDisposable
      * numerals that fit in a machine integer. It is slightly faster than
      * {@code MakeNumeral} since it is not necessary to parse a string.
      * 
-	 * @param v Value of the numeral 
-	 * @param ty Sort of the numeral
+     * @param v Value of the numeral 
+     * @param ty Sort of the numeral
      * 
      * @return A Term with value {@code v} and type {@code ty}
      **/
@@ -1877,12 +1877,12 @@ public class Context extends IDisposable
 
     /**
      * Create a real from a fraction. 
-	 * @param num numerator of rational. 
-	 * @param den denominator of rational.
+     * @param num numerator of rational. 
+     * @param den denominator of rational.
      * 
      * @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) throws Z3Exception
     {
@@ -1894,7 +1894,7 @@ public class Context extends IDisposable
 
     /**
      * Create a real numeral. 
-	 * @param v A string representing the Term value in decimal notation.
+     * @param v A string representing the Term value in decimal notation.
      * 
      * @return A Term with value {@code v} and sort Real
      **/
@@ -1907,7 +1907,7 @@ public class Context extends IDisposable
 
     /**
      * Create a real numeral. 
-	 * @param v value of the numeral.
+     * @param v value of the numeral.
      * 
      * @return A Term with value {@code v} and sort Real
      **/
@@ -1920,7 +1920,7 @@ public class Context extends IDisposable
 
     /**
      * Create a real numeral. 
-	 * @param v value of the numeral.
+     * @param v value of the numeral.
      * 
      * @return A Term with value {@code v} and sort Real
      **/
@@ -1933,7 +1933,7 @@ public class Context extends IDisposable
 
     /**
      * Create an integer numeral. 
-	 * @param v A string representing the Term value in decimal notation.
+     * @param v A string representing the Term value in decimal notation.
      **/
     public IntNum mkInt(String v) throws Z3Exception
     {
@@ -1944,7 +1944,7 @@ public class Context extends IDisposable
 
     /**
      * Create an integer numeral. 
-	 * @param v value of the numeral.
+     * @param v value of the numeral.
      * 
      * @return A Term with value {@code v} and sort Integer
      **/
@@ -1957,7 +1957,7 @@ public class Context extends IDisposable
 
     /**
      * Create an integer numeral. 
-	 * @param v value of the numeral.
+     * @param v value of the numeral.
      * 
      * @return A Term with value {@code v} and sort Integer
      **/
@@ -1970,8 +1970,8 @@ public class Context extends IDisposable
 
     /**
      * Create a bit-vector numeral. 
-	 * @param v A string representing the value in decimal notation. 
-	 * @param size the size of the bit-vector
+     * @param v A string representing the value in decimal notation. 
+     * @param size the size of the bit-vector
      **/
     public BitVecNum mkBV(String v, int size) throws Z3Exception
     {
@@ -1980,8 +1980,8 @@ public class Context extends IDisposable
 
     /**
      * Create a bit-vector numeral. 
-	 * @param v value of the numeral. 
-	 * @param size the size of the bit-vector
+     * @param v value of the numeral. 
+     * @param size the size of the bit-vector
      **/
     public BitVecNum mkBV(int v, int size) throws Z3Exception
     {
@@ -1990,8 +1990,8 @@ public class Context extends IDisposable
 
     /**
      * Create a bit-vector numeral. 
-	 * @param v value of the numeral. * 
-	 * @param size the size of the bit-vector
+     * @param v value of the numeral. * 
+     * @param size the size of the bit-vector
      **/
     public BitVecNum mkBV(long v, int size) throws Z3Exception
     {
@@ -2000,16 +2000,16 @@ public class Context extends IDisposable
 
     /**
      * Create a universal Quantifier.
-	 * @param sorts the sorts of the bound variables. 
-	 * @param names names of the bound variables 
-	 * @param body the body of the quantifier. 
-	 * @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
+     * @param sorts the sorts of the bound variables. 
+     * @param names names of the bound variables 
+     * @param body the body of the quantifier. 
+     * @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
      * @param patterns array containing the patterns created using {@code MkPattern}. 
-	 * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. 
-	 * @param quantifierID optional symbol to track quantifier. 
-	 * @param skolemID optional symbol to track skolem constants.
-	 * 
-	 * Remarks:  Creates a forall formula, where
+     * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. 
+     * @param quantifierID optional symbol to track quantifier. 
+     * @param skolemID optional symbol to track skolem constants.
+     * 
+     * Remarks:  Creates a forall formula, where
      * {@code weight"/> is the weight, <paramref name="patterns} is
      * an array of patterns, {@code sorts} is an array with the sorts
      * of the bound variables, {@code names} is an array with the
@@ -2040,7 +2040,7 @@ public class Context extends IDisposable
 
     /**
      * Create an existential Quantifier. 
-	 * @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,
@@ -2098,17 +2098,17 @@ public class Context extends IDisposable
 
     /**
      * Selects the format used for pretty-printing expressions.
-	 * Remarks:  The
+     * Remarks:  The
      * default mode for pretty printing expressions is to produce SMT-LIB style
      * output where common subexpressions are printed at each occurrence. The
      * mode is called Z3_PRINT_SMTLIB_FULL. To print shared common
      * subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in
      * way that conforms to SMT-LIB standards and uses let expressions to share
      * common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.  
-	 * @see AST#toString
-	 * @see Pattern#toString
+     * @see AST#toString
+     * @see Pattern#toString
      * @see FuncDecl#toString
-	 * @see Sort#toString
+     * @see Sort#toString
      **/
     public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception
     {
@@ -2117,14 +2117,14 @@ public class Context extends IDisposable
 
     /**
      * Convert a benchmark into an SMT-LIB formatted string. 
-	 * @param name Name of the benchmark. The argument is optional.
+     * @param name Name of the benchmark. The argument is optional.
      * 
-	 * @param logic The benchmark logic.  
-	 * @param status The status string (sat, unsat, or unknown) 
-	 * @param attributes Other attributes, such as source, difficulty or
+     * @param logic The benchmark logic.  
+     * @param status The status string (sat, unsat, or unknown) 
+     * @param attributes Other attributes, such as source, difficulty or
      * category.
-	 * @param assumptions Auxiliary assumptions. 
-	 * @param formula Formula to be checked for consistency in conjunction with assumptions.
+     * @param assumptions Auxiliary assumptions. 
+     * @param formula Formula to be checked for consistency in conjunction with assumptions.
      * 
      * @return A string representation of the benchmark.
      **/
@@ -2140,7 +2140,7 @@ public class Context extends IDisposable
 
     /**
      * Parse the given string using the SMT-LIB parser.
-	 * Remarks:  The symbol
+     * Remarks:  The symbol
      * table of the parser can be initialized using the given sorts and
      * declarations. The symbols in the arrays {@code sortNames} and
      * {@code declNames} don't need to match the names of the sorts
@@ -2164,7 +2164,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)
@@ -2278,7 +2278,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.
@@ -2302,7 +2302,7 @@ 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)
@@ -2324,12 +2324,12 @@ public class Context extends IDisposable
 
     /**
      * Creates a new Goal.
-	 * Remarks:  Note that the Context must have been
+     * Remarks:  Note that the Context must have been
      * created with proof generation support if {@code proofs} is set
      * to true here.  
-	 * @param models Indicates whether model generation should be enabled. 
-	 * @param unsatCores Indicates whether unsat core generation should be enabled. 
-	 * @param proofs Indicates whether proof generation should be
+     * @param models Indicates whether model generation should be enabled. 
+     * @param unsatCores Indicates whether unsat core generation should be enabled. 
+     * @param proofs Indicates whether proof generation should be
      * enabled.
      **/
     public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
@@ -2417,7 +2417,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}.
      * 
-	 * Remarks:  Shorthand for {@code AndThen}. 
+     * Remarks:  Shorthand for {@code AndThen}. 
      **/
     public Tactic then(Tactic t1, Tactic t2, Tactic... ts) throws Z3Exception
     {
@@ -2439,7 +2439,7 @@ public class Context extends IDisposable
 
     /**
      * Create a tactic that applies {@code t} to a goal for {@code ms} milliseconds.
-	 * Remarks:  If {@code t} does not
+     * Remarks:  If {@code t} does not
      * terminate within {@code ms} milliseconds, then it fails.
      * 
      **/
@@ -2453,7 +2453,7 @@ public class Context extends IDisposable
     /**
      * Create a tactic that applies {@code t} to a given goal if the
      * probe {@code p} evaluates to true.
-	 * Remarks:  If {@code p} evaluates to false, then the new tactic behaves like the
+     * Remarks:  If {@code p} evaluates to false, then the new tactic behaves like the
      * {@code skip} tactic. 
      **/
     public Tactic when(Probe p, Tactic t) throws Z3Exception
@@ -2540,7 +2540,7 @@ public class Context extends IDisposable
     /**
      * Create a tactic that applies {@code t} using the given set of
      * parameters {@code p}.
-	 * Remarks: Alias for
+     * Remarks: Alias for
      * {@code UsingParams}
      **/
     public Tactic with(Tactic t, Params p) throws Z3Exception
@@ -2572,7 +2572,7 @@ public class Context extends IDisposable
 
     /**
      * Interrupt the execution of a Z3 procedure.
-	 * Remarks: This procedure can be
+     * Remarks: This procedure can be
      * used to interrupt: solvers, simplifiers and tactics.
      **/
     public void interrupt() throws Z3Exception
@@ -2721,7 +2721,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a new (incremental) solver.
-	 * Remarks:  This solver also uses a set
+     * Remarks:  This solver also uses a set
      * of builtin tactics for handling the first check-sat command, and
      * check-sat commands that take more than a given number of milliseconds to
      * be solved. 
@@ -2733,7 +2733,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a new (incremental) solver.
-	 * Remarks:  This solver also uses a set
+     * Remarks:  This solver also uses a set
      * of builtin tactics for handling the first check-sat command, and
      * check-sat commands that take more than a given number of milliseconds to
      * be solved. 
@@ -2750,7 +2750,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a new (incremental) solver. 
-	 * @see mkSolver(Symbol)
+     * @see mkSolver(Symbol)
      **/
     public Solver mkSolver(String logic) throws Z3Exception
     {
@@ -2767,7 +2767,7 @@ public class Context extends IDisposable
 
     /**
      * Creates a solver that is implemented using the given tactic.
-	 * Remarks: 
+     * Remarks: 
      * The solver supports the commands {@code Push} and {@code Pop},
      * but it will always solve each check from scratch. 
      **/
@@ -3560,13 +3560,13 @@ public class Context extends IDisposable
     
     /**
      * Wraps an AST.
-	 * Remarks: This function is used for transitions between
+     * Remarks: This function is used for transitions between
      * native and managed objects. Note that {@code nativeObject}
      * must be a native object obtained from Z3 (e.g., through 
-	 * {@code UnwrapAST}) and that it must have a correct reference count.
-	 * @see Native#incRef 
-	 * @see unwrapAST
-	 * @param nativeObject The native pointer to wrap.
+     * {@code UnwrapAST}) and that it must have a correct reference count.
+     * @see Native#incRef 
+     * @see unwrapAST
+     * @param nativeObject The native pointer to wrap.
      **/
     public AST wrapAST(long nativeObject) throws Z3Exception
     {
@@ -3575,15 +3575,15 @@ public class Context extends IDisposable
 
     /**
      * Unwraps an AST.
-	 * Remarks: This function is used for transitions between
+     * Remarks: This function is used for transitions between
      * native and managed objects. It returns the native pointer to the AST.
      * Note that AST objects are reference counted and unwrapping an AST
      * disables automatic reference counting, i.e., all references to the IntPtr
      * that is returned must be handled externally and through native calls (see
      * e.g., 
-	 * @see Native#incRef 
-	 * @see wrapAST 
-	 * @param a The AST to unwrap.
+     * @see Native#incRef 
+     * @see wrapAST 
+     * @param a The AST to unwrap.
      **/
     public long unwrapAST(AST a)
     {
@@ -3609,7 +3609,7 @@ public class Context extends IDisposable
 
     /**
      * Enable/disable printing of warning messages to the console.
-	 * Remarks: Note
+     * Remarks: Note
      * that this function is static and effects the behaviour of all contexts
      * globally.
      **/
@@ -3621,7 +3621,7 @@ public class Context extends IDisposable
 
     /**
      * Update a mutable configuration parameter.
-	 * Remarks:  The list of all
+     * Remarks:  The list of all
      * configuration parameters can be obtained using the Z3 executable:
      * {@code z3.exe -ini?} Only a few configuration parameters are mutable
      * once the context is created. An exception is thrown when trying to modify
@@ -3659,20 +3659,20 @@ public class Context extends IDisposable
     }
 
     private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
-    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
-    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
-    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
-    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
-    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
-    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
-    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
-    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
-    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
-    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
-    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
-    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
-    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
-    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
+    private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
+    private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
+    private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
+    private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
+    private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
+    private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
+    private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
+    private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
+    private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
+    private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
+    private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
+    private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
+    private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
+    private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
 
     ASTDecRefQueue ast_DRQ()
     {
diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java
index c0f247b7a..3ad714dde 100644
--- a/src/api/java/DatatypeExpr.java
+++ b/src/api/java/DatatypeExpr.java
@@ -22,11 +22,11 @@ package com.microsoft.z3;
  **/
 public class DatatypeExpr extends Expr
 {
-	/**
-	 * Constructor for DatatypeExpr
-	 **/
-	DatatypeExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for DatatypeExpr
+     **/
+    DatatypeExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java
index 4a31b6c38..2e02ad68b 100644
--- a/src/api/java/DatatypeSort.java
+++ b/src/api/java/DatatypeSort.java
@@ -22,86 +22,86 @@ package com.microsoft.z3;
  **/
 public class DatatypeSort extends Sort
 {
-	/**
-	 * The number of constructors of the datatype sort.
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getNumConstructors() throws Z3Exception
-	{
-		return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
-				getNativeObject());
-	}
+    /**
+     * The number of constructors of the datatype sort.
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getNumConstructors() throws Z3Exception
+    {
+        return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
+                getNativeObject());
+    }
 
-	/**
-	 * The constructors.
-	 * 
-	 * @throws Z3Exception
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[] getConstructors() throws Z3Exception
-	{
-		int n = getNumConstructors();
-		FuncDecl[] res = new FuncDecl[n];
-		for (int i = 0; i < n; i++)
-			res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
-					getContext().nCtx(), getNativeObject(), i));
-		return res;
-	}
+    /**
+     * The constructors.
+     * 
+     * @throws Z3Exception
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[] getConstructors() throws Z3Exception
+    {
+        int n = getNumConstructors();
+        FuncDecl[] res = new FuncDecl[n];
+        for (int i = 0; i < n; i++)
+            res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
+                    getContext().nCtx(), getNativeObject(), i));
+        return res;
+    }
 
-	/**
-	 * The recognizers.
-	 * 
-	 * @throws Z3Exception
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[] getRecognizers() throws Z3Exception
-	{
-		int n = getNumConstructors();
-		FuncDecl[] res = new FuncDecl[n];
-		for (int i = 0; i < n; i++)
-			res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
-					getContext().nCtx(), getNativeObject(), i));
-		return res;
-	}
+    /**
+     * The recognizers.
+     * 
+     * @throws Z3Exception
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[] getRecognizers() throws Z3Exception
+    {
+        int n = getNumConstructors();
+        FuncDecl[] res = new FuncDecl[n];
+        for (int i = 0; i < n; i++)
+            res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
+                    getContext().nCtx(), getNativeObject(), i));
+        return res;
+    }
 
-	/**
-	 * The constructor accessors.
-	 * 
-	 * @throws Z3Exception
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[][] getAccessors() throws Z3Exception
-	{
+    /**
+     * The constructor accessors.
+     * 
+     * @throws Z3Exception
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[][] getAccessors() throws Z3Exception
+    {
 
-		int n = getNumConstructors();
-		FuncDecl[][] res = new FuncDecl[n][];
-		for (int i = 0; i < n; i++)
-		{
-			FuncDecl fd = new FuncDecl(getContext(),
-					Native.getDatatypeSortConstructor(getContext().nCtx(),
-							getNativeObject(), i));
-			int ds = fd.getDomainSize();
-			FuncDecl[] tmp = new FuncDecl[ds];
-			for (int j = 0; j < ds; j++)
-				tmp[j] = new FuncDecl(getContext(),
-						Native.getDatatypeSortConstructorAccessor(getContext()
-								.nCtx(), getNativeObject(), i, j));
-			res[i] = tmp;
-		}
-		return res;
-	}
+        int n = getNumConstructors();
+        FuncDecl[][] res = new FuncDecl[n][];
+        for (int i = 0; i < n; i++)
+        {
+            FuncDecl fd = new FuncDecl(getContext(),
+                    Native.getDatatypeSortConstructor(getContext().nCtx(),
+                            getNativeObject(), i));
+            int ds = fd.getDomainSize();
+            FuncDecl[] tmp = new FuncDecl[ds];
+            for (int j = 0; j < ds; j++)
+                tmp[j] = new FuncDecl(getContext(),
+                        Native.getDatatypeSortConstructorAccessor(getContext()
+                                .nCtx(), getNativeObject(), i, j));
+            res[i] = tmp;
+        }
+        return res;
+    }
 
-	DatatypeSort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    DatatypeSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
-			throws Z3Exception
-	{
-		super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
-				(int) constructors.length, arrayToNative(constructors)));
+    DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
+            throws Z3Exception
+    {
+        super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
+                (int) constructors.length, arrayToNative(constructors)));
 
-	}
+    }
 };
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index 06e1ade73..e33b9b348 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -22,55 +22,55 @@ package com.microsoft.z3;
  **/
 public class EnumSort extends Sort
 {
-	/**
-	 * The function declarations of the constants in the enumeration.
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[] getConstDecls() throws Z3Exception
-	{
-	    int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
+    /**
+     * The function declarations of the constants in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[] getConstDecls() throws Z3Exception
+    {
+        int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
         FuncDecl[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
             t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
         return t;
-	}
+    }
 
-	/**
-	 * The constants in the enumeration.
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr[] getConsts() throws Z3Exception
-	{	    
-	    FuncDecl[] cds = getConstDecls();
+    /**
+     * The constants in the enumeration.
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr[] getConsts() throws Z3Exception
+    {        
+        FuncDecl[] cds = getConstDecls();
         Expr[] t = new Expr[cds.length];
         for (int i = 0; i < t.length; i++)
             t[i] = getContext().mkApp(cds[i]);
         return t;
-	}
+    }
 
-	/**
-	 * The test predicates for the constants in the enumeration.
-	 * @throws Z3Exception on error
-	 **/
-	public FuncDecl[] getTesterDecls() throws Z3Exception
-	{
-	    int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
+    /**
+     * The test predicates for the constants in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl[] getTesterDecls() throws Z3Exception
+    {
+        int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
         FuncDecl[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
             t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
         return t;
-	}
+    }
 
-	EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
-	{
-		super(ctx, 0);
+    EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
+    {
+        super(ctx, 0);
 
-		int n = enumNames.length;
-		long[] n_constdecls = new long[n];
-		long[] n_testers = new long[n];
-		setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
-				name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
-				n_constdecls, n_testers));		
-	}
+        int n = enumNames.length;
+        long[] n_constdecls = new long[n];
+        long[] n_testers = new long[n];
+        setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
+                name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
+                n_constdecls, n_testers));        
+    }
 };
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 762a4b672..2b8f7e822 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -29,2167 +29,2167 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
  **/
 public class Expr extends AST
 {
-	/**
-	 * Returns a simplified version of the expression
-	 * @return Expr
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr simplify() throws Z3Exception
-	{
-	    return simplify(null);
-	}
-
-	/**
-	 * Returns a simplified version of the expression 
-	 * A set of
-	 * parameters 
-	 * @param p a Params object to configure the simplifier 
-	 * @see Context#SimplifyHelp
-	 * @return an Expr
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr simplify(Params p) throws Z3Exception
-	{
-
-		if (p == null)
-			return Expr.create(getContext(),
-					Native.simplify(getContext().nCtx(), getNativeObject()));
-		else
-			return Expr.create(
-					getContext(),
-					Native.simplifyEx(getContext().nCtx(), getNativeObject(),
-							p.getNativeObject()));
-	}
-
-	/**
-	 * The function declaration of the function that is applied in this
-	 * expression.
-	 * @return a FuncDecl
-	 * @throws Z3Exception on error 
-	 **/
-	public FuncDecl getFuncDecl() throws Z3Exception
-	{
-		return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
-				getNativeObject()));
-	}
-
-	/**
-	 * Indicates whether the expression is the true or false expression or
-	 * something else (Z3_L_UNDEF).
-	 * @throws Z3Exception on error	 
-	 * @return a Z3_lbool
-	 **/
-	public Z3_lbool getBoolValue() throws Z3Exception
-	{
-		return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
-				getNativeObject()));
-	}
-
-	/**
-	 * The number of arguments of the expression.
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getNumArgs() throws Z3Exception
-	{
-		return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
-	}
-
-	/**
-	 * The arguments of the expression.
-	 * @throws Z3Exception on error
-	 * @return an Expr[]
-	 **/
-	public Expr[] getArgs() throws Z3Exception
-	{
-		int n = getNumArgs();
-		Expr[] res = new Expr[n];
-		for (int i = 0; i < n; i++)
-			res[i] = Expr.create(getContext(),
-					Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
-		return res;
-	}
-
-	/**
-	 * Update the arguments of the expression using the arguments {@code args}
-	 * The number of new arguments should coincide with the
-	 * current number of arguments.
-	 * @param args arguments
-	 * @throws Z3Exception on error
-	 **/
-	public void update(Expr[] args) throws Z3Exception
-	{
-		getContext().checkContextMatch(args);
-		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)));
-	}
-
-	/**
-	 * Substitute every occurrence of {@code from[i]} in the expression
-	 * with {@code to[i]}, for {@code i} smaller than
-	 * {@code num_exprs}. 
-	 * Remarks: The result is the new expression. The
-	 * arrays {@code from} and {@code to} must have size
-	 * {@code num_exprs}. For every {@code i} smaller than
-	 * {@code num_exprs}, we must have that sort of {@code from[i]}
-	 * must be equal to sort of {@code to[i]}.
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr substitute(Expr[] from, Expr[] to) throws Z3Exception
-	{
-		getContext().checkContextMatch(from);
-		getContext().checkContextMatch(to);
-		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),
-				Expr.arrayToNative(to)));
-	}
-
-	/**
-	 * Substitute every occurrence of {@code from} in the expression with
-	 * {@code to}. 
-	 * @see Expr#substitute(Expr[],Expr[])
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr substitute(Expr from, Expr to) throws Z3Exception
-	{
-
-		return substitute(new Expr[] { from }, new Expr[] { to });
-	}
-
-	/**
-	 * Substitute the free variables in the expression with the expressions in
-	 * {@code to} 
-	 * Remarks:  For every {@code i} smaller than * {@code num_exprs}, the 
-	 * variable with de-Bruijn index {@code i} * is replaced with term 
-	 * {@code to[i]}.
-	 * @throws Z3Exception on error 
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr substituteVars(Expr[] to) throws Z3Exception
-	{
-
-		getContext().checkContextMatch(to);
-		return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
-				getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
-	}
-
-	/**
-	 * Translates (copies) the term to the Context {@code ctx}.
-	 * 
-	 * @param ctx A context
-	 * 
-	 * @return A copy of the term which is associated with {@code ctx}
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr translate(Context ctx) throws Z3Exception
-	{
-
-		if (getContext() == ctx)
-			return this;
-		else
-			return Expr.create(
-					ctx,
-					Native.translate(getContext().nCtx(), getNativeObject(),
-							ctx.nCtx()));
-	}
-
-	/**
-	 * Returns a string representation of the expression.
-	 **/
-	public String toString()
-	{
-		return super.toString();
-	}
-
-	/**
-	 * Indicates whether the term is a numeral
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isNumeral() throws Z3Exception
-	{
-		return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
-	}
-
-	/**
-	 * Indicates whether the term is well-sorted.
-	 * 
-	 * @return True if the term is well-sorted, false otherwise.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isWellSorted() throws Z3Exception
-	{
-		return Native.isWellSorted(getContext().nCtx(), getNativeObject());
-	}
-
-	/**
-	 * The Sort of the term.
-	 * @throws Z3Exception on error
-	 * @return a sort
-	 **/
-	public Sort getSort() throws Z3Exception
-	{
-		return Sort.create(getContext(),
-				Native.getSort(getContext().nCtx(), getNativeObject()));
-	}
-
-	/**
-	 * Indicates whether the term represents a constant.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isConst() throws Z3Exception
-	{
-		return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
-	}
-
-	/**
-	 * Indicates whether the term is an integer numeral.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIntNum() throws Z3Exception
-	{
-		return isNumeral() && isInt();
-	}
-
-	/**
-	 * Indicates whether the term is a real numeral.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRatNum() throws Z3Exception
-	{
-		return isNumeral() && isReal();
-	}
-
-	/**
-	 * Indicates whether the term is an algebraic number
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isAlgebraicNumber() throws Z3Exception
-	{
-		return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
-	}
-
-	/**
-	 * Indicates whether the term has Boolean sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBool() throws Z3Exception
-	{
-		return (isExpr() && Native.isEqSort(getContext().nCtx(),
-				Native.mkBoolSort(getContext().nCtx()),
-				Native.getSort(getContext().nCtx(), getNativeObject())));
-	}
-
-	/**
-	 * Indicates whether the term is the constant true.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isTrue() throws Z3Exception
-	{
-	        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
-	}
-
-	/**
-	 * Indicates whether the term is the constant false.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isFalse() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
-	}
-
-	/**
-	 * Indicates whether the term is an equality predicate.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isEq() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
-	}
-
-	/**
-	 * Indicates whether the term is an n-ary distinct predicate (every argument
-	 * is mutually distinct).
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isDistinct() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
-	}
-
-	/**
-	 * Indicates whether the term is a ternary if-then-else term
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isITE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
-	}
-
-	/**
-	 * Indicates whether the term is an n-ary conjunction
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isAnd() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
-	}
-
-	/**
-	 * Indicates whether the term is an n-ary disjunction
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isOr() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
-	}
-
-	/**
-	 * Indicates whether the term is an if-and-only-if (Boolean equivalence,
-	 * binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIff() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
-	}
-
-	/**
-	 * Indicates whether the term is an exclusive or
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isXor() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
-	}
-
-	/**
-	 * Indicates whether the term is a negation
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isNot() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
-	}
-
-	/**
-	 * Indicates whether the term is an implication
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isImplies() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
-	}
-
-	/**
-	 * Indicates whether the term is of integer sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isInt() throws Z3Exception
-	{
-		return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
-				.getSortKind(getContext().nCtx(),
-						Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
-				.toInt());
-	}
-
-	/**
-	 * Indicates whether the term is of sort real.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isReal() throws Z3Exception
-	{
-		return Native.getSortKind(getContext().nCtx(),
-				Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
-				.toInt();
-	}
-
-	/**
-	 * Indicates whether the term is an arithmetic numeral.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isArithmeticNumeral() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
-	}
-
-	/**
-	 * Indicates whether the term is a less-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isLE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
-	}
-
-	/**
-	 * Indicates whether the term is a greater-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isGE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
-	}
-
-	/**
-	 * Indicates whether the term is a less-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isLT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
-	}
-
-	/**
-	 * Indicates whether the term is a greater-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isGT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
-	}
-
-	/**
-	 * Indicates whether the term is addition (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isAdd() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
-	}
-
-	/**
-	 * Indicates whether the term is subtraction (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSub() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
-	}
-
-	/**
-	 * Indicates whether the term is a unary minus
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isUMinus() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
-	}
-
-	/**
-	 * Indicates whether the term is multiplication (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isMul() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
-	}
-
-	/**
-	 * Indicates whether the term is division (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isDiv() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
-	}
-
-	/**
-	 * Indicates whether the term is integer division (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIDiv() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
-	}
-
-	/**
-	 * Indicates whether the term is remainder (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRemainder() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
-	}
-
-	/**
-	 * Indicates whether the term is modulus (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isModulus() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
-	}
-
-	/**
-	 * Indicates whether the term is a coercion of integer to real (unary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIntToReal() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
-	}
-
-	/**
-	 * Indicates whether the term is a coercion of real to integer (unary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRealToInt() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
-	}
-
-	/**
-	 * Indicates whether the term is a check that tests whether a real is
-	 * integral (unary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRealIsInt() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
-	}
-
-	/**
-	 * Indicates whether the term is of an array sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isArray() throws Z3Exception
-	{
-		return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
-				.fromInt(Native.getSortKind(getContext().nCtx(),
-						Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
-	}
-
-	/**
-	 * Indicates whether the term is an array store. 
-	 * Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isStore() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
-	}
-
-	/**
-	 * Indicates whether the term is an array select.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSelect() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
-	}
-
-	/**
-	 * Indicates whether the term is a constant array. 
-	 * Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isConstantArray() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
-	}
-
-	/**
-	 * Indicates whether the term is a default array. 
-	 * Remarks: For example default(const(v)) = v. The function is unary.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isDefaultArray() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
-	}
-
-	/**
-	 * Indicates whether the term is an array map. 
-	 * Remarks: It satisfies
-	 * map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isArrayMap() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
-	}
-
-	/**
-	 * Indicates whether the term is an as-array term. 
-	 * Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isAsArray() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
-	}
-
-	/**
-	 * Indicates whether the term is set union
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSetUnion() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
-	}
-
-	/**
-	 * Indicates whether the term is set intersection
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSetIntersect() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
-	}
-
-	/**
-	 * Indicates whether the term is set difference
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSetDifference() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
-	}
-
-	/**
-	 * Indicates whether the term is set complement
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSetComplement() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
-	}
-
-	/**
-	 * Indicates whether the term is set subset
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isSetSubset() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
-	}
-
-	/**
-	 * Indicates whether the terms is of bit-vector sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBV() throws Z3Exception
-	{
-		return Native.getSortKind(getContext().nCtx(),
-				Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
-				.toInt();
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector numeral
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVNumeral() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
-	}
-
-	/**
-	 * Indicates whether the term is a one-bit bit-vector with value one
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVBitOne() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
-	}
-
-	/**
-	 * Indicates whether the term is a one-bit bit-vector with value zero
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVBitZero() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector unary minus
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVUMinus() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector addition (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVAdd() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector subtraction (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSub() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector multiplication (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVMul() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed division (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSDiv() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector unsigned division (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVUDiv() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed remainder (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSRem() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector unsigned remainder (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVURem() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed modulus
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSMod() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed division by zero
-	 * @return a boolean
-	 * @throws Z3Exception on error
-	 **/
-	boolean isBVSDiv0() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector unsigned division by zero
-	 * @return a boolean
-	 * @throws Z3Exception on error
-	 **/
-	boolean isBVUDiv0() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed remainder by zero
-	 * @return a boolean
-	 * @throws Z3Exception on error
-	 **/
-	boolean isBVSRem0() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector unsigned remainder by zero
-	 * @return a boolean
-	 * @throws Z3Exception on error
-	 **/
-	boolean isBVURem0() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector signed modulus by zero
-	 * @return a boolean
-	 * @throws Z3Exception on error
-	 **/
-	boolean isBVSMod0() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
-	}
-
-	/**
-	 * Indicates whether the term is an unsigned bit-vector less-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVULE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
-	}
-
-	/**
-	 * Indicates whether the term is a signed bit-vector less-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSLE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
-	}
-
-	/**
-	 * Indicates whether the term is an unsigned bit-vector
-	 * greater-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVUGE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
-	}
-
-	/**
-	 * Indicates whether the term is a signed bit-vector greater-than-or-equal
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSGE() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
-	}
-
-	/**
-	 * Indicates whether the term is an unsigned bit-vector less-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVULT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
-	}
-
-	/**
-	 * Indicates whether the term is a signed bit-vector less-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSLT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
-	}
-
-	/**
-	 * Indicates whether the term is an unsigned bit-vector greater-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVUGT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
-	}
-
-	/**
-	 * Indicates whether the term is a signed bit-vector greater-than
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSGT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise AND
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVAND() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise OR
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVOR() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise NOT
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVNOT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise XOR
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVXOR() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise NAND
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVNAND() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise NOR
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVNOR() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-wise XNOR
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVXNOR() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector concatenation (binary)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVConcat() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector sign extension
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVSignExtension() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector zero extension
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVZeroExtension() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector extraction
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVExtract() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector repetition
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVRepeat() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector reduce OR
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVReduceOR() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector reduce AND
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVReduceAND() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector comparison
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVComp() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector shift left
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVShiftLeft() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector logical shift right
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVShiftRightLogical() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector arithmetic shift left
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVShiftRightArithmetic() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector rotate left
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVRotateLeft() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector rotate right
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVRotateRight() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector rotate left (extended)
-	 * Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator
-	 * instead of a parametric one.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVRotateLeftExtended() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector rotate right (extended)
-	 * Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator
-	 * instead of a parametric one.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVRotateRightExtended() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
-	}
-
-	/**
-	 * Indicates whether the term is a coercion from integer to bit-vector
-	 * 
-	 * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIntToBV() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
-	}
-
-	/**
-	 * Indicates whether the term is a coercion from bit-vector to integer
-	 * 
-	 * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVToInt() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector carry 
-	 * Remarks: Compute the * carry bit in a full-adder. The meaning is given by the equivalence (carry * l1 l2 l3) &lt;=&gt; (or (and l1 l2) (and l1 l3) (and l2 l3)))
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVCarry() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
-	}
-
-	/**
-	 * Indicates whether the term is a bit-vector ternary XOR 
-	 * Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) &lt;=&gt; (xor (xor * l1 l2) l3)
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isBVXOR3() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
-	}
-
-	/**
-	 * Indicates whether the term is a label (used by the Boogie Verification
-	 * condition generator).
-	 * Remarks: The label has two parameters, a string and
-	 * a Boolean polarity. It takes one argument, a formula.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isLabel() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
-	}
-
-	/**
-	 * Indicates whether the term is a label literal (used by the Boogie
-	 * Verification condition generator).
-	 * Remarks: A label literal has a set of
-	 * string parameters. It takes no arguments.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isLabelLit() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
-	}
-
-	/**
-	 * Indicates whether the term is a binary equivalence modulo namings.
-	 * Remarks: This binary predicate is used in proof terms. It captures
-	 * equisatisfiability and equivalence modulo renamings.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isOEQ() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
-	}
-
-	/**
-	 * Indicates whether the term is a Proof for the expression 'true'.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofTrue() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for a fact asserted by the user.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofAsserted() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for a fact (tagged as goal)
-	 * asserted by the user.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofGoal() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
-	}
-
-	/**
-	 * Indicates whether the term is proof via modus ponens
-	 * Remarks:  Given a
-	 * proof for p and a proof for (implies p q), produces a proof for q. T1: p
-	 * T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a
-	 * proof for (iff p q).
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofModusPonens() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for (R t t), where R is a reflexive
-	 * relation.
-	 * Remarks: This proof object has no antecedents. The only
-	 * reflexive relations that are used are equivalence modulo namings,
-	 * equality and equivalence. That is, R is either '~', '=' or
-	 * 'iff'.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofReflexivity() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
-	}
-
-	/**
-	 * Indicates whether the term is proof by symmetricity of a relation
-	 * 
-	 * Remarks:  Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the * antecedent of this proof object. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofSymmetry() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by transitivity of a relation
-	 * 
-	 * Remarks:  Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: * (R t u) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofTransitivity() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by condensed transitivity of a
-	 * relation
-	 * Remarks:  Condensed transitivity proof. This proof object is
-	 * only used if the parameter PROOF_MODE is 1. It combines several symmetry
-	 * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
-	 * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
-	 * 
-	 * Assuming that this proof object is a proof for (R s t), then a proof
-	 * checker must check if it is possible to prove (R s t) using the
-	 * antecedents, symmetry and transitivity. That is, if there is a path from
-	 * s to t, if we view every antecedent (R a b) as an edge between a and b.
-	 * 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofTransitivityStar() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
-	}
-
-	/**
-	 * Indicates whether the term is a monotonicity proof object.
-	 * Remarks:  T1:
-	 * (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ...
-	 * t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is
-	 * suppressed. That is, reflexivity proofs are supressed to save space.
-	 * 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofMonotonicity() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
-	}
-
-	/**
-	 * Indicates whether the term is a quant-intro proof 
-	 * Remarks:  Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofQuantIntro() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
-	}
-
-	/**
-	 * Indicates whether the term is a distributivity proof object.
-	 * Remarks: 
-	 * Given that f (= or) distributes over g (= and), produces a proof for (=
-	 * (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof
-	 * also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c)
-	 * (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of
-	 * arguments.
-	 * 
-	 * This proof object has no antecedents. Remark. This rule is used by the
-	 * CNF conversion pass and instantiated by f = or, and g = and. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofDistributivity() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by elimination of AND 
-	 * Remarks:  * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofAndElimination() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by eliminiation of not-or 
-	 * Remarks:  * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofOrElimination() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by rewriting
-	 * Remarks:  A proof for
-	 * a local rewriting step (= t s). The head function symbol of t is
-	 * interpreted.
-	 * 
-	 * This proof object has no antecedents. The conclusion of a rewrite rule is
-	 * either an equality (= t s), an equivalence (iff t s), or
-	 * equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.
-	 * 
-	 * Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)
-	 * 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofRewrite() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by rewriting
-	 * Remarks:  A proof for
-	 * rewriting an expression t into an expression s. This proof object is used
-	 * if the parameter PROOF_MODE is 1. This proof object can have n
-	 * antecedents. The antecedents are proofs for equalities used as
-	 * substitution rules. The object is also used in a few cases if the
-	 * parameter PROOF_MODE is 2. The cases are: - When applying contextual
-	 * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
-	 * Booleans (BIT2BOOL=true) - When pulling ite expression up
-	 * (PULL_CHEAP_ITE_TREES=true) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofRewriteStar() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for pulling quantifiers out.
-	 * Remarks:  A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x)
-	 * r))). This proof object has no antecedents. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofPullQuant() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for pulling quantifiers out.
-	 * 
-	 * Remarks:  A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofPullQuantStar() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for pushing quantifiers in.
-	 * Remarks:  A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m]
-	 * ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ...
-	 * (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no
-	 * antecedents 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofPushQuant() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for elimination of unused
-	 * variables.
-	 * Remarks:  A proof for (iff (forall (x_1 ... x_n y_1 ... y_m)
-	 * p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))
-	 * 
-	 * It is used to justify the elimination of unused variables. This proof
-	 * object has no antecedents. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofElimUnusedVars() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for destructive equality resolution
-	 * Remarks:  A proof for destructive equality resolution: (iff (forall (x)
-	 * (or (not (= x t)) P[x])) P[t]) if x does not occur in t.
-	 * 
-	 * This proof object has no antecedents.
-	 * 
-	 * Several variables can be eliminated simultaneously. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofDER() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for quantifier instantiation
-	 * 
-	 * Remarks:  A proof of (or (not (forall (x) (P x))) (P a)) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofQuantInst() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
-	}
-
-	/**
-	 * Indicates whether the term is a hypthesis marker.
-	 * Remarks: Mark a
-	 * hypothesis in a natural deduction style proof.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofHypothesis() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by lemma
-	 * Remarks:  T1: false [lemma
-	 * T1]: (or (not l_1) ... (not l_n))
-	 * 
-	 * This proof object has one antecedent: a hypothetical proof for false. It
-	 * converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1
-	 * contains the hypotheses: l_1, ..., l_n. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofLemma() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by unit resolution 
-	 * Remarks:  T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofUnitResolution() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by iff-true
-	 * Remarks:  T1: p
-	 * [iff-true T1]: (iff p true) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofIFFTrue() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by iff-false
-	 * Remarks:  T1: (not p)
-	 * [iff-false T1]: (iff p false) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofIFFFalse() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by commutativity
-	 * Remarks:  [comm]:
-	 * (= (f a b) (f b a))
-	 * 
-	 * f is a commutative operator.
-	 * 
-	 * This proof object has no antecedents. Remark: if f is bool, then = is
-	 * iff. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofCommutativity() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for Tseitin-like axioms
-	 * Remarks: 
-	 * Proof object used to justify Tseitin's like axioms:
-	 * 
-	 * (or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p)
-	 * (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not
-	 * p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q)
-	 * (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q))
-	 * (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c))
-	 * (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b))
-	 * (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)
-	 * 
-	 * This proof object has no antecedents. Note: all axioms are propositional
-	 * tautologies. Note also that 'and' and 'or' can take multiple arguments.
-	 * You can recover the propositional tautologies by unfolding the Boolean
-	 * connectives in the axioms a small bounded number of steps (=3).
-	 * 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofDefAxiom() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for introduction of a name
-	 * Remarks:  Introduces a name for a formula/term. Suppose e is an
-	 * expression with free variables x, and def-intro introduces the name n(x).
-	 * The possible cases are:
-	 * 
-	 * When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n)
-	 * e))
-	 * 
-	 * or: [def-intro]: (or (not n) e) when e only occurs positively.
-	 * 
-	 * When e is of the form (ite cond th el): [def-intro]: (and (or (not cond)
-	 * (= n th)) (or cond (= n el)))
-	 * 
-	 * Otherwise: [def-intro]: (= n e) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofDefIntro() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for application of a definition
-	 * Remarks:  [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is
-	 * a proof that n is a name for F. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofApplyDef() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
-	}
-
-	/**
-	 * Indicates whether the term is a proof iff-oeq
-	 * Remarks:  T1: (iff p q)
-	 * [iff~ T1]: (~ p q) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofIFFOEQ() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for a positive NNF step
-	 * Remarks: 
-	 * Proof for a (positive) NNF step. Example:
-	 * 
-	 * T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'
-	 * [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1'
-	 * r_2)))
-	 * 
-	 * The negation normal form steps NNF_POS and NNF_NEG are used in the
-	 * following cases: (a) When creating the NNF of a positive force
-	 * quantifier. The quantifier is retained (unless the bound variables are
-	 * eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q)
-	 * (forall (x T) q_new))
-	 * 
-	 * (b) When recursively creating NNF over Boolean formulas, where the
-	 * top-level connective is changed during NNF conversion. The relevant
-	 * Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
-	 * NNF_NEG furthermore handles the case where negation is pushed over
-	 * Boolean connectives 'and' and 'or'. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofNNFPos() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for a negative NNF step
-	 * Remarks: 
-	 * Proof for a (negative) NNF step. Examples:
-	 * 
-	 * T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not
-	 * (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn:
-	 * (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1
-	 * ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4:
-	 * s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1
-	 * r_2) (or r_1' r_2'))) 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofNNFNeg() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for (~ P Q) here Q is in negation
-	 * normal form.
-	 * Remarks:  A proof for (~ P Q) where Q is in negation normal
-	 * form.
-	 * 
-	 * This proof object is only used if the parameter PROOF_MODE is 1.
-	 * 
-	 * This proof object may have n antecedents. Each antecedent is a
-	 * PR_DEF_INTRO. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofNNFStar() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for (~ P Q) where Q is in
-	 * conjunctive normal form.
-	 * Remarks:  A proof for (~ P Q) where Q is in
-	 * conjunctive normal form. This proof object is only used if the parameter
-	 * PROOF_MODE is 1. This proof object may have n antecedents. Each
-	 * antecedent is a PR_DEF_INTRO. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofCNFStar() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for a Skolemization step
-	 * Remarks: 
-	 * Proof for:
-	 * 
-	 * [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x
-	 * (p x y)) (p (sk y) y))
-	 * 
-	 * This proof object has no antecedents. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofSkolemize() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
-	}
-
-	/**
-	 * Indicates whether the term is a proof by modus ponens for
-	 * equi-satisfiability.
-	 * Remarks:  Modus ponens style rule for
-	 * equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofModusPonensOEQ() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
-	}
-
-	/**
-	 * Indicates whether the term is a proof for theory lemma
-	 * Remarks:  Generic
-	 * proof for theory lemmas.
-	 * 
-	 * The theory lemma function comes with one or more parameters. The first
-	 * parameter indicates the name of the theory. For the theory of arithmetic,
-	 * additional parameters provide hints for checking the theory lemma. The
-	 * hints for arithmetic are: - farkas - followed by rational coefficients.
-	 * Multiply the coefficients to the inequalities in the lemma, add the
-	 * (negated) inequalities and obtain a contradiction. - triangle-eq -
-	 * Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (&lt;=
-	 * t1 t2) (&lt;= t2 t1))) - gcd-test - Indicates an integer linear
-	 * arithmetic lemma that uses a gcd test. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isProofTheoryLemma() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
-	}
-
-	/**
-	 * Indicates whether the term is of an array sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelation() throws Z3Exception
-	{
-		return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
-				.getSortKind(getContext().nCtx(),
-						Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
-				.toInt());
-	}
-
-	/**
-	 * Indicates whether the term is an relation store
-	 * Remarks:  Insert a record
-	 * into a relation. The function takes {@code n+1} arguments, where the
-	 * first argument is the relation and the remaining {@code n} elements
-	 * correspond to the {@code n} columns of the relation. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationStore() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
-	}
-
-	/**
-	 * Indicates whether the term is an empty relation
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isEmptyRelation() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
-	}
-
-	/**
-	 * Indicates whether the term is a test for the emptiness of a relation
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isIsEmptyRelation() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
-	}
-
-	/**
-	 * Indicates whether the term is a relational join
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationalJoin() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
-	}
-
-	/**
-	 * Indicates whether the term is the union or convex hull of two relations.
-	 * 
-	 * Remarks: The function takes two arguments.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationUnion() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
-	}
-
-	/**
-	 * Indicates whether the term is the widening of two relations
-	 * Remarks: The
-	 * function takes two arguments.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationWiden() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
-	}
-
-	/**
-	 * Indicates whether the term is a projection of columns (provided as
-	 * numbers in the parameters).
-	 * Remarks: The function takes one
-	 * argument.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationProject() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
-	}
-
-	/**
-	 * Indicates whether the term is a relation filter
-	 * Remarks:  Filter
-	 * (restrict) a relation with respect to a predicate. The first argument is
-	 * a relation. The second argument is a predicate with free de-Brujin
-	 * indices corresponding to the columns of the relation. So the first column
-	 * in the relation has index 0. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationFilter() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
-	}
-
-	/**
-	 * Indicates whether the term is an intersection of a relation with the
-	 * negation of another.
-	 * Remarks:  Intersect the first relation with respect
-	 * to negation of the second relation (the function takes two arguments).
-	 * Logically, the specification can be described by a function
-	 * 
-	 * target = filter_by_negation(pos, neg, columns)
-	 * 
-	 * where columns are pairs c1, d1, .., cN, dN of columns from pos and neg,
-	 * such that target are elements in x in pos, such that there is no y in neg
-	 * that agrees with x on the columns c1, d1, .., cN, dN. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationNegationFilter() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
-	}
-
-	/**
-	 * Indicates whether the term is the renaming of a column in a relation
-	 * Remarks:  The function takes one argument. The parameters contain the
-	 * renaming as a cycle. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationRename() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
-	}
-
-	/**
-	 * Indicates whether the term is the complement of a relation
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationComplement() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
-	}
-
-	/**
-	 * Indicates whether the term is a relational select
-	 * Remarks:  Check if a
-	 * record is an element of the relation. The function takes {@code n+1}
-	 * arguments, where the first argument is a relation, and the remaining
-	 * {@code n} arguments correspond to a record. 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationSelect() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
-	}
-
-	/**
-	 * Indicates whether the term is a relational clone (copy)
-	 * Remarks:  Create
-	 * a fresh copy (clone) of a relation. The function is logically the
-	 * 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 
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isRelationClone() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
-	}
-
-	/**
-	 * Indicates whether the term is of an array sort.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isFiniteDomain() throws Z3Exception
-	{
-		return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
-				.getSortKind(getContext().nCtx(),
-						Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
-				.toInt());
-	}
-
-	/**
-	 * Indicates whether the term is a less than predicate over a finite domain.
-	 * @throws Z3Exception on error
-	 * @return a boolean
-	 **/
-	public boolean isFiniteDomainLT() throws Z3Exception
-	{
-		return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
-	}
-
-	/**
-	 * The de-Burijn index of a bound variable.
-	 * Remarks:  Bound variables are
-	 * indexed by de-Bruijn indices. It is perhaps easiest to explain the
-	 * meaning of de-Bruijn indices by indicating the compilation process from
-	 * non-de-Bruijn formulas to de-Bruijn format. {@code 
-	 * abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
-	 * abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
-	 * abs1(x, x, n) = b_n
-	 * abs1(y, x, n) = y
-	 * abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
-	 * abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
-	 * } The last line is significant: the index of a bound variable is
-	 * different depending on the scope in which it appears. The deeper x
-	 * appears, the higher is its index. 
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getIndex() throws Z3Exception
-	{
-		if (!isVar())
-			throw new Z3Exception("Term is not a bound variable.");
-
-		return Native.getIndexValue(getContext().nCtx(), getNativeObject());
-	}
-
-	/**
-	 * Constructor for Expr
-	 **/
-	protected Expr(Context ctx)
-	{
-		super(ctx);
-		{
-		}
-	}
-
-	/**
-	 * Constructor for Expr
-	 * @throws Z3Exception on error
-	 **/
-	protected Expr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-		{
-		}
-	}
-
-	void checkNativeObject(long obj) throws Z3Exception
-	{
-		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())
-		    throw new Z3Exception("Underlying object is not a term");
-		super.checkNativeObject(obj);
-	}
-
-	static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
-			throws Z3Exception
-	{
-		long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
-				AST.arrayLength(arguments), AST.arrayToNative(arguments));
-		return create(ctx, obj);
-	}
-
-	static Expr create(Context ctx, long obj) throws Z3Exception
-	{
-		Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
-		if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
-			return new Quantifier(ctx, obj);
-		long s = Native.getSort(ctx.nCtx(), obj);
-		Z3_sort_kind sk = Z3_sort_kind
-				.fromInt(Native.getSortKind(ctx.nCtx(), s));
-
-		if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
-			return new AlgebraicNum(ctx, obj);
-
-		if (Native.isNumeralAst(ctx.nCtx(), obj))
-		{
-			switch (sk)
-			{
-			case Z3_INT_SORT:
-				return new IntNum(ctx, obj);
-			case Z3_REAL_SORT:
-				return new RatNum(ctx, obj);
-			case Z3_BV_SORT:
-				return new BitVecNum(ctx, obj);
-			case Z3_FLOATING_POINT_SORT:
-				return new FPNum(ctx, obj);
-			case Z3_ROUNDING_MODE_SORT:
-				return new FPRMNum(ctx, obj);
-			default: ;
-			}
-		}
-
-		switch (sk)
-		{
-		case Z3_BOOL_SORT:
-			return new BoolExpr(ctx, obj);
-		case Z3_INT_SORT:
-			return new IntExpr(ctx, obj);
-		case Z3_REAL_SORT:
-			return new RealExpr(ctx, obj);
-		case Z3_BV_SORT:
-			return new BitVecExpr(ctx, obj);
-		case Z3_ARRAY_SORT:
-			return new ArrayExpr(ctx, obj);
-		case Z3_DATATYPE_SORT:
-			return new DatatypeExpr(ctx, obj);
-		case Z3_FLOATING_POINT_SORT:
-			return new FPExpr(ctx, obj);
-		case Z3_ROUNDING_MODE_SORT:
-			return new FPRMExpr(ctx, obj);
-		default: ;
-		}
-
-		return new Expr(ctx, obj);
-	}
+    /**
+     * Returns a simplified version of the expression
+     * @return Expr
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr simplify() throws Z3Exception
+    {
+        return simplify(null);
+    }
+
+    /**
+     * Returns a simplified version of the expression 
+     * A set of
+     * parameters 
+     * @param p a Params object to configure the simplifier 
+     * @see Context#SimplifyHelp
+     * @return an Expr
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr simplify(Params p) throws Z3Exception
+    {
+
+        if (p == null)
+            return Expr.create(getContext(),
+                    Native.simplify(getContext().nCtx(), getNativeObject()));
+        else
+            return Expr.create(
+                    getContext(),
+                    Native.simplifyEx(getContext().nCtx(), getNativeObject(),
+                            p.getNativeObject()));
+    }
+
+    /**
+     * The function declaration of the function that is applied in this
+     * expression.
+     * @return a FuncDecl
+     * @throws Z3Exception on error 
+     **/
+    public FuncDecl getFuncDecl() throws Z3Exception
+    {
+        return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
+                getNativeObject()));
+    }
+
+    /**
+     * Indicates whether the expression is the true or false expression or
+     * something else (Z3_L_UNDEF).
+     * @throws Z3Exception on error     
+     * @return a Z3_lbool
+     **/
+    public Z3_lbool getBoolValue() throws Z3Exception
+    {
+        return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
+                getNativeObject()));
+    }
+
+    /**
+     * The number of arguments of the expression.
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getNumArgs() throws Z3Exception
+    {
+        return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * The arguments of the expression.
+     * @throws Z3Exception on error
+     * @return an Expr[]
+     **/
+    public Expr[] getArgs() throws Z3Exception
+    {
+        int n = getNumArgs();
+        Expr[] res = new Expr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Expr.create(getContext(),
+                    Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
+        return res;
+    }
+
+    /**
+     * Update the arguments of the expression using the arguments {@code args}
+     * The number of new arguments should coincide with the
+     * current number of arguments.
+     * @param args arguments
+     * @throws Z3Exception on error
+     **/
+    public void update(Expr[] args) throws Z3Exception
+    {
+        getContext().checkContextMatch(args);
+        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)));
+    }
+
+    /**
+     * Substitute every occurrence of {@code from[i]} in the expression
+     * with {@code to[i]}, for {@code i} smaller than
+     * {@code num_exprs}. 
+     * Remarks: The result is the new expression. The
+     * arrays {@code from} and {@code to} must have size
+     * {@code num_exprs}. For every {@code i} smaller than
+     * {@code num_exprs}, we must have that sort of {@code from[i]}
+     * must be equal to sort of {@code to[i]}.
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr substitute(Expr[] from, Expr[] to) throws Z3Exception
+    {
+        getContext().checkContextMatch(from);
+        getContext().checkContextMatch(to);
+        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),
+                Expr.arrayToNative(to)));
+    }
+
+    /**
+     * Substitute every occurrence of {@code from} in the expression with
+     * {@code to}. 
+     * @see Expr#substitute(Expr[],Expr[])
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr substitute(Expr from, Expr to) throws Z3Exception
+    {
+
+        return substitute(new Expr[] { from }, new Expr[] { to });
+    }
+
+    /**
+     * Substitute the free variables in the expression with the expressions in
+     * {@code to} 
+     * Remarks:  For every {@code i} smaller than * {@code num_exprs}, the 
+     * variable with de-Bruijn index {@code i} * is replaced with term 
+     * {@code to[i]}.
+     * @throws Z3Exception on error 
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr substituteVars(Expr[] to) throws Z3Exception
+    {
+
+        getContext().checkContextMatch(to);
+        return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
+                getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
+    }
+
+    /**
+     * Translates (copies) the term to the Context {@code ctx}.
+     * 
+     * @param ctx A context
+     * 
+     * @return A copy of the term which is associated with {@code ctx}
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr translate(Context ctx) throws Z3Exception
+    {
+
+        if (getContext() == ctx)
+            return this;
+        else
+            return Expr.create(
+                    ctx,
+                    Native.translate(getContext().nCtx(), getNativeObject(),
+                            ctx.nCtx()));
+    }
+
+    /**
+     * Returns a string representation of the expression.
+     **/
+    public String toString()
+    {
+        return super.toString();
+    }
+
+    /**
+     * Indicates whether the term is a numeral
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isNumeral() throws Z3Exception
+    {
+        return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Indicates whether the term is well-sorted.
+     * 
+     * @return True if the term is well-sorted, false otherwise.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isWellSorted() throws Z3Exception
+    {
+        return Native.isWellSorted(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * The Sort of the term.
+     * @throws Z3Exception on error
+     * @return a sort
+     **/
+    public Sort getSort() throws Z3Exception
+    {
+        return Sort.create(getContext(),
+                Native.getSort(getContext().nCtx(), getNativeObject()));
+    }
+
+    /**
+     * Indicates whether the term represents a constant.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isConst() throws Z3Exception
+    {
+        return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
+    }
+
+    /**
+     * Indicates whether the term is an integer numeral.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIntNum() throws Z3Exception
+    {
+        return isNumeral() && isInt();
+    }
+
+    /**
+     * Indicates whether the term is a real numeral.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRatNum() throws Z3Exception
+    {
+        return isNumeral() && isReal();
+    }
+
+    /**
+     * Indicates whether the term is an algebraic number
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isAlgebraicNumber() throws Z3Exception
+    {
+        return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Indicates whether the term has Boolean sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBool() throws Z3Exception
+    {
+        return (isExpr() && Native.isEqSort(getContext().nCtx(),
+                Native.mkBoolSort(getContext().nCtx()),
+                Native.getSort(getContext().nCtx(), getNativeObject())));
+    }
+
+    /**
+     * Indicates whether the term is the constant true.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isTrue() throws Z3Exception
+    {
+            return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
+    }
+
+    /**
+     * Indicates whether the term is the constant false.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isFalse() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
+    }
+
+    /**
+     * Indicates whether the term is an equality predicate.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isEq() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
+    }
+
+    /**
+     * Indicates whether the term is an n-ary distinct predicate (every argument
+     * is mutually distinct).
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isDistinct() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
+    }
+
+    /**
+     * Indicates whether the term is a ternary if-then-else term
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isITE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
+    }
+
+    /**
+     * Indicates whether the term is an n-ary conjunction
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isAnd() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
+    }
+
+    /**
+     * Indicates whether the term is an n-ary disjunction
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isOr() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
+    }
+
+    /**
+     * Indicates whether the term is an if-and-only-if (Boolean equivalence,
+     * binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIff() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
+    }
+
+    /**
+     * Indicates whether the term is an exclusive or
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isXor() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
+    }
+
+    /**
+     * Indicates whether the term is a negation
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isNot() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
+    }
+
+    /**
+     * Indicates whether the term is an implication
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isImplies() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
+    }
+
+    /**
+     * Indicates whether the term is of integer sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isInt() throws Z3Exception
+    {
+        return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
+                .getSortKind(getContext().nCtx(),
+                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
+                .toInt());
+    }
+
+    /**
+     * Indicates whether the term is of sort real.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isReal() throws Z3Exception
+    {
+        return Native.getSortKind(getContext().nCtx(),
+                Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
+                .toInt();
+    }
+
+    /**
+     * Indicates whether the term is an arithmetic numeral.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isArithmeticNumeral() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
+    }
+
+    /**
+     * Indicates whether the term is a less-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isLE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
+    }
+
+    /**
+     * Indicates whether the term is a greater-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isGE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
+    }
+
+    /**
+     * Indicates whether the term is a less-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isLT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
+    }
+
+    /**
+     * Indicates whether the term is a greater-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isGT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
+    }
+
+    /**
+     * Indicates whether the term is addition (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isAdd() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
+    }
+
+    /**
+     * Indicates whether the term is subtraction (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSub() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
+    }
+
+    /**
+     * Indicates whether the term is a unary minus
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isUMinus() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
+    }
+
+    /**
+     * Indicates whether the term is multiplication (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isMul() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
+    }
+
+    /**
+     * Indicates whether the term is division (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isDiv() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
+    }
+
+    /**
+     * Indicates whether the term is integer division (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIDiv() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
+    }
+
+    /**
+     * Indicates whether the term is remainder (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRemainder() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
+    }
+
+    /**
+     * Indicates whether the term is modulus (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isModulus() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
+    }
+
+    /**
+     * Indicates whether the term is a coercion of integer to real (unary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIntToReal() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
+    }
+
+    /**
+     * Indicates whether the term is a coercion of real to integer (unary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRealToInt() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
+    }
+
+    /**
+     * Indicates whether the term is a check that tests whether a real is
+     * integral (unary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRealIsInt() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
+    }
+
+    /**
+     * Indicates whether the term is of an array sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isArray() throws Z3Exception
+    {
+        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
+                .fromInt(Native.getSortKind(getContext().nCtx(),
+                        Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
+    }
+
+    /**
+     * Indicates whether the term is an array store. 
+     * Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isStore() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
+    }
+
+    /**
+     * Indicates whether the term is an array select.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSelect() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
+    }
+
+    /**
+     * Indicates whether the term is a constant array. 
+     * Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isConstantArray() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
+    }
+
+    /**
+     * Indicates whether the term is a default array. 
+     * Remarks: For example default(const(v)) = v. The function is unary.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isDefaultArray() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
+    }
+
+    /**
+     * Indicates whether the term is an array map. 
+     * Remarks: It satisfies
+     * map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isArrayMap() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
+    }
+
+    /**
+     * Indicates whether the term is an as-array term. 
+     * Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isAsArray() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
+    }
+
+    /**
+     * Indicates whether the term is set union
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSetUnion() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
+    }
+
+    /**
+     * Indicates whether the term is set intersection
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSetIntersect() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
+    }
+
+    /**
+     * Indicates whether the term is set difference
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSetDifference() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
+    }
+
+    /**
+     * Indicates whether the term is set complement
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSetComplement() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
+    }
+
+    /**
+     * Indicates whether the term is set subset
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isSetSubset() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
+    }
+
+    /**
+     * Indicates whether the terms is of bit-vector sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBV() throws Z3Exception
+    {
+        return Native.getSortKind(getContext().nCtx(),
+                Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
+                .toInt();
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector numeral
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVNumeral() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
+    }
+
+    /**
+     * Indicates whether the term is a one-bit bit-vector with value one
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVBitOne() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
+    }
+
+    /**
+     * Indicates whether the term is a one-bit bit-vector with value zero
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVBitZero() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector unary minus
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVUMinus() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector addition (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVAdd() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector subtraction (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSub() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector multiplication (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVMul() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed division (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSDiv() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector unsigned division (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVUDiv() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed remainder (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSRem() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector unsigned remainder (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVURem() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed modulus
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSMod() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed division by zero
+     * @return a boolean
+     * @throws Z3Exception on error
+     **/
+    boolean isBVSDiv0() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector unsigned division by zero
+     * @return a boolean
+     * @throws Z3Exception on error
+     **/
+    boolean isBVUDiv0() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed remainder by zero
+     * @return a boolean
+     * @throws Z3Exception on error
+     **/
+    boolean isBVSRem0() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector unsigned remainder by zero
+     * @return a boolean
+     * @throws Z3Exception on error
+     **/
+    boolean isBVURem0() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector signed modulus by zero
+     * @return a boolean
+     * @throws Z3Exception on error
+     **/
+    boolean isBVSMod0() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
+    }
+
+    /**
+     * Indicates whether the term is an unsigned bit-vector less-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVULE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
+    }
+
+    /**
+     * Indicates whether the term is a signed bit-vector less-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSLE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
+    }
+
+    /**
+     * Indicates whether the term is an unsigned bit-vector
+     * greater-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVUGE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
+    }
+
+    /**
+     * Indicates whether the term is a signed bit-vector greater-than-or-equal
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSGE() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
+    }
+
+    /**
+     * Indicates whether the term is an unsigned bit-vector less-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVULT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
+    }
+
+    /**
+     * Indicates whether the term is a signed bit-vector less-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSLT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
+    }
+
+    /**
+     * Indicates whether the term is an unsigned bit-vector greater-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVUGT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
+    }
+
+    /**
+     * Indicates whether the term is a signed bit-vector greater-than
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSGT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise AND
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVAND() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise OR
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVOR() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise NOT
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVNOT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise XOR
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVXOR() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise NAND
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVNAND() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise NOR
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVNOR() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-wise XNOR
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVXNOR() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector concatenation (binary)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVConcat() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector sign extension
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVSignExtension() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector zero extension
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVZeroExtension() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector extraction
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVExtract() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector repetition
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVRepeat() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector reduce OR
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVReduceOR() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector reduce AND
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVReduceAND() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector comparison
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVComp() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector shift left
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVShiftLeft() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector logical shift right
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVShiftRightLogical() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector arithmetic shift left
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVShiftRightArithmetic() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector rotate left
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVRotateLeft() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector rotate right
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVRotateRight() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector rotate left (extended)
+     * Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator
+     * instead of a parametric one.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVRotateLeftExtended() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector rotate right (extended)
+     * Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator
+     * instead of a parametric one.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVRotateRightExtended() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
+    }
+
+    /**
+     * Indicates whether the term is a coercion from integer to bit-vector
+     * 
+     * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIntToBV() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
+    }
+
+    /**
+     * Indicates whether the term is a coercion from bit-vector to integer
+     * 
+     * Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVToInt() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector carry 
+     * Remarks: Compute the * carry bit in a full-adder. The meaning is given by the equivalence (carry * l1 l2 l3) &lt;=&gt; (or (and l1 l2) (and l1 l3) (and l2 l3)))
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVCarry() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
+    }
+
+    /**
+     * Indicates whether the term is a bit-vector ternary XOR 
+     * Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) &lt;=&gt; (xor (xor * l1 l2) l3)
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isBVXOR3() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
+    }
+
+    /**
+     * Indicates whether the term is a label (used by the Boogie Verification
+     * condition generator).
+     * Remarks: The label has two parameters, a string and
+     * a Boolean polarity. It takes one argument, a formula.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isLabel() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
+    }
+
+    /**
+     * Indicates whether the term is a label literal (used by the Boogie
+     * Verification condition generator).
+     * Remarks: A label literal has a set of
+     * string parameters. It takes no arguments.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isLabelLit() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
+    }
+
+    /**
+     * Indicates whether the term is a binary equivalence modulo namings.
+     * Remarks: This binary predicate is used in proof terms. It captures
+     * equisatisfiability and equivalence modulo renamings.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isOEQ() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
+    }
+
+    /**
+     * Indicates whether the term is a Proof for the expression 'true'.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofTrue() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
+    }
+
+    /**
+     * Indicates whether the term is a proof for a fact asserted by the user.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofAsserted() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
+    }
+
+    /**
+     * Indicates whether the term is a proof for a fact (tagged as goal)
+     * asserted by the user.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofGoal() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
+    }
+
+    /**
+     * Indicates whether the term is proof via modus ponens
+     * Remarks:  Given a
+     * proof for p and a proof for (implies p q), produces a proof for q. T1: p
+     * T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a
+     * proof for (iff p q).
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofModusPonens() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
+    }
+
+    /**
+     * Indicates whether the term is a proof for (R t t), where R is a reflexive
+     * relation.
+     * Remarks: This proof object has no antecedents. The only
+     * reflexive relations that are used are equivalence modulo namings,
+     * equality and equivalence. That is, R is either '~', '=' or
+     * 'iff'.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofReflexivity() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
+    }
+
+    /**
+     * Indicates whether the term is proof by symmetricity of a relation
+     * 
+     * Remarks:  Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the * antecedent of this proof object. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofSymmetry() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
+    }
+
+    /**
+     * Indicates whether the term is a proof by transitivity of a relation
+     * 
+     * Remarks:  Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: * (R t u) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofTransitivity() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
+    }
+
+    /**
+     * Indicates whether the term is a proof by condensed transitivity of a
+     * relation
+     * Remarks:  Condensed transitivity proof. This proof object is
+     * only used if the parameter PROOF_MODE is 1. It combines several symmetry
+     * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
+     * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
+     * 
+     * Assuming that this proof object is a proof for (R s t), then a proof
+     * checker must check if it is possible to prove (R s t) using the
+     * antecedents, symmetry and transitivity. That is, if there is a path from
+     * s to t, if we view every antecedent (R a b) as an edge between a and b.
+     * 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofTransitivityStar() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
+    }
+
+    /**
+     * Indicates whether the term is a monotonicity proof object.
+     * Remarks:  T1:
+     * (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ...
+     * t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is
+     * suppressed. That is, reflexivity proofs are supressed to save space.
+     * 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofMonotonicity() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
+    }
+
+    /**
+     * Indicates whether the term is a quant-intro proof 
+     * Remarks:  Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofQuantIntro() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
+    }
+
+    /**
+     * Indicates whether the term is a distributivity proof object.
+     * Remarks: 
+     * Given that f (= or) distributes over g (= and), produces a proof for (=
+     * (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof
+     * also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c)
+     * (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of
+     * arguments.
+     * 
+     * This proof object has no antecedents. Remark. This rule is used by the
+     * CNF conversion pass and instantiated by f = or, and g = and. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofDistributivity() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
+    }
+
+    /**
+     * Indicates whether the term is a proof by elimination of AND 
+     * Remarks:  * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofAndElimination() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
+    }
+
+    /**
+     * Indicates whether the term is a proof by eliminiation of not-or 
+     * Remarks:  * Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). * T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofOrElimination() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
+    }
+
+    /**
+     * Indicates whether the term is a proof by rewriting
+     * Remarks:  A proof for
+     * a local rewriting step (= t s). The head function symbol of t is
+     * interpreted.
+     * 
+     * This proof object has no antecedents. The conclusion of a rewrite rule is
+     * either an equality (= t s), an equivalence (iff t s), or
+     * equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.
+     * 
+     * Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)
+     * 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofRewrite() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
+    }
+
+    /**
+     * Indicates whether the term is a proof by rewriting
+     * Remarks:  A proof for
+     * rewriting an expression t into an expression s. This proof object is used
+     * if the parameter PROOF_MODE is 1. This proof object can have n
+     * antecedents. The antecedents are proofs for equalities used as
+     * substitution rules. The object is also used in a few cases if the
+     * parameter PROOF_MODE is 2. The cases are: - When applying contextual
+     * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
+     * Booleans (BIT2BOOL=true) - When pulling ite expression up
+     * (PULL_CHEAP_ITE_TREES=true) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofRewriteStar() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
+    }
+
+    /**
+     * Indicates whether the term is a proof for pulling quantifiers out.
+     * Remarks:  A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x)
+     * r))). This proof object has no antecedents. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofPullQuant() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
+    }
+
+    /**
+     * Indicates whether the term is a proof for pulling quantifiers out.
+     * 
+     * Remarks:  A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofPullQuantStar() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
+    }
+
+    /**
+     * Indicates whether the term is a proof for pushing quantifiers in.
+     * Remarks:  A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m]
+     * ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ...
+     * (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no
+     * antecedents 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofPushQuant() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
+    }
+
+    /**
+     * Indicates whether the term is a proof for elimination of unused
+     * variables.
+     * Remarks:  A proof for (iff (forall (x_1 ... x_n y_1 ... y_m)
+     * p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))
+     * 
+     * It is used to justify the elimination of unused variables. This proof
+     * object has no antecedents. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofElimUnusedVars() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
+    }
+
+    /**
+     * Indicates whether the term is a proof for destructive equality resolution
+     * Remarks:  A proof for destructive equality resolution: (iff (forall (x)
+     * (or (not (= x t)) P[x])) P[t]) if x does not occur in t.
+     * 
+     * This proof object has no antecedents.
+     * 
+     * Several variables can be eliminated simultaneously. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofDER() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
+    }
+
+    /**
+     * Indicates whether the term is a proof for quantifier instantiation
+     * 
+     * Remarks:  A proof of (or (not (forall (x) (P x))) (P a)) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofQuantInst() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
+    }
+
+    /**
+     * Indicates whether the term is a hypthesis marker.
+     * Remarks: Mark a
+     * hypothesis in a natural deduction style proof.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofHypothesis() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
+    }
+
+    /**
+     * Indicates whether the term is a proof by lemma
+     * Remarks:  T1: false [lemma
+     * T1]: (or (not l_1) ... (not l_n))
+     * 
+     * This proof object has one antecedent: a hypothetical proof for false. It
+     * converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1
+     * contains the hypotheses: l_1, ..., l_n. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofLemma() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
+    }
+
+    /**
+     * Indicates whether the term is a proof by unit resolution 
+     * Remarks:  T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) * [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofUnitResolution() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
+    }
+
+    /**
+     * Indicates whether the term is a proof by iff-true
+     * Remarks:  T1: p
+     * [iff-true T1]: (iff p true) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofIFFTrue() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
+    }
+
+    /**
+     * Indicates whether the term is a proof by iff-false
+     * Remarks:  T1: (not p)
+     * [iff-false T1]: (iff p false) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofIFFFalse() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
+    }
+
+    /**
+     * Indicates whether the term is a proof by commutativity
+     * Remarks:  [comm]:
+     * (= (f a b) (f b a))
+     * 
+     * f is a commutative operator.
+     * 
+     * This proof object has no antecedents. Remark: if f is bool, then = is
+     * iff. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofCommutativity() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
+    }
+
+    /**
+     * Indicates whether the term is a proof for Tseitin-like axioms
+     * Remarks: 
+     * Proof object used to justify Tseitin's like axioms:
+     * 
+     * (or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p)
+     * (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not
+     * p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q)
+     * (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q))
+     * (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c))
+     * (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b))
+     * (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)
+     * 
+     * This proof object has no antecedents. Note: all axioms are propositional
+     * tautologies. Note also that 'and' and 'or' can take multiple arguments.
+     * You can recover the propositional tautologies by unfolding the Boolean
+     * connectives in the axioms a small bounded number of steps (=3).
+     * 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofDefAxiom() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
+    }
+
+    /**
+     * Indicates whether the term is a proof for introduction of a name
+     * Remarks:  Introduces a name for a formula/term. Suppose e is an
+     * expression with free variables x, and def-intro introduces the name n(x).
+     * The possible cases are:
+     * 
+     * When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n)
+     * e))
+     * 
+     * or: [def-intro]: (or (not n) e) when e only occurs positively.
+     * 
+     * When e is of the form (ite cond th el): [def-intro]: (and (or (not cond)
+     * (= n th)) (or cond (= n el)))
+     * 
+     * Otherwise: [def-intro]: (= n e) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofDefIntro() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
+    }
+
+    /**
+     * Indicates whether the term is a proof for application of a definition
+     * Remarks:  [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is
+     * a proof that n is a name for F. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofApplyDef() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
+    }
+
+    /**
+     * Indicates whether the term is a proof iff-oeq
+     * Remarks:  T1: (iff p q)
+     * [iff~ T1]: (~ p q) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofIFFOEQ() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
+    }
+
+    /**
+     * Indicates whether the term is a proof for a positive NNF step
+     * Remarks: 
+     * Proof for a (positive) NNF step. Example:
+     * 
+     * T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'
+     * [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1'
+     * r_2)))
+     * 
+     * The negation normal form steps NNF_POS and NNF_NEG are used in the
+     * following cases: (a) When creating the NNF of a positive force
+     * quantifier. The quantifier is retained (unless the bound variables are
+     * eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q)
+     * (forall (x T) q_new))
+     * 
+     * (b) When recursively creating NNF over Boolean formulas, where the
+     * top-level connective is changed during NNF conversion. The relevant
+     * Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
+     * NNF_NEG furthermore handles the case where negation is pushed over
+     * Boolean connectives 'and' and 'or'. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofNNFPos() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
+    }
+
+    /**
+     * Indicates whether the term is a proof for a negative NNF step
+     * Remarks: 
+     * Proof for a (negative) NNF step. Examples:
+     * 
+     * T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not
+     * (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn:
+     * (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1
+     * ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4:
+     * s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1
+     * r_2) (or r_1' r_2'))) 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofNNFNeg() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
+    }
+
+    /**
+     * Indicates whether the term is a proof for (~ P Q) here Q is in negation
+     * normal form.
+     * Remarks:  A proof for (~ P Q) where Q is in negation normal
+     * form.
+     * 
+     * This proof object is only used if the parameter PROOF_MODE is 1.
+     * 
+     * This proof object may have n antecedents. Each antecedent is a
+     * PR_DEF_INTRO. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofNNFStar() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
+    }
+
+    /**
+     * Indicates whether the term is a proof for (~ P Q) where Q is in
+     * conjunctive normal form.
+     * Remarks:  A proof for (~ P Q) where Q is in
+     * conjunctive normal form. This proof object is only used if the parameter
+     * PROOF_MODE is 1. This proof object may have n antecedents. Each
+     * antecedent is a PR_DEF_INTRO. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofCNFStar() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
+    }
+
+    /**
+     * Indicates whether the term is a proof for a Skolemization step
+     * Remarks: 
+     * Proof for:
+     * 
+     * [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x
+     * (p x y)) (p (sk y) y))
+     * 
+     * This proof object has no antecedents. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofSkolemize() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
+    }
+
+    /**
+     * Indicates whether the term is a proof by modus ponens for
+     * equi-satisfiability.
+     * Remarks:  Modus ponens style rule for
+     * equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofModusPonensOEQ() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
+    }
+
+    /**
+     * Indicates whether the term is a proof for theory lemma
+     * Remarks:  Generic
+     * proof for theory lemmas.
+     * 
+     * The theory lemma function comes with one or more parameters. The first
+     * parameter indicates the name of the theory. For the theory of arithmetic,
+     * additional parameters provide hints for checking the theory lemma. The
+     * hints for arithmetic are: - farkas - followed by rational coefficients.
+     * Multiply the coefficients to the inequalities in the lemma, add the
+     * (negated) inequalities and obtain a contradiction. - triangle-eq -
+     * Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (&lt;=
+     * t1 t2) (&lt;= t2 t1))) - gcd-test - Indicates an integer linear
+     * arithmetic lemma that uses a gcd test. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isProofTheoryLemma() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
+    }
+
+    /**
+     * Indicates whether the term is of an array sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelation() throws Z3Exception
+    {
+        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
+                .getSortKind(getContext().nCtx(),
+                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
+                .toInt());
+    }
+
+    /**
+     * Indicates whether the term is an relation store
+     * Remarks:  Insert a record
+     * into a relation. The function takes {@code n+1} arguments, where the
+     * first argument is the relation and the remaining {@code n} elements
+     * correspond to the {@code n} columns of the relation. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationStore() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
+    }
+
+    /**
+     * Indicates whether the term is an empty relation
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isEmptyRelation() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
+    }
+
+    /**
+     * Indicates whether the term is a test for the emptiness of a relation
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isIsEmptyRelation() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
+    }
+
+    /**
+     * Indicates whether the term is a relational join
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationalJoin() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
+    }
+
+    /**
+     * Indicates whether the term is the union or convex hull of two relations.
+     * 
+     * Remarks: The function takes two arguments.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationUnion() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
+    }
+
+    /**
+     * Indicates whether the term is the widening of two relations
+     * Remarks: The
+     * function takes two arguments.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationWiden() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
+    }
+
+    /**
+     * Indicates whether the term is a projection of columns (provided as
+     * numbers in the parameters).
+     * Remarks: The function takes one
+     * argument.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationProject() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
+    }
+
+    /**
+     * Indicates whether the term is a relation filter
+     * Remarks:  Filter
+     * (restrict) a relation with respect to a predicate. The first argument is
+     * a relation. The second argument is a predicate with free de-Brujin
+     * indices corresponding to the columns of the relation. So the first column
+     * in the relation has index 0. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationFilter() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
+    }
+
+    /**
+     * Indicates whether the term is an intersection of a relation with the
+     * negation of another.
+     * Remarks:  Intersect the first relation with respect
+     * to negation of the second relation (the function takes two arguments).
+     * Logically, the specification can be described by a function
+     * 
+     * target = filter_by_negation(pos, neg, columns)
+     * 
+     * where columns are pairs c1, d1, .., cN, dN of columns from pos and neg,
+     * such that target are elements in x in pos, such that there is no y in neg
+     * that agrees with x on the columns c1, d1, .., cN, dN. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationNegationFilter() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
+    }
+
+    /**
+     * Indicates whether the term is the renaming of a column in a relation
+     * Remarks:  The function takes one argument. The parameters contain the
+     * renaming as a cycle. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationRename() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
+    }
+
+    /**
+     * Indicates whether the term is the complement of a relation
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationComplement() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
+    }
+
+    /**
+     * Indicates whether the term is a relational select
+     * Remarks:  Check if a
+     * record is an element of the relation. The function takes {@code n+1}
+     * arguments, where the first argument is a relation, and the remaining
+     * {@code n} arguments correspond to a record. 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationSelect() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
+    }
+
+    /**
+     * Indicates whether the term is a relational clone (copy)
+     * Remarks:  Create
+     * a fresh copy (clone) of a relation. The function is logically the
+     * 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 
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isRelationClone() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
+    }
+
+    /**
+     * Indicates whether the term is of an array sort.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isFiniteDomain() throws Z3Exception
+    {
+        return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
+                .getSortKind(getContext().nCtx(),
+                        Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
+                .toInt());
+    }
+
+    /**
+     * Indicates whether the term is a less than predicate over a finite domain.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isFiniteDomainLT() throws Z3Exception
+    {
+        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
+    }
+
+    /**
+     * The de-Burijn index of a bound variable.
+     * Remarks:  Bound variables are
+     * indexed by de-Bruijn indices. It is perhaps easiest to explain the
+     * meaning of de-Bruijn indices by indicating the compilation process from
+     * non-de-Bruijn formulas to de-Bruijn format. {@code 
+     * abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
+     * abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
+     * abs1(x, x, n) = b_n
+     * abs1(y, x, n) = y
+     * abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
+     * abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
+     * } The last line is significant: the index of a bound variable is
+     * different depending on the scope in which it appears. The deeper x
+     * appears, the higher is its index. 
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getIndex() throws Z3Exception
+    {
+        if (!isVar())
+            throw new Z3Exception("Term is not a bound variable.");
+
+        return Native.getIndexValue(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Constructor for Expr
+     **/
+    protected Expr(Context ctx)
+    {
+        super(ctx);
+        {
+        }
+    }
+
+    /**
+     * Constructor for Expr
+     * @throws Z3Exception on error
+     **/
+    protected Expr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+        {
+        }
+    }
+
+    void checkNativeObject(long obj) throws Z3Exception
+    {
+        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())
+            throw new Z3Exception("Underlying object is not a term");
+        super.checkNativeObject(obj);
+    }
+
+    static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
+            throws Z3Exception
+    {
+        long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
+                AST.arrayLength(arguments), AST.arrayToNative(arguments));
+        return create(ctx, obj);
+    }
+
+    static Expr create(Context ctx, long obj) throws Z3Exception
+    {
+        Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
+        if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
+            return new Quantifier(ctx, obj);
+        long s = Native.getSort(ctx.nCtx(), obj);
+        Z3_sort_kind sk = Z3_sort_kind
+                .fromInt(Native.getSortKind(ctx.nCtx(), s));
+
+        if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast?
+            return new AlgebraicNum(ctx, obj);
+
+        if (Native.isNumeralAst(ctx.nCtx(), obj))
+        {
+            switch (sk)
+            {
+            case Z3_INT_SORT:
+                return new IntNum(ctx, obj);
+            case Z3_REAL_SORT:
+                return new RatNum(ctx, obj);
+            case Z3_BV_SORT:
+                return new BitVecNum(ctx, obj);
+            case Z3_FLOATING_POINT_SORT:
+                return new FPNum(ctx, obj);
+            case Z3_ROUNDING_MODE_SORT:
+                return new FPRMNum(ctx, obj);
+            default: ;
+            }
+        }
+
+        switch (sk)
+        {
+        case Z3_BOOL_SORT:
+            return new BoolExpr(ctx, obj);
+        case Z3_INT_SORT:
+            return new IntExpr(ctx, obj);
+        case Z3_REAL_SORT:
+            return new RealExpr(ctx, obj);
+        case Z3_BV_SORT:
+            return new BitVecExpr(ctx, obj);
+        case Z3_ARRAY_SORT:
+            return new ArrayExpr(ctx, obj);
+        case Z3_DATATYPE_SORT:
+            return new DatatypeExpr(ctx, obj);
+        case Z3_FLOATING_POINT_SORT:
+            return new FPExpr(ctx, obj);
+        case Z3_ROUNDING_MODE_SORT:
+            return new FPRMExpr(ctx, obj);
+        default: ;
+        }
+
+        return new Expr(ctx, obj);
+    }
 }
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
index 037fe63a4..8ac2eae2b 100644
--- a/src/api/java/FPNum.java
+++ b/src/api/java/FPNum.java
@@ -21,13 +21,13 @@ package com.microsoft.z3;
  */
 public class FPNum extends FPExpr
 {
-	/**
-	 * Retrieves the sign of a floating-point literal	 
+    /**
+     * Retrieves the sign of a floating-point literal     
      * Remarks: returns true if the numeral is negative 
-	 * @throws Z3Exception 
+     * @throws Z3Exception 
      */
     public boolean getSign() throws Z3Exception {
-    	Native.IntPtr res = new Native.IntPtr();
+        Native.IntPtr res = new Native.IntPtr();
         if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true)                
             throw new Z3Exception("Sign is not a Boolean value");
         return res.value != 0;
diff --git a/src/api/java/FPRMNum.java b/src/api/java/FPRMNum.java
index 04e7727e2..86ee3c97e 100644
--- a/src/api/java/FPRMNum.java
+++ b/src/api/java/FPRMNum.java
@@ -23,7 +23,7 @@ import com.microsoft.z3.enumerations.Z3_decl_kind;
  */
 public class FPRMNum extends FPRMExpr {
 
-	/**
+    /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
      * @throws Z3Exception 
      * **/
@@ -83,8 +83,8 @@ public class FPRMNum extends FPRMExpr {
      */
     public boolean isRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
     
-	public FPRMNum(Context ctx, long obj) throws Z3Exception {
-		super(ctx, obj);
-	}
+    public FPRMNum(Context ctx, long obj) throws Z3Exception {
+        super(ctx, obj);
+    }
 
 }
diff --git a/src/api/java/FPSort.java b/src/api/java/FPSort.java
index 284979524..e9bfc94c4 100644
--- a/src/api/java/FPSort.java
+++ b/src/api/java/FPSort.java
@@ -28,22 +28,22 @@ public class FPSort extends Sort
     }
     
     public FPSort(Context ctx, int ebits, int sbits) throws Z3Exception
-	{
-    	super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));	    
-	}
+    {
+        super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));        
+    }
     
     /**
      * The number of exponent bits.
      */
     public int getEBits() throws Z3Exception {
-    	return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());    	
+        return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
     }
     
     /**
      * The number of significand bits.
      */
     public int getSBits() throws Z3Exception {
-    	return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());    	
+        return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
     }
     
 }
diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java
index cece06f1a..b275cce87 100644
--- a/src/api/java/FiniteDomainSort.java
+++ b/src/api/java/FiniteDomainSort.java
@@ -22,25 +22,25 @@ package com.microsoft.z3;
  **/
 public class FiniteDomainSort extends Sort
 {
-	/**
-	 * The size of the finite domain sort.
-	 * @throws Z3Exception on error
-	 **/
-	public long getSize() throws Z3Exception
-	{
-		Native.LongPtr res = new Native.LongPtr();
-		Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
-		return res.value;
-	}
+    /**
+     * The size of the finite domain sort.
+     * @throws Z3Exception on error
+     **/
+    public long getSize() throws Z3Exception
+    {
+        Native.LongPtr res = new Native.LongPtr();
+        Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
+        return res.value;
+    }
 
-	FiniteDomainSort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    FiniteDomainSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	FiniteDomainSort(Context ctx, Symbol name, long size) throws Z3Exception
-	{
-		super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
-				size));
-	}
+    FiniteDomainSort(Context ctx, Symbol name, long size) throws Z3Exception
+    {
+        super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
+                size));
+    }
 }
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 8504392bf..808785ddc 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() throws Z3Exception
     {
@@ -173,10 +173,10 @@ public class Fixedpoint extends Z3Object
 
     /**
      * Backtrack one backtracking point.
-	 * Remarks: Note that an exception is thrown if {@code pop} 
-	 * is called without a corresponding {@code push}
+     * Remarks: Note that an exception is thrown if {@code pop} 
+     * is called without a corresponding {@code push}
      *  
-	 * @see push
+     * @see push
      **/
     public void pop() throws Z3Exception
     {
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index 2ea40dd2c..da2af3a41 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class FixedpointDecRefQueue extends IDecRefQueue
 {
+    public FixedpointDecRefQueue() 
+    {
+        super();
+    }
+
+    public FixedpointDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 5307951e5..e9b05f08c 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -93,7 +93,7 @@ public class FuncDecl extends AST
 
     /**
      * The size of the domain of the function declaration 
-	 * @see getArity
+     * @see getArity
      **/
     public int getDomainSize() throws Z3Exception
     {
@@ -376,7 +376,7 @@ public class FuncDecl extends AST
 
     /**
      * Create expression that applies function to arguments. 
-	 * @param args 
+     * @param args 
      * 
      * @return
      **/
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index fd0c10d2e..7fb5ac13e 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -24,183 +24,183 @@ package com.microsoft.z3;
  **/
 public class FuncInterp extends Z3Object
 {
-	/**
-	 * An Entry object represents an element in the finite map used to encode a
-	 * function interpretation.
-	 **/
-	public class Entry extends Z3Object
-	{
-		/**
-		 * Return the (symbolic) value of this entry.
-		 * 
-		 * @throws Z3Exception
-		 * @throws Z3Exception on error
-	 **/
-		public Expr getValue() throws Z3Exception
-		{
-			return Expr.create(getContext(),
-					Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
-		}
+    /**
+     * An Entry object represents an element in the finite map used to encode a
+     * function interpretation.
+     **/
+    public class Entry extends Z3Object
+    {
+        /**
+         * Return the (symbolic) value of this entry.
+         * 
+         * @throws Z3Exception
+         * @throws Z3Exception on error
+     **/
+        public Expr getValue() throws Z3Exception
+        {
+            return Expr.create(getContext(),
+                    Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
+        }
 
-		/**
-		 * The number of arguments of the entry.
-		 * @throws Z3Exception on error
-	 **/
-		public int getNumArgs() throws Z3Exception
-		{
-			return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
-		}
+        /**
+         * The number of arguments of the entry.
+         * @throws Z3Exception on error
+     **/
+        public int getNumArgs() throws Z3Exception
+        {
+            return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
+        }
 
-		/**
-		 * The arguments of the function entry.
-		 * 
-		 * @throws Z3Exception
-		 * @throws Z3Exception on error
-	 **/
-		public Expr[] getArgs() throws Z3Exception
-		{
-			int n = getNumArgs();
-			Expr[] res = new Expr[n];
-			for (int i = 0; i < n; i++)
-				res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
-						getContext().nCtx(), getNativeObject(), i));
-			return res;
-		}
+        /**
+         * The arguments of the function entry.
+         * 
+         * @throws Z3Exception
+         * @throws Z3Exception on error
+     **/
+        public Expr[] getArgs() throws Z3Exception
+        {
+            int n = getNumArgs();
+            Expr[] res = new Expr[n];
+            for (int i = 0; i < n; i++)
+                res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
+                        getContext().nCtx(), getNativeObject(), i));
+            return res;
+        }
 
-		/**
-		 * A string representation of the function entry.
-		 **/
-		public String toString()
-		{
-			try
-			{
-				int n = getNumArgs();
-				String res = "[";
-				Expr[] args = getArgs();
-				for (int i = 0; i < n; i++)
-					res += args[i] + ", ";
-				return res + getValue() + "]";
-			} catch (Z3Exception e)
-			{
-				return new String("Z3Exception: " + e.getMessage());
-			}
-		}
+        /**
+         * A string representation of the function entry.
+         **/
+        public String toString()
+        {
+            try
+            {
+                int n = getNumArgs();
+                String res = "[";
+                Expr[] args = getArgs();
+                for (int i = 0; i < n; i++)
+                    res += args[i] + ", ";
+                return res + getValue() + "]";
+            } catch (Z3Exception e)
+            {
+                return new String("Z3Exception: " + e.getMessage());
+            }
+        }
 
-		Entry(Context ctx, long obj) throws Z3Exception
-		{
-			super(ctx, obj);
-		}
+        Entry(Context ctx, long obj) throws Z3Exception
+        {
+            super(ctx, obj);
+        }
 
-		void incRef(long o) throws Z3Exception
-		{
-			getContext().funcEntry_DRQ().incAndClear(getContext(), o);
-			super.incRef(o);
-		}
+        void incRef(long o) throws Z3Exception
+        {
+            getContext().funcEntry_DRQ().incAndClear(getContext(), o);
+            super.incRef(o);
+        }
 
-		void decRef(long o) throws Z3Exception
-		{
-			getContext().funcEntry_DRQ().add(o);
-			super.decRef(o);
-		}
-	};
+        void decRef(long o) throws Z3Exception
+        {
+            getContext().funcEntry_DRQ().add(o);
+            super.decRef(o);
+        }
+    };
 
-	/**
-	 * The number of entries in the function interpretation.
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getNumEntries() throws Z3Exception
-	{
-		return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
-	}
+    /**
+     * The number of entries in the function interpretation.
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getNumEntries() throws Z3Exception
+    {
+        return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
+    }
 
-	/**
-	 * The entries in the function interpretation
-	 * 
-	 * @throws Z3Exception
-	 * @throws Z3Exception on error
-	 **/
-	public Entry[] getEntries() throws Z3Exception
-	{
-		int n = getNumEntries();
-		Entry[] res = new Entry[n];
-		for (int i = 0; i < n; i++)
-			res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
-					.nCtx(), getNativeObject(), i));
-		return res;
-	}
+    /**
+     * The entries in the function interpretation
+     * 
+     * @throws Z3Exception
+     * @throws Z3Exception on error
+     **/
+    public Entry[] getEntries() throws Z3Exception
+    {
+        int n = getNumEntries();
+        Entry[] res = new Entry[n];
+        for (int i = 0; i < n; i++)
+            res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
+                    .nCtx(), getNativeObject(), i));
+        return res;
+    }
 
-	/**
-	 * The (symbolic) `else' value of the function interpretation.
-	 * 
-	 * @throws Z3Exception
-	 * @throws Z3Exception on error
-	 * @return an Expr
-	 **/
-	public Expr getElse() throws Z3Exception
-	{
-		return Expr.create(getContext(),
-				Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
-	}
+    /**
+     * The (symbolic) `else' value of the function interpretation.
+     * 
+     * @throws Z3Exception
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr getElse() throws Z3Exception
+    {
+        return Expr.create(getContext(),
+                Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
+    }
 
-	/**
-	 * The arity of the function interpretation
-	 * @throws Z3Exception on error
-	 * @return an int
-	 **/
-	public int getArity() throws Z3Exception
-	{
-		return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
-	}
+    /**
+     * The arity of the function interpretation
+     * @throws Z3Exception on error
+     * @return an int
+     **/
+    public int getArity() throws Z3Exception
+    {
+        return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
+    }
 
-	/**
-	 * A string representation of the function interpretation.
-	 **/
-	public String toString()
-	{
-		try
-		{
-			String res = "";
-			res += "[";
-			for (Entry e : getEntries())
-			{
-				int n = e.getNumArgs();
-				if (n > 1)
-					res += "[";
-				Expr[] args = e.getArgs();
-				for (int i = 0; i < n; i++)
-				{
-					if (i != 0)
-						res += ", ";
-					res += args[i];
-				}
-				if (n > 1)
-					res += "]";
-				res += " -> " + e.getValue() + ", ";
-			}
-			res += "else -> " + getElse();
-			res += "]";
-			return res;
-		} catch (Z3Exception e)
-		{
-			return new String("Z3Exception: " + e.getMessage());
-		}
-	}
+    /**
+     * A string representation of the function interpretation.
+     **/
+    public String toString()
+    {
+        try
+        {
+            String res = "";
+            res += "[";
+            for (Entry e : getEntries())
+            {
+                int n = e.getNumArgs();
+                if (n > 1)
+                    res += "[";
+                Expr[] args = e.getArgs();
+                for (int i = 0; i < n; i++)
+                {
+                    if (i != 0)
+                        res += ", ";
+                    res += args[i];
+                }
+                if (n > 1)
+                    res += "]";
+                res += " -> " + e.getValue() + ", ";
+            }
+            res += "else -> " + getElse();
+            res += "]";
+            return res;
+        } catch (Z3Exception e)
+        {
+            return new String("Z3Exception: " + e.getMessage());
+        }
+    }
 
-	FuncInterp(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    FuncInterp(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	void incRef(long o) throws Z3Exception
-	{
-		getContext().funcInterp_DRQ().incAndClear(getContext(), o);
-		super.incRef(o);
-	}
+    void incRef(long o) throws Z3Exception
+    {
+        getContext().funcInterp_DRQ().incAndClear(getContext(), o);
+        super.incRef(o);
+    }
 
-	void decRef(long o) throws Z3Exception
-	{
-		getContext().funcInterp_DRQ().add(o);
-		super.decRef(o);
-	}
+    void decRef(long o) throws Z3Exception
+    {
+        getContext().funcInterp_DRQ().add(o);
+        super.decRef(o);
+    }
 }
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index 8bdad4ad5..56660d2f9 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class FuncInterpDecRefQueue extends IDecRefQueue
 {
+    public FuncInterpDecRefQueue() 
+    {
+        super();
+    }
+
+    public FuncInterpDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index 494c2695c..406c0b33a 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class FuncInterpEntryDecRefQueue extends IDecRefQueue
 {
+    public FuncInterpEntryDecRefQueue() 
+    {
+        super();
+    }
+
+    public FuncInterpEntryDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Global.java b/src/api/java/Global.java
index b31c4a7ae..44fb4cac7 100644
--- a/src/api/java/Global.java
+++ b/src/api/java/Global.java
@@ -44,7 +44,7 @@ public final class Global
      **/
     public static void setParameter(String id, String value)
     {
-	Native.globalParamSet(id, value);
+    Native.globalParamSet(id, value);
     }
     
     /**
@@ -67,10 +67,10 @@ public final class Global
      * 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()
     {
-	Native.globalParamResetAll();
+    Native.globalParamResetAll();
     }   
 }
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index 5a9221b63..b6897c517 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -27,7 +27,7 @@ public class Goal extends Z3Object
 {
     /**
      * The precision of the goal.
-	 * Remarks:  Goals can be transformed using over
+     * Remarks:  Goals can be transformed using over
      * and under approximations. An under approximation is applied when the
      * objective is to find a model for a given goal. An over approximation is
      * applied when the objective is to find a proof for a given goal.
@@ -97,7 +97,7 @@ public class Goal extends Z3Object
 
     /**
      * The depth of the goal.
-	 * Remarks:  This tracks how many transformations
+     * Remarks:  This tracks how many transformations
      * were applied to it. 
      **/
     public int getDepth() throws Z3Exception
@@ -176,7 +176,7 @@ public class Goal extends Z3Object
 
     /**
      * Simplifies the goal.
-	 * Remarks: Essentially invokes the `simplify' tactic
+     * Remarks: Essentially invokes the `simplify' tactic
      * on the goal.
      **/
     public Goal simplify() throws Z3Exception
@@ -192,7 +192,7 @@ public class Goal extends Z3Object
     
     /**
      * Simplifies the goal.
-	 * Remarks: Essentially invokes the `simplify' tactic
+     * Remarks: Essentially invokes the `simplify' tactic
      * on the goal.
      **/
     public Goal simplify(Params p) throws Z3Exception
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index 45992170f..dd9d69414 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class GoalDecRefQueue extends IDecRefQueue
 {
+    public GoalDecRefQueue() 
+    {
+        super();
+    }
+
+    public GoalDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index 2190f8e4d..e8cab3477 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -21,39 +21,49 @@ import java.util.LinkedList;
 
 abstract class IDecRefQueue
 {
-	protected Object m_lock = new Object();
-	protected LinkedList<Long> m_queue = new LinkedList<Long>();
-	protected final int m_move_limit = 1024;
+    protected Object m_lock = new Object();
+    protected LinkedList<Long> m_queue = new LinkedList<Long>();
+    protected int m_move_limit;
 
-	protected abstract void incRef(Context ctx, long obj);
+    public IDecRefQueue() 
+    {
+    m_move_limit = 1024;
+    }
 
-	protected abstract void decRef(Context ctx, long obj);
+    public IDecRefQueue(int move_limit) 
+    {
+    m_move_limit = move_limit;
+    }
 
-	protected void incAndClear(Context ctx, long o)
-	{
-		incRef(ctx, o);
-		if (m_queue.size() >= m_move_limit)
-			clear(ctx);
-	}
+    protected abstract void incRef(Context ctx, long obj);
 
-	protected void add(long o)
-	{
-		if (o == 0)
-			return;
+    protected abstract void decRef(Context ctx, long obj);
 
-		synchronized (m_lock)
-		{
-			m_queue.add(o);
-		}
-	}
+    protected void incAndClear(Context ctx, long o)
+    {
+        incRef(ctx, o);
+        if (m_queue.size() >= m_move_limit)
+            clear(ctx);
+    }
 
-	protected void clear(Context ctx)
-	{
-		synchronized (m_lock)
-		{
-			for (Long o : m_queue)
-				decRef(ctx, o);
-			m_queue.clear();
-		}
-	}
+    protected void add(long o)
+    {
+        if (o == 0)
+            return;
+
+        synchronized (m_lock)
+        {
+            m_queue.add(o);
+        }
+    }
+
+    protected void clear(Context ctx)
+    {
+        synchronized (m_lock)
+        {
+            for (Long o : m_queue)
+                decRef(ctx, o);
+            m_queue.clear();
+        }
+    }
 }
diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java
index 9092213e3..dddfa5824 100644
--- a/src/api/java/IDisposable.java
+++ b/src/api/java/IDisposable.java
@@ -21,7 +21,7 @@ package com.microsoft.z3;
 
 public class IDisposable
 {
-	public void dispose() throws Z3Exception
-	{
-	}
+    public void dispose() throws Z3Exception
+    {
+    }
 }
diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java
index 642a58a54..a424cd51e 100644
--- a/src/api/java/IntExpr.java
+++ b/src/api/java/IntExpr.java
@@ -22,12 +22,12 @@ package com.microsoft.z3;
  **/
 public class IntExpr extends ArithExpr
 {
-	/**
-	 * Constructor for IntExpr
-	 * @throws Z3Exception on error
-	 **/
-	IntExpr(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    /**
+     * Constructor for IntExpr
+     * @throws Z3Exception on error
+     **/
+    IntExpr(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 }
diff --git a/src/api/java/IntSort.java b/src/api/java/IntSort.java
index bcfc730c4..0b1047718 100644
--- a/src/api/java/IntSort.java
+++ b/src/api/java/IntSort.java
@@ -22,13 +22,13 @@ package com.microsoft.z3;
  **/
 public class IntSort extends ArithSort
 {
-	IntSort(Context ctx, long obj) throws Z3Exception
-	{
-		super(ctx, obj);
-	}
+    IntSort(Context ctx, long obj) throws Z3Exception
+    {
+        super(ctx, obj);
+    }
 
-	IntSort(Context ctx) throws Z3Exception
-	{
-		super(ctx, Native.mkIntSort(ctx.nCtx()));
-	}
+    IntSort(Context ctx) throws Z3Exception
+    {
+        super(ctx, Native.mkIntSort(ctx.nCtx()));
+    }
 }
diff --git a/src/api/java/IntSymbol.java b/src/api/java/IntSymbol.java
index a677c9102..01f75e0a4 100644
--- a/src/api/java/IntSymbol.java
+++ b/src/api/java/IntSymbol.java
@@ -26,7 +26,7 @@ public class IntSymbol extends Symbol
 {
     /**
      * The int value of the symbol.
-	 * Remarks: Throws an exception if the symbol
+     * Remarks: Throws an exception if the symbol
      * is not of int kind. 
      **/
     public int getInt() throws Z3Exception
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index c1590e07f..4c20ec6ae 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -43,8 +43,8 @@ public class InterpolationContext extends Context
      * Constructor.
      *
      * 
-	 * Remarks: 
-	 * @see Context#Context
+     * Remarks: 
+     * @see Context#Context
      **/
     public InterpolationContext(Map<String, String> settings) throws Z3Exception
     { 
diff --git a/src/api/java/Log.java b/src/api/java/Log.java
index 3e8f0050b..ac0ebfb7f 100644
--- a/src/api/java/Log.java
+++ b/src/api/java/Log.java
@@ -19,7 +19,7 @@ package com.microsoft.z3;
 
 /**
  * Interaction logging for Z3.
-	 * Remarks:  Note that this is a global, static log
+     * Remarks:  Note that this is a global, static log
  * and if multiple Context objects are created, it logs the interaction with all
  * of them. 
  **/
@@ -29,7 +29,7 @@ public final class Log
 
     /**
      * Open an interaction log file. 
-	 * @param filename the name of the file to open
+     * @param filename the name of the file to open
      * 
      * @return True if opening the log file succeeds, false otherwise.
      **/
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 70f0e91c5..9392aacb6 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -27,7 +27,7 @@ public class Model extends Z3Object
     /**
      * Retrieves the interpretation (the assignment) of {@code a} in
      * the model. 
-	 * @param a A Constant
+     * @param a A Constant
      * 
      * @return An expression if the constant has an interpretation in the model,
      *         null otherwise.
@@ -42,7 +42,7 @@ public class Model extends Z3Object
     /**
      * Retrieves the interpretation (the assignment) of {@code f} in
      * the model. 
-	 * @param f A function declaration of zero arity
+     * @param f A function declaration of zero arity
      * 
      * @return An expression if the function has an interpretation in the model,
      *         null otherwise.
@@ -68,7 +68,7 @@ public class Model extends Z3Object
 
     /**
      * Retrieves the interpretation (the assignment) of a non-constant {@code f} in the model. 
-	 * @param f A function declaration of non-zero arity
+     * @param f A function declaration of non-zero arity
      * 
      * @return A FunctionInterpretation if the function has an interpretation in
      *         the model, null otherwise.
@@ -201,7 +201,7 @@ public class Model extends Z3Object
      * Remarks:  This function may fail if {@code t} contains
      * quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a
      * {@code ModelEvaluationFailedException} is thrown.  
-	 * @param t An expression {@code completion} When this flag
+     * @param t An expression {@code completion} When this flag
      * is enabled, a model value will be assigned to any constant or function
      * that does not have an interpretation in the model.
      * 
@@ -243,8 +243,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
      **/
@@ -262,7 +262,7 @@ public class Model extends Z3Object
     /**
      * The finite set of distinct values that represent the interpretation for
      * sort {@code s}. 
-	 * @param s An uninterpreted sort
+     * @param s An uninterpreted sort
      * 
      * @return An array of expressions, where each is an element of the universe
      *         of {@code s}
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index 1200b29be..c954a1fa8 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ModelDecRefQueue extends IDecRefQueue
 {
+    public ModelDecRefQueue() 
+    {
+        super();
+    }
+
+    public ModelDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index a29565e8e..95a92475e 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ParamDescrsDecRefQueue extends IDecRefQueue
 {
+    public ParamDescrsDecRefQueue() 
+    {
+        super();
+    }
+
+    public ParamDescrsDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index 7d71feb8f..7b9f34c00 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ParamsDecRefQueue extends IDecRefQueue
 {
+    public ParamsDecRefQueue() 
+    {
+        super();
+    }
+
+    public ParamsDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index fda5d37b4..e271bd949 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class ProbeDecRefQueue extends IDecRefQueue
 {
+    public ProbeDecRefQueue() 
+    {
+        super();
+    }
+
+    public ProbeDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index 58245d723..3ea2b2eaf 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -171,13 +171,13 @@ public class Quantifier extends BoolExpr
         } else
         {
             setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), 
-		    (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), 
-		     AST.getNativeObject(skolemID), 
-		     AST.arrayLength(patterns), AST.arrayToNative(patterns), 
-		     AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), 
-		     AST.arrayLength(sorts), AST.arrayToNative(sorts), 
-		     Symbol.arrayToNative(names), 
-		     body.getNativeObject()));
+            (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), 
+             AST.getNativeObject(skolemID), 
+             AST.arrayLength(patterns), AST.arrayToNative(patterns), 
+             AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), 
+             AST.arrayLength(sorts), AST.arrayToNative(sorts), 
+             Symbol.arrayToNative(names), 
+             body.getNativeObject()));
         }
     }
 
diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java
index 2e92a9429..278aba65e 100644
--- a/src/api/java/RatNum.java
+++ b/src/api/java/RatNum.java
@@ -62,7 +62,7 @@ public class RatNum extends RealExpr
 
     /**
      * Returns a string representation in decimal notation.
-	 * Remarks: The result
+     * Remarks: The result
      * has at most {@code precision} decimal places.
      **/
     public String toDecimalString(int precision) throws Z3Exception
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index b9c9ebca6..3e66a29ac 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() throws Z3Exception
     {
@@ -68,7 +68,7 @@ public class Solver extends Z3Object
 
     /**
      * Creates a backtracking point. 
-	 * @see pop
+     * @see pop
      **/
     public void push() throws Z3Exception
     {
@@ -77,7 +77,7 @@ public class Solver extends Z3Object
 
     /**
      * Backtracks one backtracking point.
-	 * Remarks: .
+     * Remarks: .
      **/
     public void pop() throws Z3Exception
     {
@@ -86,10 +86,10 @@ public class Solver extends Z3Object
 
     /**
      * Backtracks {@code n} backtracking points.
-	 * Remarks: Note that
+     * 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) throws Z3Exception
     {
@@ -98,7 +98,7 @@ public class Solver extends Z3Object
 
     /**
      * Resets the Solver.
-	 * Remarks: This removes all assertions from the
+     * Remarks: This removes all assertions from the
      * solver.
      **/
     public void reset() throws Z3Exception
@@ -121,20 +121,20 @@ public class Solver extends Z3Object
         }
     }
 
-    // / 
-    // / Assert multiple constraints into the solver, and track them (in the
-    // unsat) core
-    // / using the Boolean constants in ps.
-    // /
-    // / Remarks: 
-    // / This API is an alternative to <see cref="Check"/> with assumptions for
-    // extracting unsat cores.
-    // / Both APIs can be used in the same solver. The unsat core will contain a
-    // combination
-    // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
-    // and the Boolean literals
-    // / provided using <see cref="Check"/> with assumptions.
-    // / 
+    /** 
+     *  Assert multiple constraints into the solver, and track them (in the
+     * unsat) core
+     * using the Boolean constants in ps.
+     *
+     * Remarks: 
+     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * extracting unsat cores.
+     * Both APIs can be used in the same solver. The unsat core will contain a
+     * combination
+     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * and the Boolean literals
+     * provided using <see cref="Check"/> with assumptions.
+     **/
     public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
     {
         getContext().checkContextMatch(constraints);
@@ -147,19 +147,19 @@ public class Solver extends Z3Object
                     constraints[i].getNativeObject(), ps[i].getNativeObject());
     }
 
-    // / 
-    // / Assert a constraint into the solver, and track it (in the unsat) core
-    // / using the Boolean constant p.
-    // /
-    // / Remarks: 
-    // / This API is an alternative to <see cref="Check"/> with assumptions for
-    // extracting unsat cores.
-    // / Both APIs can be used in the same solver. The unsat core will contain a
-    // combination
-    // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
-    // and the Boolean literals
-    // / provided using <see cref="Check"/> with assumptions.
-    // / 
+    /** 
+     * Assert a constraint into the solver, and track it (in the unsat) core
+     * using the Boolean constant p.
+     * 
+     * Remarks: 
+     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * extracting unsat cores.
+     * Both APIs can be used in the same solver. The unsat core will contain a
+     * combination
+     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * and the Boolean literals
+     * provided using <see cref="Check"/> with assumptions.
+     */ 
     public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception
     {
         getContext().checkContextMatch(constraint);
@@ -200,9 +200,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(Expr... assumptions) throws Z3Exception
     {
@@ -228,9 +228,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() throws Z3Exception
     {
@@ -239,7 +239,7 @@ public class Solver extends Z3Object
 
     /**
      * The model of the last {@code Check}.
-	 * Remarks:  The result is
+     * Remarks:  The result is
      * {@code null} if {@code Check} was not invoked before, if its
      * results was not {@code SATISFIABLE}, or if model production is not
      * enabled. 
@@ -257,7 +257,7 @@ public class Solver extends Z3Object
 
     /**
      * The proof of the last {@code Check}.
-	 * Remarks:  The result is
+     * Remarks:  The result is
      * {@code null} if {@code Check} was not invoked before, if its
      * results was not {@code UNSATISFIABLE}, or if proof production is
      * disabled. 
@@ -275,7 +275,7 @@ public class Solver extends Z3Object
 
     /**
      * The unsat core of the last {@code Check}.
-	 * Remarks:  The unsat core
+     * Remarks:  The unsat core
      * is a subset of {@code Assertions} The result is empty if
      * {@code Check} was not invoked before, if its results was not
      * {@code UNSATISFIABLE}, or if core production is disabled. 
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index 993c99621..cbe5bbc3b 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -19,6 +19,13 @@ package com.microsoft.z3;
 
 class SolverDecRefQueue extends IDecRefQueue
 {
+    public SolverDecRefQueue() { super(); }
+    
+    public SolverDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index 270abd43f..e1cbbea7c 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -29,20 +29,20 @@ public class Sort extends AST
 
     /**
      * Equality operator for objects of type Sort. 
-	 * @param o
+     * @param o
      * @return
      **/
     public boolean equals(Object o)
     {
         Sort casted = null;
 
-	try {
-	    casted = Sort.class.cast(o);
-	} catch (ClassCastException e) {
-	    return false;
-	}
+    try {
+        casted = Sort.class.cast(o);
+    } catch (ClassCastException e) {
+        return false;
+    }
 
-	return this.getNativeObject() == casted.getNativeObject();
+    return this.getNativeObject() == casted.getNativeObject();
     }
 
     /**
@@ -135,9 +135,9 @@ public class Sort extends AST
         case Z3_RELATION_SORT:
             return new RelationSort(ctx, obj);
         case Z3_FLOATING_POINT_SORT:
-        	return new FPSort(ctx, obj);
+            return new FPSort(ctx, obj);
         case Z3_ROUNDING_MODE_SORT:
-    		return new FPRMSort(ctx, obj);
+            return new FPRMSort(ctx, obj);
         default:
             throw new Z3Exception("Unknown sort kind");
         }
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 88a897d15..475352024 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -177,7 +177,7 @@ public class Statistics extends Z3Object
 
     /**
      * The value of a particular statistical counter.
-	 * Remarks: Returns null if
+     * Remarks: Returns null if
      * the key is unknown.
      * 
      * @throws Z3Exception
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index db3e32c86..89c66a746 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/src/api/java/StatisticsDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class StatisticsDecRefQueue extends IDecRefQueue
 {
+    public StatisticsDecRefQueue() 
+    {
+        super();
+    }
+
+    public StatisticsDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java
index 4692b0fb9..122c7765f 100644
--- a/src/api/java/StringSymbol.java
+++ b/src/api/java/StringSymbol.java
@@ -26,7 +26,7 @@ public class StringSymbol extends Symbol
 {
     /**
      * The string value of the symbol.
-	 * Remarks: Throws an exception if the
+     * Remarks: Throws an exception if the
      * symbol is not of string kind.
      **/
     public String getString() throws Z3Exception
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index 0286e786d..79f60e497 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -49,7 +49,7 @@ public class Tactic extends Z3Object
      * @throws Z3Exception 
      **/
     public ApplyResult apply(Goal g) throws Z3Exception
-    {	
+    {    
         return apply(g, null);
     }
 
@@ -74,7 +74,7 @@ public class Tactic extends Z3Object
 
     /**
      * Creates a solver that is implemented using the given tactic. 
-	 * @see Context#mkSolver(Tactic)
+     * @see Context#mkSolver(Tactic)
      * @throws Z3Exception 
      **/
     public Solver getSolver() throws Z3Exception
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 5557d03b8..026760e46 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/src/api/java/TacticDecRefQueue.java
@@ -19,6 +19,16 @@ package com.microsoft.z3;
 
 class TacticDecRefQueue extends IDecRefQueue
 {
+    public TacticDecRefQueue() 
+    {
+        super();
+    }
+
+    public TacticDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
     protected void incRef(Context ctx, long obj)
     {
         try
diff --git a/src/api/java/Version.java b/src/api/java/Version.java
index 6e2fe5084..939a3ca5c 100644
--- a/src/api/java/Version.java
+++ b/src/api/java/Version.java
@@ -19,7 +19,7 @@ package com.microsoft.z3;
 
 /**
  * Version information. 
-	 * Remarks: Note that this class is static.
+     * Remarks: Note that this class is static.
  **/
 public class Version
 {
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 03cfcd625..9b39a3e2f 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -115,7 +115,7 @@ public class Z3Object extends IDisposable
             return null;
         long[] an = new long[a.length];
         for (int i = 0; i < a.length; i++)
-	    an[i] = (a[i] == null) ? 0 : a[i].getNativeObject();
+        an[i] = (a[i] == null) ? 0 : a[i].getNativeObject();
         return an;
     }