diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 936184e3c2c..bd705456f37 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -599,7 +599,7 @@ void quantifierExample1(Context ctx)
         System.out.println("QuantifierExample");
         Log.append("QuantifierExample");
 
-        Sort[] types = new Sort[3];
+        IntSort[] types = new IntSort[3];
         IntExpr[] xs = new IntExpr[3];
         Symbol[] names = new Symbol[3];
         IntExpr[] vars = new IntExpr[3];
@@ -1398,7 +1398,7 @@ public void bitvectorExample1(Context ctx) throws TestFailedException
         System.out.println("BitvectorExample1");
         Log.append("BitvectorExample1");
 
-        Sort bv_type = ctx.mkBitVecSort(32);
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
         BitVecExpr x = (BitVecExpr) ctx.mkConst("x", bv_type);
         BitVecNum zero = (BitVecNum) ctx.mkNumeral("0", bv_type);
         BitVecNum ten = ctx.mkBV(10, 32);
@@ -1420,7 +1420,7 @@ public void bitvectorExample2(Context ctx) throws TestFailedException
         Log.append("BitvectorExample2");
 
         /* construct x ^ y - 103 == x * y */
-        Sort bv_type = ctx.mkBitVecSort(32);
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
         BitVecExpr x = ctx.mkBVConst("x", 32);
         BitVecExpr y = ctx.mkBVConst("y", 32);
         BitVecExpr x_xor_y = ctx.mkBVXOR(x, y);
diff --git a/examples/java/JavaGenericExample.java b/examples/java/JavaGenericExample.java
new file mode 100644
index 00000000000..8dd31fed028
--- /dev/null
+++ b/examples/java/JavaGenericExample.java
@@ -0,0 +1,2135 @@
+/*++
+ Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    Program.java
+
+Abstract:
+
+    Z3 Java API: Example program
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-27
+
+Notes:
+    
+--*/
+
+import com.microsoft.z3.*;
+
+import java.util.*;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+import java.util.stream.Stream;
+
+import static java.util.stream.Stream.concat;
+
+class JavaGenericExample
+{
+    @SuppressWarnings("serial")
+    static class TestFailedException extends Exception
+    {
+        public TestFailedException()
+        {
+            super("Check FAILED");
+        }
+    }
+
+    // / Create axiom: function f is injective in the i-th argument.
+
+    // / <remarks>
+    // / The following axiom is produced:
+    // / <code>
+    // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
+    // / </code>
+    // / Where, <code>finv</code>is a fresh function declaration.
+
+    public <R extends Sort> BoolExpr injAxiom(Context ctx, FuncDecl<R> f, int i)
+    {
+        Sort[] domain = f.getDomain();
+        int sz = f.getDomainSize();
+
+        if (i >= sz)
+        {
+            System.out.println("failed to create inj axiom");
+            return null;
+        }
+
+        /* declare the i-th inverse of f: finv */
+        Sort finv_domain = f.getRange();
+        Sort finv_range = domain[i];
+        FuncDecl<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);
+
+        /* allocate temporary arrays */
+        /* fill types, names and xs */
+        Sort[] types = domain.clone();
+        List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkBound(j, types[j])).collect(Collectors.toList());
+        Symbol[] names = IntStream.range(0, sz).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new);
+
+        Expr<Sort> x_i = xs.get(i);
+
+        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
+        Expr<R> fxs = f.apply(xs.toArray(new Expr[0]));
+
+        /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
+        Expr<Sort> finv_fxs = finv.apply(fxs);
+
+        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
+        BoolExpr eq = ctx.mkEq(finv_fxs, x_i);
+
+        /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
+        Pattern p = ctx.mkPattern(fxs);
+
+        /* create & assert quantifier */
+
+        return ctx.mkForall(types, /* types of quantified variables */
+                names, /* names of quantified variables */
+                eq, 1, new Pattern[] { p } /* patterns */, null, null, null);
+    }
+
+    // / Create axiom: function f is injective in the i-th argument.
+
+    // / <remarks>
+    // / The following axiom is produced:
+    // / <code>
+    // / forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i
+    // / </code>
+    // / Where, <code>finv</code>is a fresh function declaration.
+
+    public <R extends Sort> BoolExpr injAxiomAbs(Context ctx, FuncDecl<R> f, int i)
+    {
+        Sort[] domain = f.getDomain();
+        int sz = f.getDomainSize();
+
+        if (i >= sz)
+        {
+            System.out.println("failed to create inj axiom");
+            return null;
+        }
+
+        /* declare the i-th inverse of f: finv */
+        R finv_domain = f.getRange();
+        Sort finv_range = domain[i];
+        FuncDecl<Sort> finv = ctx.mkFuncDecl("f_fresh", finv_domain, finv_range);
+
+        /* allocate temporary arrays */
+        List<Expr<Sort>> xs = IntStream.range(0, sz).mapToObj(j -> ctx.mkConst(String.format("x_%d", j), domain[j])).collect(Collectors.toList());
+
+        /* fill types, names and xs */
+        Expr<Sort> x_i = xs.get(i);
+
+        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
+        Expr<R> fxs = f.apply(xs.toArray(new Expr[0]));
+
+        /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
+        Expr<Sort> finv_fxs = finv.apply(fxs);
+
+        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
+        BoolExpr eq = ctx.mkEq(finv_fxs, x_i);
+
+        /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
+        Pattern p = ctx.mkPattern(fxs);
+
+        /* create & assert quantifier */
+        return ctx.mkForall(xs.toArray(new Expr[0]), /* types of quantified variables */
+                eq, /* names of quantified variables */
+                1, new Pattern[] { p } /* patterns */, null, null, null);
+    }
+
+    // / Assert the axiom: function f is commutative.
+
+    // / <remarks>
+    // / This example uses the SMT-LIB parser to simplify the axiom
+    // construction.
+    // / </remarks>
+    private <R extends Sort> BoolExpr commAxiom(Context ctx, FuncDecl<R> f) throws Exception
+    {
+        R t = f.getRange();
+        Sort[] dom = f.getDomain();
+
+        if (dom.length != 2 || !t.equals(dom[0]) || !t.equals(dom[1]))
+        {
+            System.out.printf("%d %s %s %s%n", dom.length, dom[0], dom[1], t);
+            throw new Exception("function must be binary, and argument types must be equal to return type");
+        }
+
+        String bench = String.format("(assert (forall (x %s) (y %s) (= (%s x y) (%s y x))))", t.getName(), t.getName(), f.getName(), f.getName());
+        return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
+                new Sort[] { t }, new Symbol[] { f.getName() },
+                new FuncDecl[] { f })[0];
+    }
+
+    // / "Hello world" example: create a Z3 logical context, and delete it.
+
+    public void simpleExample()
+    {
+        System.out.println("SimpleExample");
+        Log.append("SimpleExample");
+
+        {
+            Context ctx = new Context();
+            /* do something with the context */
+
+            /* be kind to dispose manually and not wait for the GC. */
+            ctx.close();
+        }
+    }
+
+    @SuppressWarnings("unchecked")
+    Model check(Context ctx, Expr<BoolSort> f, Status sat) throws TestFailedException
+    {
+        Solver s = ctx.mkSolver();
+        s.add(f);
+        if (s.check() != sat)
+            throw new TestFailedException();
+        if (sat == Status.SATISFIABLE)
+            return s.getModel();
+        else
+            return null;
+    }
+
+    void solveTactical(Context ctx, Tactic t, Goal g, Status sat)
+            throws TestFailedException
+    {
+        Solver s = ctx.mkSolver(t);
+        System.out.printf("%nTactical solver: %s%n", s);
+
+        s.add(g.getFormulas());
+        System.out.printf("Solver: %s%n", s);
+
+        if (s.check() != sat)
+            throw new TestFailedException();
+    }
+
+    ApplyResult applyTactic(Context ctx, Tactic t, Goal g)
+    {
+        System.out.printf("%nGoal: %s%n", g);
+
+        ApplyResult res = t.apply(g);
+        System.out.printf("Application result: %s%n", res);
+
+        Status q = Status.UNKNOWN;
+        for (Goal sg : res.getSubgoals())
+            if (sg.isDecidedSat())
+                q = Status.SATISFIABLE;
+            else if (sg.isDecidedUnsat())
+                q = Status.UNSATISFIABLE;
+
+        switch (q)
+        {
+        case UNKNOWN:
+            System.out.println("Tactic result: Undecided");
+            break;
+        case SATISFIABLE:
+            System.out.println("Tactic result: SAT");
+            break;
+        case UNSATISFIABLE:
+            System.out.println("Tactic result: UNSAT");
+            break;
+        }
+
+        return res;
+    }
+
+    void prove(Context ctx, Expr<BoolSort> f, boolean useMBQI) throws TestFailedException
+    {
+        BoolExpr[] assumptions = new BoolExpr[0];
+        prove(ctx, f, useMBQI, assumptions);
+    }
+
+    @SafeVarargs
+    final void prove(Context ctx, Expr<BoolSort> f, boolean useMBQI,
+                     Expr<BoolSort>... assumptions) throws TestFailedException
+    {
+        System.out.printf("Proving: %s%n", f);
+        Solver s = ctx.mkSolver();
+        Params p = ctx.mkParams();
+        p.add("mbqi", useMBQI);
+        s.setParameters(p);
+        s.add(assumptions);
+        s.add(ctx.mkNot(f));
+        Status q = s.check();
+
+        switch (q)
+        {
+        case UNKNOWN:
+            System.out.printf("Unknown because: %s%n", s.getReasonUnknown());
+            break;
+        case SATISFIABLE:
+            throw new TestFailedException();
+        case UNSATISFIABLE:
+            System.out.printf("OK, proof: %s%n", s.getProof());
+            break;
+        }
+    }
+
+    void disprove(Context ctx, Expr<BoolSort> f, boolean useMBQI)
+        throws TestFailedException
+    {
+        BoolExpr[] a = {};
+        disprove(ctx, f, useMBQI, a);
+    }
+
+    @SafeVarargs
+    final void disprove(Context ctx, Expr<BoolSort> f, boolean useMBQI,
+                        Expr<BoolSort>... assumptions) throws TestFailedException
+    {
+        System.out.printf("Disproving: %s%n", f);
+        Solver s = ctx.mkSolver();
+        Params p = ctx.mkParams();
+        p.add("mbqi", useMBQI);
+        s.setParameters(p);
+        s.add(assumptions);
+        s.add(ctx.mkNot(f));
+        Status q = s.check();
+
+        switch (q)
+        {
+        case UNKNOWN:
+            System.out.printf("Unknown because: %s%n", s.getReasonUnknown());
+            break;
+        case SATISFIABLE:
+            System.out.printf("OK, model: %s%n", s.getModel());
+            break;
+        case UNSATISFIABLE:
+            throw new TestFailedException();
+        }
+    }
+
+    @SuppressWarnings("unchecked")
+    void modelConverterTest(Context ctx) throws TestFailedException
+    {
+        System.out.println("ModelConverterTest");
+
+        Expr<RealSort> xr = ctx.mkConst(ctx.mkSymbol("x"), ctx.mkRealSort());
+        Expr<RealSort> yr = ctx.mkConst(ctx.mkSymbol("y"), ctx.mkRealSort());
+        Goal g4 = ctx.mkGoal(true, false, false);
+        g4.add(ctx.mkGt(xr, ctx.mkReal(10, 1)));
+        g4.add(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1))));
+        g4.add(ctx.mkGt(yr, ctx.mkReal(1, 1)));
+
+        ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g4);
+        if (ar.getNumSubgoals() == 1
+                && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0]
+                        .isDecidedUnsat()))
+            throw new TestFailedException();
+
+        ar = applyTactic(ctx, ctx.andThen(ctx.mkTactic("simplify"),
+                ctx.mkTactic("solve-eqs")), g4);
+        if (ar.getNumSubgoals() == 1
+                && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0]
+                        .isDecidedUnsat()))
+            throw new TestFailedException();
+
+        Solver s = ctx.mkSolver();
+        for (BoolExpr e : ar.getSubgoals()[0].getFormulas())
+            s.add(e);
+        Status q = s.check();
+        System.out.printf("Solver says: %s%n", q);
+        System.out.printf("Model: %n%s%n", s.getModel());
+        if (q != Status.SATISFIABLE)
+            throw new TestFailedException();
+    }
+
+    // / A simple array example.
+
+    @SuppressWarnings("unchecked")
+    void arrayExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("ArrayExample1");
+        Log.append("ArrayExample1");
+
+        Goal g = ctx.mkGoal(true, false, false);
+        ArraySort<IntSort, BitVecSort> asort = ctx.mkArraySort(ctx.getIntSort(),
+                ctx.mkBitVecSort(32));
+        Expr<ArraySort<IntSort, BitVecSort>> aex = ctx.mkConst(ctx.mkSymbol("MyArray"), asort);
+        Expr<BitVecSort> sel = ctx.mkSelect(aex, ctx.mkInt(0));
+        g.add(ctx.mkEq(sel, ctx.mkBV(42, 32)));
+        Symbol xs = ctx.mkSymbol("x");
+        IntExpr xc = (IntExpr) ctx.mkConst(xs, ctx.getIntSort());
+
+        Symbol fname = ctx.mkSymbol("f");
+        Sort[] domain = { ctx.getIntSort() };
+        FuncDecl<IntSort> fd = ctx.mkFuncDecl(fname, domain, ctx.getIntSort());
+        Expr<?>[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) };
+        Expr<IntSort> fapp = ctx.mkApp(fd, fargs);
+
+        g.add(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123)));
+
+        Solver s = ctx.mkSolver();
+        for (BoolExpr a : g.getFormulas())
+            s.add(a);
+        System.out.printf("Solver: %s%n", s);
+
+        Status q = s.check();
+        System.out.printf("Status: %s%n", q);
+
+        if (q != Status.SATISFIABLE)
+            throw new TestFailedException();
+
+        System.out.printf("Model = %s%n", s.getModel());
+
+        System.out.printf("Interpretation of MyArray:%n%s%n", s.getModel().getFuncInterp(aex.getFuncDecl()));
+        System.out.printf("Interpretation of x:%n%s%n", s.getModel().getConstInterp(xc));
+        System.out.printf("Interpretation of f:%n%s%n", s.getModel().getFuncInterp(fd));
+        System.out.printf("Interpretation of MyArray as Term:%n%s%n", s.getModel().getFuncInterp(aex.getFuncDecl()));
+    }
+
+    // / Prove <tt>store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2
+    // = i3 or select(a1, i3) = select(a2, i3))</tt>.
+
+    // / <remarks>This example demonstrates how to use the array
+    // theory.</remarks>
+    public void arrayExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("ArrayExample2");
+        Log.append("ArrayExample2");
+
+        IntSort int_type = ctx.getIntSort();
+        ArraySort<IntSort, IntSort> array_type = ctx.mkArraySort(int_type, int_type);
+
+        Expr<ArraySort<IntSort, IntSort>> a1 = ctx.mkConst("a1", array_type);
+        ArrayExpr<IntSort, IntSort> a2 = ctx.mkArrayConst("a2", int_type, int_type);
+        Expr<IntSort> i1 = ctx.mkConst("i1", int_type);
+        Expr<IntSort> i2 = ctx.mkConst("i2", int_type);
+        Expr<IntSort> i3 = ctx.mkConst("i3", int_type);
+        Expr<IntSort> v1 = ctx.mkConst("v1", int_type);
+        Expr<IntSort> v2 = ctx.mkConst("v2", int_type);
+
+        ArrayExpr<IntSort, IntSort> st1 = ctx.mkStore(a1, i1, v1);
+        ArrayExpr<IntSort, IntSort> st2 = ctx.mkStore(a2, i2, v2);
+
+        Expr<IntSort> sel1 = ctx.mkSelect(a1, i3);
+        Expr<IntSort> sel2 = ctx.mkSelect(a2, i3);
+
+        /* create antecedent */
+        BoolExpr antecedent = ctx.mkEq(st1, st2);
+
+        /*
+         * create consequent: i1 = i3 or i2 = i3 or select(a1, i3) = select(a2,
+         * i3)
+         */
+        BoolExpr consequent = ctx.mkOr(ctx.mkEq(i1, i3), ctx.mkEq(i2, i3), ctx.mkEq(sel1, sel2));
+
+        /*
+         * prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 =
+         * i3 or select(a1, i3) = select(a2, i3))
+         */
+        BoolExpr thm = ctx.mkImplies(antecedent, consequent);
+        System.out.println("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))");
+        System.out.println(thm);
+        prove(ctx, thm, false);
+    }
+
+    // / Show that <code>distinct(a_0, ... , a_n)</code> is
+    // / unsatisfiable when <code>a_i</code>'s are arrays from boolean to
+    // / boolean and n > 4.
+
+    // / <remarks>This example also shows how to use the <code>distinct</code>
+    // construct.</remarks>
+    @SuppressWarnings("unchecked")
+    public void arrayExample3(Context ctx) throws TestFailedException
+    {
+        System.out.println("ArrayExample3");
+        Log.append("ArrayExample2");
+
+        for (int n = 2; n <= 5; n++)
+        {
+            System.out.printf("n = %d%n", n);
+
+            BoolSort bool_type = ctx.mkBoolSort();
+            ArraySort<BoolSort, BoolSort> array_type = ctx.mkArraySort(bool_type, bool_type);
+            List<Expr<ArraySort<BoolSort, BoolSort>>> a = IntStream.range(0, n).mapToObj(i -> ctx.mkConst(String.format("array_%d", i), array_type)).collect(Collectors.toList());
+
+            /* create arrays */
+
+            /* assert distinct(a[0], ..., a[n]) */
+            BoolExpr d = ctx.mkDistinct(a.toArray(new Expr[0]));
+            System.out.println(d);
+
+            /* context is satisfiable if n < 5 */
+            Model model = check(ctx, d, n < 5 ? Status.SATISFIABLE : Status.UNSATISFIABLE);
+            if (n < 5)
+            {
+                for (int i = 0; i < n; i++)
+                {
+                    System.out.printf("%s = %s%n", a.get(i), model.evaluate(a.get(i), false));
+                }
+            }
+        }
+    }
+
+    // / Sudoku solving example.
+
+    @SuppressWarnings({"unchecked", "CodeBlock2Expr"})
+    void sudokuExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("SudokuExample");
+        Log.append("SudokuExample");
+
+        // 9x9 matrix of integer variables
+        List<List<Expr<IntSort>>> X = IntStream.range(0, 9).mapToObj(i -> IntStream.range(0, 9).mapToObj(j ->
+                ctx.mkConst(ctx.mkSymbol(String.format("x_%d_%d", i + 1, j + 1)), ctx.getIntSort()))
+                .collect(Collectors.toList())).collect(Collectors.toList());
+
+        // each cell contains a value in {1, ..., 9}
+        List<List<BoolExpr>> cells_c = X.stream().map(r -> r.stream().map(c ->
+                ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), c), ctx.mkLe(c, ctx.mkInt(9))))
+                .collect(Collectors.toList())).collect(Collectors.toList());
+
+        // each row contains a digit at most once
+        List<BoolExpr> rows_c = new ArrayList<>();
+        for (int i1 = 0; i1 < 9; i1++) {
+            BoolExpr boolExpr = ctx.mkDistinct(X.get(i1).toArray(new Expr[0]));
+            rows_c.add(boolExpr);
+        }
+
+        // each column contains a digit at most once
+        List<BoolExpr> cols_c = new ArrayList<>();
+        for (int idx = 0; idx < 9; idx++) {
+            int j1 = idx;
+            BoolExpr boolExpr = ctx.mkDistinct(X.stream().map(r -> r.get(j1)).toArray(Expr[]::new));
+            cols_c.add(boolExpr);
+        }
+
+        // each 3x3 square contains a digit at most once
+        List<List<BoolExpr>> sq_c = new ArrayList<>();
+        for (int i0 = 0; i0 < 3; i0++) {
+            List<BoolExpr> collect = new ArrayList<>();
+            for (int j0 = 0; j0 < 3; j0++) {
+                List<Expr<IntSort>> list = new ArrayList<>();
+                for (int i = 0; i < 3; i++) {
+                    for (int j = 0; j < 3; j++) {
+                        Expr<IntSort> intSortExpr = X.get(3 * i0 + i).get(3 * j0 + j);
+                        list.add(intSortExpr);
+                    }
+                }
+                BoolExpr boolExpr = ctx.mkDistinct(list.toArray(new Expr[0]));
+                collect.add(boolExpr);
+            }
+            sq_c.add(collect);
+        }
+
+        Stream<BoolExpr> sudoku_s = cells_c.stream().flatMap(Collection::stream);
+        sudoku_s = concat(sudoku_s, rows_c.stream());
+        sudoku_s = concat(sudoku_s, cols_c.stream());
+        sudoku_s = concat(sudoku_s, sq_c.stream().flatMap(Collection::stream));
+        BoolExpr sudoku_c = ctx.mkAnd(sudoku_s.toArray(BoolExpr[]::new));
+
+        // sudoku instance, we use '0' for empty cells
+        int[][] instance = {
+                { 0, 0, 0, 0, 9, 4, 0, 3, 0 },
+                { 0, 0, 0, 5, 1, 0, 0, 0, 7 },
+                { 0, 8, 9, 0, 0, 0, 0, 4, 0 },
+                { 0, 0, 0, 0, 0, 0, 2, 0, 8 },
+                { 0, 6, 0, 2, 0, 1, 0, 5, 0 },
+                { 1, 0, 2, 0, 0, 0, 0, 0, 0 },
+                { 0, 7, 0, 0, 0, 0, 5, 2, 0 },
+                { 9, 0, 0, 0, 6, 5, 0, 0, 0 },
+                { 0, 4, 0, 9, 7, 0, 0, 0, 0 }
+        };
+
+        // assert the variables we know
+        BoolExpr instance_c = ctx.mkAnd(IntStream.range(0, 9).boxed().flatMap(i -> IntStream.range(0, 9).filter(j -> instance[i][j] != 0).mapToObj(j -> ctx.mkEq(X.get(i).get(j), ctx.mkInt(instance[i][j])))).toArray(Expr[]::new));
+
+        Solver s = ctx.mkSolver();
+        s.add(sudoku_c);
+        s.add(instance_c);
+
+        if (s.check() == Status.SATISFIABLE)
+        {
+            Model m = s.getModel();
+            List<List<Expr<IntSort>>> R = X.stream().map(r -> r.stream().map(c -> m.eval(c, false)).collect(Collectors.toList())).collect(Collectors.toList());
+            System.out.println("Sudoku solution:");
+            R.forEach(r -> System.out.println(r.stream().map(Objects::toString).collect(Collectors.joining(" "))));
+        } else
+        {
+            System.out.println("Failed to solve sudoku");
+            throw new TestFailedException();
+        }
+    }
+
+    // / A basic example of how to use quantifiers.
+
+    @SuppressWarnings("unchecked")
+    void quantifierExample1(Context ctx)
+    {
+        System.out.println("QuantifierExample");
+        Log.append("QuantifierExample");
+
+        IntSort[] types = new IntSort[3];
+        Arrays.fill(types, ctx.getIntSort());
+        Symbol[] names = IntStream.range(0, 3).mapToObj(j -> ctx.mkSymbol(String.format("x_%d", j))).toArray(Symbol[]::new);
+        List<Expr<IntSort>> xs = IntStream.range(0, 3).mapToObj(j -> ctx.mkConst(names[j], types[j])).collect(Collectors.toList());
+        List<Expr<IntSort>> vars = IntStream.range(0, 3).mapToObj(j -> ctx.mkBound(2 - j, types[j])).collect(Collectors.toList());
+
+        BoolExpr body_vars = ctx.mkAnd(
+                ctx.mkEq(ctx.mkAdd(vars.get(0), ctx.mkInt(1)), ctx.mkInt(2)),
+                ctx.mkEq(ctx.mkAdd(vars.get(1), ctx.mkInt(2)),
+                        ctx.mkAdd(vars.get(2), ctx.mkInt(3))));
+
+        BoolExpr body_const = ctx.mkAnd(
+                ctx.mkEq(ctx.mkAdd(xs.get(0), ctx.mkInt(1)), ctx.mkInt(2)),
+                ctx.mkEq(ctx.mkAdd(xs.get(1), ctx.mkInt(2)),
+                        ctx.mkAdd(xs.get(2), ctx.mkInt(3))));
+
+        Quantifier x = ctx.mkForall(types, names, body_vars, 1, null, null,
+                ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
+        System.out.printf("Quantifier X: %s%n", x.toString());
+
+        Quantifier y = ctx.mkForall(xs.toArray(new Expr[0]), body_const, 1, null, null,
+                ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));
+        System.out.printf("Quantifier Y: %s%n", y.toString());
+    }
+
+    void quantifierExample2(Context ctx)
+    {
+
+        System.out.println("QuantifierExample2");
+        Log.append("QuantifierExample2");
+
+        Quantifier q1, q2;
+        FuncDecl<IntSort> f = ctx.mkFuncDecl("f", ctx.getIntSort(), ctx.getIntSort());
+        FuncDecl<IntSort> g = ctx.mkFuncDecl("g", ctx.getIntSort(), ctx.getIntSort());
+
+        // Quantifier with Exprs as the bound variables.
+        {
+            Expr<IntSort> x = ctx.mkConst("x", ctx.getIntSort());
+            Expr<IntSort> y = ctx.mkConst("y", ctx.getIntSort());
+            Expr<IntSort> f_x = ctx.mkApp(f, x);
+            Expr<IntSort> f_y = ctx.mkApp(f, y);
+            Expr<IntSort> g_y = ctx.mkApp(g, y);
+            @SuppressWarnings("unused")
+            Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) };
+            Expr[] no_pats = new Expr[] { f_y };
+            Expr[] bound = new Expr[] { x, y };
+            BoolExpr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y));
+
+            q1 = ctx.mkForall(bound, body, 1, null, no_pats, ctx.mkSymbol("q"),
+                    ctx.mkSymbol("sk"));
+
+            System.out.println(q1);
+        }
+
+        // Quantifier with de-Bruijn indices.
+        {
+            Expr<IntSort> x = ctx.mkBound(1, ctx.getIntSort());
+            Expr<IntSort> y = ctx.mkBound(0, ctx.getIntSort());
+            Expr<IntSort> f_x = ctx.mkApp(f, x);
+            Expr<IntSort> f_y = ctx.mkApp(f, y);
+            Expr<IntSort> g_y = ctx.mkApp(g, y);
+            @SuppressWarnings("unused")
+            Pattern[] pats = new Pattern[] { ctx.mkPattern(f_x, g_y) };
+            Expr[] no_pats = new Expr[] { f_y };
+            Symbol[] names = new Symbol[] { ctx.mkSymbol("x"),
+                    ctx.mkSymbol("y") };
+            Sort[] sorts = new Sort[] { ctx.getIntSort(), ctx.getIntSort() };
+            BoolExpr body = ctx.mkAnd(ctx.mkEq(f_x, f_y), ctx.mkEq(f_y, g_y));
+
+            q2 = ctx.mkForall(sorts, names, body, 1, null, // pats,
+                    no_pats, ctx.mkSymbol("q"), ctx.mkSymbol("sk"));
+            System.out.println(q2);
+        }
+
+        System.out.println(q1.equals(q2));
+    }
+
+    // / Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
+    // / <code>f</code> is injective in the second argument. <seealso
+    // cref="inj_axiom"/>
+
+    public void quantifierExample3(Context ctx) throws TestFailedException
+    {
+        System.out.println("QuantifierExample3");
+        Log.append("QuantifierExample3");
+
+        /*
+         * If quantified formulas are asserted in a logical context, then the
+         * model produced by Z3 should be viewed as a potential model.
+         */
+
+        /* declare function f */
+        IntSort I = ctx.getIntSort();
+        FuncDecl<IntSort> f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I);
+
+        /* f is injective in the second argument. */
+        BoolExpr inj = injAxiom(ctx, f, 1);
+
+        /* create x, y, v, w, fxy, fwv */
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntExpr v = ctx.mkIntConst("v");
+        IntExpr w = ctx.mkIntConst("w");
+        Expr<IntSort> fxy = ctx.mkApp(f, x, y);
+        Expr<IntSort> fwv = ctx.mkApp(f, w, v);
+
+        /* f(x, y) = f(w, v) */
+        BoolExpr p1 = ctx.mkEq(fxy, fwv);
+
+        /* prove f(x, y) = f(w, v) implies y = v */
+        BoolExpr p2 = ctx.mkEq(y, v);
+        prove(ctx, p2, false, inj, p1);
+
+        /* disprove f(x, y) = f(w, v) implies x = w */
+        BoolExpr p3 = ctx.mkEq(x, w);
+        disprove(ctx, p3, false, inj, p1);
+    }
+
+    // / Prove that <tt>f(x, y) = f(w, v) implies y = v</tt> when
+    // / <code>f</code> is injective in the second argument. <seealso
+    // cref="inj_axiom"/>
+
+    public void quantifierExample4(Context ctx) throws TestFailedException
+    {
+        System.out.println("QuantifierExample4");
+        Log.append("QuantifierExample4");
+
+        /*
+         * If quantified formulas are asserted in a logical context, then the
+         * model produced by Z3 should be viewed as a potential model.
+         */
+
+        /* declare function f */
+        IntSort I = ctx.getIntSort();
+        FuncDecl<IntSort> f = ctx.mkFuncDecl("f", new Sort[] { I, I }, I);
+
+        /* f is injective in the second argument. */
+        BoolExpr inj = injAxiomAbs(ctx, f, 1);
+
+        /* create x, y, v, w, fxy, fwv */
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntExpr v = ctx.mkIntConst("v");
+        IntExpr w = ctx.mkIntConst("w");
+        Expr<IntSort> fxy = ctx.mkApp(f, x, y);
+        Expr<IntSort> fwv = ctx.mkApp(f, w, v);
+
+        /* f(x, y) = f(w, v) */
+        BoolExpr p1 = ctx.mkEq(fxy, fwv);
+
+        /* prove f(x, y) = f(w, v) implies y = v */
+        BoolExpr p2 = ctx.mkEq(y, v);
+        prove(ctx, p2, false, inj, p1);
+
+        /* disprove f(x, y) = f(w, v) implies x = w */
+        BoolExpr p3 = ctx.mkEq(x, w);
+        disprove(ctx, p3, false, inj, p1);
+    }
+
+    // / Some basic tests.
+
+    void basicTests(Context ctx) throws TestFailedException
+    {
+        System.out.println("BasicTests");
+
+        Symbol fname = ctx.mkSymbol("f");
+        Symbol x = ctx.mkSymbol("x");
+        Symbol y = ctx.mkSymbol("y");
+
+        BoolSort bs = ctx.mkBoolSort();
+
+        Sort[] domain = { bs, bs };
+        FuncDecl<BoolSort> f = ctx.mkFuncDecl(fname, domain, bs);
+        Expr<BoolSort> fapp = ctx.mkApp(f, ctx.mkConst(x, bs), ctx.mkConst(y, bs));
+
+        Expr<?>[] fargs2 = { ctx.mkFreshConst("cp", bs) };
+        Sort[] domain2 = { bs };
+        Expr<BoolSort> fapp2 = ctx.mkApp(ctx.mkFreshFuncDecl("fp", domain2, bs), fargs2);
+
+        BoolExpr trivial_eq = ctx.mkEq(fapp, fapp);
+        BoolExpr nontrivial_eq = ctx.mkEq(fapp, fapp2);
+
+        Goal g = ctx.mkGoal(true, false, false);
+        g.add(trivial_eq);
+        g.add(nontrivial_eq);
+        System.out.printf("Goal: %s%n", g);
+
+        Solver solver = ctx.mkSolver();
+
+        solver.add(g.getFormulas());
+
+        if (solver.check() != Status.SATISFIABLE)
+            throw new TestFailedException();
+
+        ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g);
+        if (ar.getNumSubgoals() == 1
+                && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0]
+                        .isDecidedUnsat()))
+            throw new TestFailedException();
+
+        ar = applyTactic(ctx, ctx.mkTactic("smt"), g);
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat())
+            throw new TestFailedException();
+
+        g.add(ctx.mkEq(ctx.mkNumeral(1, ctx.mkBitVecSort(32)),
+                ctx.mkNumeral(2, ctx.mkBitVecSort(32))));
+        ar = applyTactic(ctx, ctx.mkTactic("smt"), g);
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat())
+            throw new TestFailedException();
+
+        Goal g2 = ctx.mkGoal(true, true, false);
+        ar = applyTactic(ctx, ctx.mkTactic("smt"), g2);
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat())
+            throw new TestFailedException();
+
+        g2 = ctx.mkGoal(true, true, false);
+        g2.add(ctx.mkFalse());
+        ar = applyTactic(ctx, ctx.mkTactic("smt"), g2);
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat())
+            throw new TestFailedException();
+
+        Goal g3 = ctx.mkGoal(true, true, false);
+        Expr<IntSort> xc = ctx.mkConst(ctx.mkSymbol("x"), ctx.getIntSort());
+        Expr<IntSort> yc = ctx.mkConst(ctx.mkSymbol("y"), ctx.getIntSort());
+        g3.add(ctx.mkEq(xc, ctx.mkNumeral(1, ctx.getIntSort())));
+        g3.add(ctx.mkEq(yc, ctx.mkNumeral(2, ctx.getIntSort())));
+        BoolExpr constr = ctx.mkEq(xc, yc);
+        g3.add(constr);
+        ar = applyTactic(ctx, ctx.mkTactic("smt"), g3);
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedUnsat())
+            throw new TestFailedException();
+
+        modelConverterTest(ctx);
+
+        // Real num/den test.
+        RatNum rn = ctx.mkReal(42, 43);
+        IntNum inum = rn.getNumerator();
+        IntNum iden = rn.getDenominator();
+        System.out.printf("Numerator: %s Denominator: %s%n", inum, iden);
+        if (!inum.toString().equals("42") || !iden.toString().equals("43"))
+            throw new TestFailedException();
+
+        if (!rn.toDecimalString(3).equals("0.976?"))
+            throw new TestFailedException();
+
+        bigIntCheck(ctx, ctx.mkReal("-1231231232/234234333"));
+        bigIntCheck(ctx, ctx.mkReal("-123123234234234234231232/234234333"));
+        bigIntCheck(ctx, ctx.mkReal("-234234333"));
+        bigIntCheck(ctx, ctx.mkReal("234234333/2"));
+
+        String bn = "1234567890987654321";
+
+        if (!ctx.mkInt(bn).getBigInteger().toString().equals(bn))
+            throw new TestFailedException();
+
+        if (!ctx.mkBV(bn, 128).getBigInteger().toString().equals(bn))
+            throw new TestFailedException();
+
+        if (ctx.mkBV(bn, 32).getBigInteger().toString().equals(bn))
+            throw new TestFailedException();
+
+        // Error handling test.
+        try
+        {
+            @SuppressWarnings("unused")
+            IntExpr i = ctx.mkInt("1/2");
+            throw new TestFailedException(); // unreachable
+        } catch (Z3Exception ignored)
+        {
+        }
+    }
+
+    // / Shows how to use Solver(logic)
+
+    // / @param ctx 
+    void logicExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("LogicTest");
+        Log.append("LogicTest");
+
+        Global.ToggleWarningMessages(true);
+
+        BitVecSort bvs = ctx.mkBitVecSort(32);
+        Expr<BitVecSort> x = ctx.mkConst("x", bvs);
+        Expr<BitVecSort> y = ctx.mkConst("y", bvs);
+        BoolExpr eq = ctx.mkEq(x, y);
+
+        // Use a solver for QF_BV
+        Solver s = ctx.mkSolver("QF_BV");
+        s.add(eq);
+        Status res = s.check();
+        System.out.printf("solver result: %s%n", res);
+
+        // Or perhaps a tactic for QF_BV
+        Goal g = ctx.mkGoal(true, false, false);
+        g.add(eq);
+
+        Tactic t = ctx.mkTactic("qfbv");
+        ApplyResult ar = t.apply(g);
+        System.out.printf("tactic result: %s%n", ar);
+
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat())
+            throw new TestFailedException();
+    }
+
+    // / Demonstrates how to use the ParOr tactic.
+
+    void parOrExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("ParOrExample");
+        Log.append("ParOrExample");
+
+        BitVecSort bvs = ctx.mkBitVecSort(32);
+        Expr<BitVecSort> x = ctx.mkConst("x", bvs);
+        Expr<BitVecSort> y = ctx.mkConst("y", bvs);
+        BoolExpr q = ctx.mkEq(x, y);
+
+        Goal g = ctx.mkGoal(true, false, false);
+        g.add(q);
+
+        Tactic t1 = ctx.mkTactic("qfbv");
+        Tactic t2 = ctx.mkTactic("qfbv");
+        Tactic p = ctx.parOr(t1, t2);
+
+        ApplyResult ar = p.apply(g);
+
+        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat())
+            throw new TestFailedException();
+    }
+
+    void bigIntCheck(Context ctx, RatNum r)
+    {
+        System.out.printf("Num: %s%n", r.getBigIntNumerator());
+        System.out.printf("Den: %s%n", r.getBigIntDenominator());
+    }
+
+    // / Find a model for <code>x xor y</code>.
+
+    public void findModelExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("FindModelExample1");
+        Log.append("FindModelExample1");
+
+        BoolExpr x = ctx.mkBoolConst("x");
+        BoolExpr y = ctx.mkBoolConst("y");
+        BoolExpr x_xor_y = ctx.mkXor(x, y);
+
+        Model model = check(ctx, x_xor_y, Status.SATISFIABLE);
+        System.out.printf("x = %s, y = %s%n", model.evaluate(x, false), model.evaluate(y, false));
+    }
+
+    // / Find a model for <tt>x < y + 1, x > 2</tt>.
+    // / Then, assert <tt>not(x = y)</tt>, and find another model.
+
+    public void findModelExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("FindModelExample2");
+        Log.append("FindModelExample2");
+
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntNum one = ctx.mkInt(1);
+        IntNum two = ctx.mkInt(2);
+
+        ArithExpr<IntSort> y_plus_one = ctx.mkAdd(y, one);
+
+        BoolExpr c1 = ctx.mkLt(x, y_plus_one);
+        BoolExpr c2 = ctx.mkGt(x, two);
+
+        BoolExpr q = ctx.mkAnd(c1, c2);
+
+        System.out.println("model for: x < y + 1, x > 2");
+        Model model = check(ctx, q, Status.SATISFIABLE);
+        System.out.printf("x = %s, y =%s%n", model.evaluate(x, false), model.evaluate(y, false));
+
+        /* assert not(x = y) */
+        BoolExpr x_eq_y = ctx.mkEq(x, y);
+        BoolExpr c3 = ctx.mkNot(x_eq_y);
+
+        q = ctx.mkAnd(q, c3);
+
+        System.out.println("model for: x < y + 1, x > 2, not(x = y)");
+        model = check(ctx, q, Status.SATISFIABLE);
+        System.out.printf("x = %s, y = %s%n", model.evaluate(x, false), model.evaluate(y, false));
+    }
+
+    // / Prove <tt>x = y implies g(x) = g(y)</tt>, and
+    // / disprove <tt>x = y implies g(g(x)) = g(y)</tt>.
+
+    // / <remarks>This function demonstrates how to create uninterpreted
+    // / types and functions.</remarks>
+    public void proveExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("ProveExample1");
+        Log.append("ProveExample1");
+
+        /* create uninterpreted type. */
+        UninterpretedSort U = ctx.mkUninterpretedSort(ctx.mkSymbol("U"));
+
+        /* declare function g */
+        FuncDecl<UninterpretedSort> g = ctx.mkFuncDecl("g", U, U);
+
+        /* create x and y */
+        Expr<UninterpretedSort> x = ctx.mkConst("x", U);
+        Expr<UninterpretedSort> y = ctx.mkConst("y", U);
+        /* create g(x), g(y) */
+        Expr<UninterpretedSort> gx = g.apply(x);
+        Expr<UninterpretedSort> gy = g.apply(y);
+
+        /* assert x = y */
+        BoolExpr eq = ctx.mkEq(x, y);
+
+        /* prove g(x) = g(y) */
+        BoolExpr f = ctx.mkEq(gx, gy);
+        System.out.println("prove: x = y implies g(x) = g(y)");
+        prove(ctx, ctx.mkImplies(eq, f), false);
+
+        /* create g(g(x)) */
+        Expr<UninterpretedSort> ggx = g.apply(gx);
+
+        /* disprove g(g(x)) = g(y) */
+        f = ctx.mkEq(ggx, gy);
+        System.out.println("disprove: x = y implies g(g(x)) = g(y)");
+        disprove(ctx, ctx.mkImplies(eq, f), false);
+
+        /* Print the model using the custom model printer */
+        Model m = check(ctx, ctx.mkNot(f), Status.SATISFIABLE);
+        System.out.println(m);
+    }
+
+    // / Prove <tt>not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0
+    // </tt>.
+    // / Then, show that <tt>z < -1</tt> is not implied.
+
+    // / <remarks>This example demonstrates how to combine uninterpreted
+    // functions
+    // / and arithmetic.</remarks>
+    public void proveExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("ProveExample2");
+        Log.append("ProveExample2");
+
+        /* declare function g */
+        IntSort I = ctx.getIntSort();
+
+        FuncDecl<IntSort> g = ctx.mkFuncDecl("g", I, I);
+
+        /* create x, y, and z */
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntExpr z = ctx.mkIntConst("z");
+
+        /* create gx, gy, gz */
+        Expr<IntSort> gx = ctx.mkApp(g, x);
+        Expr<IntSort> gy = ctx.mkApp(g, y);
+        Expr<IntSort> gz = ctx.mkApp(g, z);
+
+        /* create zero */
+        IntNum zero = ctx.mkInt(0);
+
+        /* assert not(g(g(x) - g(y)) = g(z)) */
+        ArithExpr<IntSort> gx_gy = ctx.mkSub(gx, gy);
+        Expr<IntSort> ggx_gy = ctx.mkApp(g, gx_gy);
+        BoolExpr eq = ctx.mkEq(ggx_gy, gz);
+        BoolExpr c1 = ctx.mkNot(eq);
+
+        /* assert x + z <= y */
+        ArithExpr<IntSort> x_plus_z = ctx.mkAdd(x, z);
+        BoolExpr c2 = ctx.mkLe(x_plus_z, y);
+
+        /* assert y <= x */
+        BoolExpr c3 = ctx.mkLe(y, x);
+
+        /* prove z < 0 */
+        BoolExpr f = ctx.mkLt(z, zero);
+        System.out.println("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0");
+        prove(ctx, f, false, c1, c2, c3);
+
+        /* disprove z < -1 */
+        IntNum minus_one = ctx.mkInt(-1);
+        f = ctx.mkLt(z, minus_one);
+        System.out.println("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1");
+        disprove(ctx, f, false, c1, c2, c3);
+    }
+
+    // / Show how push & pop can be used to create "backtracking" points.
+
+    // / <remarks>This example also demonstrates how big numbers can be
+    // / created in ctx.</remarks>
+    public void pushPopExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("PushPopExample1");
+        Log.append("PushPopExample1");
+
+        /* create a big number */
+        IntSort int_type = ctx.getIntSort();
+        IntNum big_number = ctx.mkInt("1000000000000000000000000000000000000000000000000000000");
+
+        /* create number 3 */
+        IntExpr three = (IntExpr) ctx.mkNumeral("3", int_type);
+
+        /* create x */
+        IntExpr x = ctx.mkIntConst("x");
+
+        Solver solver = ctx.mkSolver();
+
+        /* assert x >= "big number" */
+        BoolExpr c1 = ctx.mkGe(x, big_number);
+        System.out.println("assert: x >= 'big number'");
+        solver.add(c1);
+
+        /* create a backtracking point */
+        System.out.println("push");
+        solver.push();
+
+        /* assert x <= 3 */
+        BoolExpr c2 = ctx.mkLe(x, three);
+        System.out.println("assert: x <= 3");
+        solver.add(c2);
+
+        /* context is inconsistent at this point */
+        if (solver.check() != Status.UNSATISFIABLE)
+            throw new TestFailedException();
+
+        /*
+         * backtrack: the constraint x <= 3 will be removed, since it was
+         * asserted after the last ctx.Push.
+         */
+        System.out.println("pop");
+        solver.pop(1);
+
+        /* the context is consistent again. */
+        if (solver.check() != Status.SATISFIABLE)
+            throw new TestFailedException();
+
+        /* new constraints can be asserted... */
+
+        /* create y */
+        IntExpr y = ctx.mkIntConst("y");
+
+        /* assert y > x */
+        BoolExpr c3 = ctx.mkGt(y, x);
+        System.out.println("assert: y > x");
+        solver.add(c3);
+
+        /* the context is still consistent. */
+        if (solver.check() != Status.SATISFIABLE)
+            throw new TestFailedException();
+    }
+
+    // / Tuples.
+
+    // / <remarks>Check that the projection of a tuple
+    // / returns the corresponding element.</remarks>
+    public void tupleExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("TupleExample");
+        Log.append("TupleExample");
+
+        IntSort int_type = ctx.getIntSort();
+        TupleSort tuple = ctx.mkTupleSort(ctx.mkSymbol("mk_tuple"), // name of
+                                                                    // tuple
+                                                                    // constructor
+                new Symbol[] { ctx.mkSymbol("first"), ctx.mkSymbol("second") }, // names
+                                                                                // of
+                                                                                // projection
+                                                                                // operators
+                new Sort[] { int_type, int_type } // types of projection
+                                                  // operators
+                );
+        // have to cast here because it is not possible to type a member of an array of mixed generics
+        @SuppressWarnings("unchecked")
+        FuncDecl<IntSort> first = (FuncDecl<IntSort>) tuple.getFieldDecls()[0]; // declarations are for
+                                                   // projections
+        @SuppressWarnings("unused")
+        FuncDecl<?> second = tuple.getFieldDecls()[1];
+        Expr<IntSort> x = ctx.mkConst("x", int_type);
+        Expr<IntSort> y = ctx.mkConst("y", int_type);
+        Expr<TupleSort> n1 = tuple.mkDecl().apply(x, y);
+        Expr<IntSort> n2 = first.apply(n1);
+        BoolExpr n3 = ctx.mkEq(x, n2);
+        System.out.printf("Tuple example: %s%n", n3);
+        prove(ctx, n3, false);
+    }
+
+    // / Simple bit-vector example.
+
+    // / <remarks>
+    // / This example disproves that x - 10 &lt;= 0 IFF x &lt;= 10 for (32-bit)
+    // machine integers
+    // / </remarks>
+    public void bitvectorExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("BitvectorExample1");
+        Log.append("BitvectorExample1");
+
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
+        Expr<BitVecSort> x = ctx.mkConst("x", bv_type);
+        Expr<BitVecSort> zero = ctx.mkNumeral("0", bv_type);
+        BitVecNum ten = ctx.mkBV(10, 32);
+        BitVecExpr x_minus_ten = ctx.mkBVSub(x, ten);
+        /* bvsle is signed less than or equal to */
+        BoolExpr c1 = ctx.mkBVSLE(x, ten);
+        BoolExpr c2 = ctx.mkBVSLE(x_minus_ten, zero);
+        BoolExpr thm = ctx.mkIff(c1, c2);
+        System.out.println("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers");
+        disprove(ctx, thm, false);
+    }
+
+    // / Find x and y such that: x ^ y - 103 == x * y
+
+    public void bitvectorExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("BitvectorExample2");
+        Log.append("BitvectorExample2");
+
+        /* construct x ^ y - 103 == x * y */
+        BitVecSort bv_type = ctx.mkBitVecSort(32);
+        BitVecExpr x = ctx.mkBVConst("x", 32);
+        BitVecExpr y = ctx.mkBVConst("y", 32);
+        BitVecExpr x_xor_y = ctx.mkBVXOR(x, y);
+        Expr<BitVecSort> c103 = ctx.mkNumeral("103", bv_type);
+        BitVecExpr lhs = ctx.mkBVSub(x_xor_y, c103);
+        BitVecExpr rhs = ctx.mkBVMul(x, y);
+        BoolExpr ctr = ctx.mkEq(lhs, rhs);
+
+        System.out.println("find values of x and y, such that x ^ y - 103 == x * y");
+
+        /* find a model (i.e., values for x an y that satisfy the constraint */
+        Model m = check(ctx, ctr, Status.SATISFIABLE);
+        System.out.println(m);
+    }
+
+    // / Demonstrates how to use the SMTLIB parser.
+
+    public void parserExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("ParserExample1");
+        Log.append("ParserExample1");
+
+        BoolExpr f = ctx.parseSMTLIB2String(
+                "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
+                null, null, null, null)[0];
+        System.out.printf("formula %s%n", f);
+
+        @SuppressWarnings("unused")
+        Model m = check(ctx, f, Status.SATISFIABLE);
+    }
+
+    // / Demonstrates how to initialize the parser symbol table.
+
+    public void parserExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("ParserExample2");
+        Log.append("ParserExample2");
+
+        Symbol[] declNames = { ctx.mkSymbol("a"), ctx.mkSymbol("b") };
+        FuncDecl<IntSort> a = ctx.mkConstDecl(declNames[0], ctx.mkIntSort());
+        FuncDecl<IntSort> b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort());
+        FuncDecl[] decls = new FuncDecl[] { a, b };
+
+        BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null, declNames, decls)[0];
+        System.out.printf("formula: %s%n", f);
+        check(ctx, f, Status.SATISFIABLE);
+    }
+
+    // / Demonstrates how to initialize the parser symbol table.
+
+    public void parserExample3(Context ctx) throws Exception
+    {
+        System.out.println("ParserExample3");
+        Log.append("ParserExample3");
+
+        /* declare function g */
+        IntSort I = ctx.mkIntSort();
+        FuncDecl<IntSort> g = ctx.mkFuncDecl("g", new Sort[] { I, I }, I);
+
+        BoolExpr ca = commAxiom(ctx, g);
+
+        BoolExpr thm = ctx.parseSMTLIB2String(
+                "(declare-fun (Int Int) Int) (assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
+                null, null, new Symbol[] { ctx.mkSymbol("gg") },
+                new FuncDecl[] { g })[0];
+        System.out.printf("formula: %s%n", thm);
+        prove(ctx, thm, false, ca);
+    }
+
+
+    // / Demonstrates how to handle parser errors using Z3 error handling
+    // support.
+
+    // / <remarks></remarks>
+    public void parserExample5(Context ctx)
+    {
+        System.out.println("ParserExample5");
+
+        try
+        {
+            ctx.parseSMTLIB2String(
+                    /*
+                     * the following string has a parsing error: missing
+                     * parenthesis
+                     */
+                    "(declare-const x Int (declare-const y Int)) (assert (> x y))",
+                    null, null, null, null);
+        } catch (Z3Exception e)
+        {
+            System.out.printf("Z3 error: %s%n", e);
+        }
+    }
+
+    // / Create an ite-Expr (if-then-else Exprs).
+
+    public void iteExample(Context ctx)
+    {
+        System.out.println("ITEExample");
+        Log.append("ITEExample");
+
+        BoolExpr f = ctx.mkFalse();
+        IntNum one = ctx.mkInt(1);
+        IntNum zero = ctx.mkInt(0);
+        Expr<IntSort> ite = ctx.mkITE(f, one, zero);
+
+        System.out.printf("Expr: %s%n", ite);
+    }
+
+    // / Create an enumeration data type.
+
+    public <T extends Sort> void enumExampleTyped(Context ctx) throws TestFailedException
+    {
+        System.out.println("EnumExample");
+        Log.append("EnumExample");
+
+        Symbol name = ctx.mkSymbol("fruit");
+
+        EnumSort<T> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple"),
+                ctx.mkSymbol("banana"), ctx.mkSymbol("orange"));
+
+        // helper function for consistent typing: https://docs.oracle.com/javase/tutorial/java/generics/capture.html
+        System.out.println((fruit.getConsts()[0]));
+        System.out.println((fruit.getConsts()[1]));
+        System.out.println((fruit.getConsts()[2]));
+
+        System.out.println((fruit.getTesterDecls()[0]));
+        System.out.println((fruit.getTesterDecls()[1]));
+        System.out.println((fruit.getTesterDecls()[2]));
+
+        Expr<EnumSort<T>> apple = fruit.getConsts()[0];
+        Expr<EnumSort<T>> banana = fruit.getConsts()[1];
+        Expr<EnumSort<T>> orange = fruit.getConsts()[2];
+
+        /* Apples are different from oranges */
+        prove(ctx, ctx.mkNot(ctx.mkEq(apple, orange)), false);
+
+        /* Apples pass the apple test */
+        prove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], apple),
+                false);
+
+        /* Oranges fail the apple test */
+        disprove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], orange), false);
+        prove(ctx, ctx.mkNot(ctx.mkApp(fruit.getTesterDecls()[0], orange)), false);
+
+        Expr<EnumSort<T>> fruity = ctx.mkConst("fruity", fruit);
+
+        /* If something is fruity, then it is an apple, banana, or orange */
+
+        prove(ctx, ctx.mkOr(ctx.mkEq(fruity, apple), ctx.mkEq(fruity, banana), ctx.mkEq(fruity, orange)), false);
+    }
+
+    // while you can do this untyped, it's safer to have a helper function -- this will prevent you from
+    // mixing up your enum types
+    public void enumExampleUntyped(Context ctx) throws TestFailedException
+    {
+        System.out.println("EnumExample");
+        Log.append("EnumExample");
+
+        Symbol name = ctx.mkSymbol("fruit");
+
+        EnumSort<Object> fruit = ctx.mkEnumSort(name, ctx.mkSymbol("apple"),
+                ctx.mkSymbol("banana"), ctx.mkSymbol("orange"));
+
+        System.out.println((fruit.getConsts()[0]));
+        System.out.println((fruit.getConsts()[1]));
+        System.out.println((fruit.getConsts()[2]));
+
+        System.out.println((fruit.getTesterDecls()[0]));
+        System.out.println((fruit.getTesterDecls()[1]));
+        System.out.println((fruit.getTesterDecls()[2]));
+
+        Expr<EnumSort<Object>> apple = fruit.getConsts()[0];
+        Expr<EnumSort<Object>> banana = fruit.getConsts()[1];
+        Expr<EnumSort<Object>> orange = fruit.getConsts()[2];
+
+        /* Apples are different from oranges */
+        prove(ctx, ctx.mkNot(ctx.mkEq(apple, orange)), false);
+
+        /* Apples pass the apple test */
+        prove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], apple),
+                false);
+
+        /* Oranges fail the apple test */
+        disprove(ctx, ctx.mkApp(fruit.getTesterDecls()[0], orange), false);
+        prove(ctx, ctx.mkNot(ctx.mkApp(fruit.getTesterDecls()[0], orange)), false);
+
+        Expr<EnumSort<Object>> fruity = ctx.mkConst("fruity", fruit);
+
+        /* If something is fruity, then it is an apple, banana, or orange */
+
+        prove(ctx, ctx.mkOr(ctx.mkEq(fruity, apple), ctx.mkEq(fruity, banana), ctx.mkEq(fruity, orange)), false);
+    }
+
+    // / Create a list datatype.
+
+    @SuppressWarnings("unchecked")
+    public void listExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("ListExample");
+        Log.append("ListExample");
+
+        IntSort int_ty = ctx.mkIntSort();
+
+        ListSort<IntSort> int_list = ctx.mkListSort(ctx.mkSymbol("int_list"), int_ty);
+
+        Expr<ListSort<IntSort>> nil = ctx.mkConst(int_list.getNilDecl());
+        Expr<ListSort<IntSort>> l1 = ctx.mkApp(int_list.getConsDecl(), ctx.mkInt(1), nil);
+        Expr<ListSort<IntSort>> l2 = ctx.mkApp(int_list.getConsDecl(), ctx.mkInt(2), nil);
+
+        /* nil != cons(1, nil) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false);
+
+        /* cons(2,nil) != cons(1, nil) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(l1, l2)), false);
+
+        /* cons(x,nil) = cons(y, nil) => x = y */
+        Expr<IntSort> x = ctx.mkConst("x", int_ty);
+        Expr<IntSort> y = ctx.mkConst("y", int_ty);
+        l1 = ctx.mkApp(int_list.getConsDecl(), x, nil);
+        l2 = ctx.mkApp(int_list.getConsDecl(), y, nil);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false);
+
+        /* cons(x,u) = cons(x, v) => u = v */
+        Expr<ListSort<IntSort>> u = ctx.mkConst("u", int_list);
+        Expr<ListSort<IntSort>> v = ctx.mkConst("v", int_list);
+        l1 = ctx.mkApp(int_list.getConsDecl(), x, u);
+        l2 = ctx.mkApp(int_list.getConsDecl(), y, v);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false);
+
+        /* is_nil(u) or is_cons(u) */
+        prove(ctx, ctx.mkOr(ctx.mkApp(int_list.getIsNilDecl(), u), ctx.mkApp(int_list.getIsConsDecl(), u)), false);
+
+        /* occurs check u != cons(x,u) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false);
+
+        /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
+        BoolExpr fml1 = ctx.mkEq(u, ctx.mkApp(int_list.getConsDecl(),
+                        ctx.mkApp(int_list.getHeadDecl(), u),
+                        ctx.mkApp(int_list.getTailDecl(), u)));
+        BoolExpr fml = ctx.mkImplies(ctx.mkApp(int_list.getIsConsDecl(), u), fml1);
+        System.out.printf("Formula %s%n", fml);
+
+        prove(ctx, fml, false);
+
+        disprove(ctx, fml1, false);
+    }
+
+    // / Create a binary tree datatype.
+
+    @SuppressWarnings("unchecked")
+    public <Tree> void treeExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("TreeExample");
+        Log.append("TreeExample");
+
+        String[] head_tail = new String[] { "car", "cdr" };
+        Sort[] sorts = new Sort[] { null, null };
+        int[] sort_refs = new int[] { 0, 0 };
+        Constructor<Tree> nil_con, cons_con;
+
+        nil_con = ctx.mkConstructor("nil", "is_nil", null, null, null);
+        cons_con = ctx.mkConstructor("cons", "is_cons", head_tail, sorts,
+                sort_refs);
+        Constructor<Tree>[] constructors = new Constructor[] { nil_con, cons_con };
+
+        DatatypeSort<Tree> cell = ctx.mkDatatypeSort("cell", constructors);
+
+        FuncDecl<DatatypeSort<Tree>> nil_decl = nil_con.ConstructorDecl();
+        FuncDecl<BoolSort> is_nil_decl = nil_con.getTesterDecl();
+        FuncDecl<DatatypeSort<Tree>> cons_decl = cons_con.ConstructorDecl();
+        FuncDecl<BoolSort> is_cons_decl = cons_con.getTesterDecl();
+        FuncDecl<?>[] cons_accessors = cons_con.getAccessorDecls();
+        FuncDecl<?> car_decl = cons_accessors[0];
+        FuncDecl<?> cdr_decl = cons_accessors[1];
+
+        Expr<DatatypeSort<Tree>> nil = ctx.mkConst(nil_decl);
+        Expr<DatatypeSort<Tree>> l1 = ctx.mkApp(cons_decl, nil, nil);
+        Expr<DatatypeSort<Tree>> l2 = ctx.mkApp(cons_decl, l1, nil);
+
+        /* nil != cons(nil, nil) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(nil, l1)), false);
+
+        /* cons(x,u) = cons(x, v) => u = v */
+        Expr<DatatypeSort<Tree>> u = ctx.mkConst("u", cell);
+        Expr<DatatypeSort<Tree>> v = ctx.mkConst("v", cell);
+        Expr<DatatypeSort<Tree>> x = ctx.mkConst("x", cell);
+        Expr<DatatypeSort<Tree>> y = ctx.mkConst("y", cell);
+        l1 = ctx.mkApp(cons_decl, x, u);
+        l2 = ctx.mkApp(cons_decl, y, v);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false);
+
+        /* is_nil(u) or is_cons(u) */
+        prove(ctx, ctx.mkOr(ctx.mkApp(is_nil_decl, u), ctx.mkApp(is_cons_decl, u)), false);
+
+        /* occurs check u != cons(x,u) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false);
+
+        /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
+        BoolExpr fml1 = ctx.mkEq(u, ctx.mkApp(cons_decl, ctx.mkApp(car_decl, u), ctx.mkApp(cdr_decl, u)));
+        BoolExpr fml = ctx.mkImplies(ctx.mkApp(is_cons_decl, u), fml1);
+        System.out.printf("Formula %s%n", fml);
+        prove(ctx, fml, false);
+
+        disprove(ctx, fml1, false);
+    }
+
+    // / Create a forest of trees.
+
+    // / <remarks>
+    // / forest ::= nil | cons(tree, forest)
+    // / tree ::= nil | cons(forest, forest)
+    // / </remarks>
+    @SuppressWarnings({"unchecked", "unused", "UnusedAssignment"})
+    public <Tree, Forest> void forestExample(Context ctx) throws TestFailedException
+    {
+        System.out.println("ForestExample");
+        Log.append("ForestExample");
+
+        DatatypeSort<Forest> forest;
+        DatatypeSort<Tree> tree;
+        FuncDecl<DatatypeSort<Forest>> nil1_decl, cons1_decl, cdr1_decl, car2_decl, cdr2_decl;
+        FuncDecl<DatatypeSort<Tree>> car1_decl, nil2_decl, cons2_decl;
+        FuncDecl<BoolSort> is_nil1_decl, is_nil2_decl, is_cons1_decl, is_cons2_decl;
+
+        //
+        // Declare the names of the accessors for cons.
+        // Then declare the sorts of the accessors.
+        // For this example, all sorts refer to the new types 'forest' and
+        // 'tree'
+        // being declared, so we pass in null for both sorts1 and sorts2.
+        // On the other hand, the sort_refs arrays contain the indices of the
+        // two new sorts being declared. The first element in sort1_refs
+        // points to 'tree', which has index 1, the second element in sort1_refs
+        // array points to 'forest', which has index 0.
+        //
+        Symbol[] head_tail1 = new Symbol[] { ctx.mkSymbol("head"),
+                ctx.mkSymbol("tail") };
+        Sort[] sorts1 = new Sort[] { null, null };
+        int[] sort1_refs = new int[] { 1, 0 }; // the first item points to a
+                                               // tree, the second to a forest
+
+        Symbol[] head_tail2 = new Symbol[] { ctx.mkSymbol("car"),
+                ctx.mkSymbol("cdr") };
+        Sort[] sorts2 = new Sort[] { null, null };
+        int[] sort2_refs = new int[] { 0, 0 }; // both items point to the forest
+                                               // datatype.
+        Constructor<Forest> nil1_con, cons1_con;
+        Constructor<Tree> nil2_con, cons2_con;
+        Constructor<Forest>[] constructors1 = new Constructor[2];
+        Constructor<Tree>[] constructors2 = new Constructor[2];
+        Symbol[] sort_names = { ctx.mkSymbol("forest"), ctx.mkSymbol("tree") };
+
+        /* build a forest */
+        nil1_con = ctx.mkConstructor(ctx.mkSymbol("nil1"),
+                ctx.mkSymbol("is_nil1"), null, null, null);
+        cons1_con = ctx.mkConstructor(ctx.mkSymbol("cons1"),
+                ctx.mkSymbol("is_cons1"), head_tail1, sorts1, sort1_refs);
+        constructors1[0] = nil1_con;
+        constructors1[1] = cons1_con;
+
+        /* build a tree */
+        nil2_con = ctx.mkConstructor(ctx.mkSymbol("nil2"),
+                ctx.mkSymbol("is_nil2"), null, null, null);
+        cons2_con = ctx.mkConstructor(ctx.mkSymbol("cons2"),
+                ctx.mkSymbol("is_cons2"), head_tail2, sorts2, sort2_refs);
+        constructors2[0] = nil2_con;
+        constructors2[1] = cons2_con;
+
+        Constructor<Object>[][] clists = new Constructor[][] { constructors1,
+                constructors2 };
+
+        Sort[] sorts = ctx.mkDatatypeSorts(sort_names, clists);
+        forest = (DatatypeSort<Forest>) sorts[0];
+        tree = (DatatypeSort<Tree>) sorts[1];
+
+        //
+        // Now that the datatype has been created.
+        // Query the constructors for the constructor
+        // functions, testers, and field accessors.
+        //
+        nil1_decl = nil1_con.ConstructorDecl();
+        is_nil1_decl = nil1_con.getTesterDecl();
+        cons1_decl = cons1_con.ConstructorDecl();
+        is_cons1_decl = cons1_con.getTesterDecl();
+        FuncDecl<?>[] cons1_accessors = cons1_con.getAccessorDecls();
+        car1_decl = (FuncDecl<DatatypeSort<Tree>>) cons1_accessors[0];
+        cdr1_decl = (FuncDecl<DatatypeSort<Forest>>) cons1_accessors[1];
+
+        nil2_decl = nil2_con.ConstructorDecl();
+        is_nil2_decl = nil2_con.getTesterDecl();
+        cons2_decl = cons2_con.ConstructorDecl();
+        is_cons2_decl = cons2_con.getTesterDecl();
+        FuncDecl<?>[] cons2_accessors = cons2_con.getAccessorDecls();
+        car2_decl = (FuncDecl<DatatypeSort<Forest>>) cons2_accessors[0];
+        cdr2_decl = (FuncDecl<DatatypeSort<Forest>>) cons2_accessors[1];
+
+        Expr<DatatypeSort<Forest>> nil1 = ctx.mkConst(nil1_decl);
+        Expr<DatatypeSort<Tree>> nil2 = ctx.mkConst(nil2_decl);
+        Expr<DatatypeSort<Forest>> f1 = ctx.mkApp(cons1_decl, nil2, nil1);
+        Expr<DatatypeSort<Tree>> t1 = ctx.mkApp(cons2_decl, nil1, nil1);
+        Expr<DatatypeSort<Tree>> t2 = ctx.mkApp(cons2_decl, f1, nil1);
+        Expr<DatatypeSort<Tree>> t3 = ctx.mkApp(cons2_decl, f1, f1);
+        Expr<DatatypeSort<Tree>> t4 = ctx.mkApp(cons2_decl, nil1, f1);
+        Expr<DatatypeSort<Forest>> f2 = ctx.mkApp(cons1_decl, t1, nil1);
+        Expr<DatatypeSort<Forest>> f3 = ctx.mkApp(cons1_decl, t1, f1);
+
+        /* nil != cons(nil,nil) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(nil1, f1)), false);
+        prove(ctx, ctx.mkNot(ctx.mkEq(nil2, t1)), false);
+
+        /* cons(x,u) = cons(x, v) => u = v */
+        Expr<DatatypeSort<Forest>> u = ctx.mkConst("u", forest);
+        Expr<DatatypeSort<Forest>> v = ctx.mkConst("v", forest);
+        Expr<DatatypeSort<Tree>> x = ctx.mkConst("x", tree);
+        Expr<DatatypeSort<Tree>> y = ctx.mkConst("y", tree);
+        Expr<DatatypeSort<Forest>> l1 = ctx.mkApp(cons1_decl, x, u);
+        Expr<DatatypeSort<Forest>> l2 = ctx.mkApp(cons1_decl, y, v);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(u, v)), false);
+        prove(ctx, ctx.mkImplies(ctx.mkEq(l1, l2), ctx.mkEq(x, y)), false);
+
+        /* is_nil(u) or is_cons(u) */
+        prove(ctx, ctx.mkOr(ctx.mkApp(is_nil1_decl, u), ctx.mkApp(is_cons1_decl, u)), false);
+
+        /* occurs check u != cons(x,u) */
+        prove(ctx, ctx.mkNot(ctx.mkEq(u, l1)), false);
+    }
+
+    // / Demonstrate how to use #Eval.
+
+    public void evalExample1(Context ctx)
+    {
+        System.out.println("EvalExample1");
+        Log.append("EvalExample1");
+
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntNum two = ctx.mkInt(2);
+
+        Solver solver = ctx.mkSolver();
+
+        /* assert x < y */
+        solver.add(ctx.mkLt(x, y));
+
+        /* assert x > 2 */
+        solver.add(ctx.mkGt(x, two));
+
+        /* find model for the constraints above */
+        Model model = null;
+        if (Status.SATISFIABLE == solver.check())
+        {
+            model = solver.getModel();
+            System.out.println(model);
+            System.out.println("\nevaluating x+y");
+            Expr<IntSort> v = model.evaluate(ctx.mkAdd(x, y), false);
+            if (v != null)
+            {
+                System.out.printf("result = %s%n", v);
+            } else
+            {
+                System.out.println("Failed to evaluate: x+y");
+            }
+        } else
+        {
+            System.out.println("BUG, the constraints are satisfiable.");
+        }
+    }
+
+    // / Demonstrate how to use #Eval on tuples.
+
+    @SuppressWarnings("unchecked")
+    public void evalExample2(Context ctx)
+    {
+        System.out.println("EvalExample2");
+        Log.append("EvalExample2");
+
+        IntSort int_type = ctx.getIntSort();
+        TupleSort tuple = ctx.mkTupleSort(ctx.mkSymbol("mk_tuple"), // name of
+                                                                    // tuple
+                                                                    // constructor
+                new Symbol[] { ctx.mkSymbol("first"), ctx.mkSymbol("second") }, // names
+                                                                                // of
+                                                                                // projection
+                                                                                // operators
+                new Sort[] { int_type, int_type } // types of projection
+                                                  // operators
+                );
+        FuncDecl<IntSort> first = (FuncDecl<IntSort>) tuple.getFieldDecls()[0]; // declarations are for
+                                                   // projections
+        FuncDecl<IntSort> second = (FuncDecl<IntSort>) tuple.getFieldDecls()[1];
+        Expr<TupleSort> tup1 = ctx.mkConst("t1", tuple);
+        Expr<TupleSort> tup2 = ctx.mkConst("t2", tuple);
+
+        Solver solver = ctx.mkSolver();
+
+        /* assert tup1 != tup2 */
+        solver.add(ctx.mkNot(ctx.mkEq(tup1, tup2)));
+        /* assert first tup1 = first tup2 */
+        solver.add(ctx.mkEq(ctx.mkApp(first, tup1), ctx.mkApp(first, tup2)));
+
+        /* find model for the constraints above */
+        Model model = null;
+        if (Status.SATISFIABLE == solver.check())
+        {
+            model = solver.getModel();
+            System.out.println(model);
+            System.out.printf("evaluating tup1 %s%n", model.evaluate(tup1, false));
+            System.out.printf("evaluating tup2 %s%n", model.evaluate(tup2, false));
+            System.out.printf("evaluating second(tup2) %s%n", model.evaluate(ctx.mkApp(second, tup2), false));
+        } else
+        {
+            System.out.println("BUG, the constraints are satisfiable.");
+        }
+    }
+
+    // / Demonstrate how to use <code>Push</code>and <code>Pop</code>to
+    // / control the size of models.
+
+    // / <remarks>Note: this test is specialized to 32-bit bitvectors.</remarks>
+    public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize)
+    {
+        int num_Exprs = to_minimize.length;
+        int[] upper = new int[num_Exprs];
+        int[] lower = new int[num_Exprs];
+        for (int i = 0; i < upper.length; ++i)
+        {
+            upper[i] = Integer.MAX_VALUE;
+            lower[i] = 0;
+        }
+        boolean some_work = true;
+        int last_index = -1;
+        int last_upper = 0;
+        while (some_work)
+        {
+            solver.push();
+
+            boolean check_is_sat = true;
+            while (some_work)
+            {
+                // Assert all feasible bounds.
+                for (int i = 0; i < num_Exprs; ++i)
+                {
+                    solver.add(ctx.mkBVULE(to_minimize[i],
+                            ctx.mkBV(upper[i], 32)));
+                }
+
+                check_is_sat = Status.SATISFIABLE == solver.check();
+                if (!check_is_sat)
+                {
+                    if (last_index != -1)
+                    {
+                        lower[last_index] = last_upper + 1;
+                    }
+                    break;
+                }
+                System.out.println(solver.getModel());
+
+                // narrow the bounds based on the current model.
+                for (int i = 0; i < num_Exprs; ++i)
+                {
+                    Expr<BitVecSort> v = solver.getModel().evaluate(to_minimize[i], false);
+                    // we still have to cast because we want to use a method in BitVecNum
+                    // however, we cannot cast to a type which doesn't match the generic, e.g. IntNum
+                    int ui = ((BitVecNum) v).getInt();
+                    if (ui < upper[i])
+                    {
+                        upper[i] = ui;
+                    }
+                    System.out.printf("%d %d %d%n", i, lower[i], upper[i]);
+                }
+
+                // find a new bound to add
+                some_work = false;
+                last_index = 0;
+                for (int i = 0; i < num_Exprs; ++i)
+                {
+                    if (lower[i] < upper[i])
+                    {
+                        last_upper = (upper[i] + lower[i]) / 2;
+                        last_index = i;
+                        solver.add(ctx.mkBVULE(to_minimize[i],
+                                ctx.mkBV(last_upper, 32)));
+                        some_work = true;
+                        break;
+                    }
+                }
+            }
+            solver.pop();
+        }
+    }
+
+    // / Reduced-size model generation example.
+
+    public void findSmallModelExample(Context ctx)
+    {
+        System.out.println("FindSmallModelExample");
+        Log.append("FindSmallModelExample");
+
+        BitVecExpr x = ctx.mkBVConst("x", 32);
+        BitVecExpr y = ctx.mkBVConst("y", 32);
+        BitVecExpr z = ctx.mkBVConst("z", 32);
+
+        Solver solver = ctx.mkSolver();
+
+        solver.add(ctx.mkBVULE(x, ctx.mkBVAdd(y, z)));
+        checkSmall(ctx, solver, x, y, z);
+    }
+
+    // / Simplifier example.
+
+    @SuppressWarnings("unchecked")
+    public void simplifierExample(Context ctx)
+    {
+        System.out.println("SimplifierExample");
+        Log.append("SimplifierExample");
+
+        IntExpr x = ctx.mkIntConst("x");
+        IntExpr y = ctx.mkIntConst("y");
+        IntExpr z = ctx.mkIntConst("z");
+        @SuppressWarnings("unused")
+        IntExpr u = ctx.mkIntConst("u");
+
+        ArithExpr<IntSort> t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z)));
+        Expr<IntSort> t2 = t1.simplify();
+        System.out.printf("%s -> %s%n", t1, t2);
+    }
+
+    // / Extract unsatisfiable core example
+
+    public void unsatCoreAndProofExample(Context ctx)
+    {
+        System.out.println("UnsatCoreAndProofExample");
+        Log.append("UnsatCoreAndProofExample");
+
+        Solver solver = ctx.mkSolver();
+
+        BoolExpr pa = ctx.mkBoolConst("PredA");
+        BoolExpr pb = ctx.mkBoolConst("PredB");
+        BoolExpr pc = ctx.mkBoolConst("PredC");
+        BoolExpr pd = ctx.mkBoolConst("PredD");
+        BoolExpr p1 = ctx.mkBoolConst("P1");
+        BoolExpr p2 = ctx.mkBoolConst("P2");
+        BoolExpr p3 = ctx.mkBoolConst("P3");
+        BoolExpr p4 = ctx.mkBoolConst("P4");
+        BoolExpr[] assumptions = new BoolExpr[] { ctx.mkNot(p1), ctx.mkNot(p2),
+                ctx.mkNot(p3), ctx.mkNot(p4) };
+        BoolExpr f1 = ctx.mkAnd(pa, pb, pc);
+        BoolExpr f2 = ctx.mkAnd(pa, ctx.mkNot(pb), pc);
+        BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc));
+        BoolExpr f4 = pd;
+
+        solver.add(ctx.mkOr(f1, p1));
+        solver.add(ctx.mkOr(f2, p2));
+        solver.add(ctx.mkOr(f3, p3));
+        solver.add(ctx.mkOr(f4, p4));
+        Status result = solver.check(assumptions);
+
+        if (result == Status.UNSATISFIABLE)
+        {
+            System.out.println("unsat");
+            System.out.printf("proof: %s%n", solver.getProof());
+            System.out.println("core: ");
+            for (Expr<?> c : solver.getUnsatCore())
+            {
+                System.out.println(c);
+            }
+        }
+    }
+
+    /// Extract unsatisfiable core example with AssertAndTrack
+
+    public void unsatCoreAndProofExample2(Context ctx)
+    {
+        System.out.println("UnsatCoreAndProofExample2");
+        Log.append("UnsatCoreAndProofExample2");
+
+        Solver solver = ctx.mkSolver();
+
+        BoolExpr pa = ctx.mkBoolConst("PredA");
+        BoolExpr pb = ctx.mkBoolConst("PredB");
+        BoolExpr pc = ctx.mkBoolConst("PredC");
+        BoolExpr pd = ctx.mkBoolConst("PredD");
+
+        BoolExpr f1 = ctx.mkAnd(new BoolExpr[] { pa, pb, pc });
+        BoolExpr f2 = ctx.mkAnd(new BoolExpr[] { pa, ctx.mkNot(pb), pc });
+        BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc));
+        BoolExpr f4 = pd;
+
+        BoolExpr p1 = ctx.mkBoolConst("P1");
+        BoolExpr p2 = ctx.mkBoolConst("P2");
+        BoolExpr p3 = ctx.mkBoolConst("P3");
+        BoolExpr p4 = ctx.mkBoolConst("P4");
+
+        solver.assertAndTrack(f1, p1);
+        solver.assertAndTrack(f2, p2);
+        solver.assertAndTrack(f3, p3);
+        solver.assertAndTrack(f4, p4);
+        Status result = solver.check();
+
+        if (result == Status.UNSATISFIABLE)
+        {
+            System.out.println("unsat");
+            System.out.println("core: ");
+            for (Expr<?> c : solver.getUnsatCore())
+            {
+                System.out.println(c);
+            }
+        }
+    }
+
+    public <S, T> void finiteDomainExample(Context ctx)
+    {
+        System.out.println("FiniteDomainExample");
+        Log.append("FiniteDomainExample");
+
+        FiniteDomainSort<S> s = ctx.mkFiniteDomainSort("S", 10);
+        FiniteDomainSort<T> t = ctx.mkFiniteDomainSort("T", 10);
+        FiniteDomainNum<S> s1 = (FiniteDomainNum<S>) ctx.mkNumeral(1, s);
+        FiniteDomainNum<T> t1 = (FiniteDomainNum<T>) ctx.mkNumeral(1, t);
+        System.out.println(s);
+        System.out.println(t);
+        System.out.println(s1);
+        System.out.println(t1);
+        System.out.println(s1.getInt());
+        System.out.println(t1.getInt());
+        // But you cannot mix numerals of different sorts
+        // even if the size of their domains are the same:
+        // System.out.println(ctx.mkEq(s1, t1));
+    }
+
+    public void floatingPointExample1(Context ctx) throws TestFailedException
+    {
+        System.out.println("FloatingPointExample1");
+        Log.append("FloatingPointExample1");
+
+        FPSort s = ctx.mkFPSort(11, 53);
+        System.out.printf("Sort: %s%n", s);
+
+        FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */
+        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.printf("x=%s; y=%s; z=%s%n", x.toString(), y.toString(), z.toString());
+
+        BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z));
+        check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE);
+
+        /* nothing is equal to NaN according to floating-point
+         * equality, so NaN == k should be unsatisfiable. */
+        FPExpr k = (FPExpr)ctx.mkConst("x", s);
+        FPExpr nan = ctx.mkFPNaN(s);
+
+        /* solver that runs the default tactic for QF_FP. */
+        Solver slvr = ctx.mkSolver("QF_FP");
+        slvr.add(ctx.mkFPEq(nan, k));
+        if (slvr.check() != Status.UNSATISFIABLE)
+            throw new TestFailedException();
+        System.out.printf("OK, unsat:%n%s%n", slvr);
+
+        /* NaN is equal to NaN according to normal equality. */
+        slvr = ctx.mkSolver("QF_FP");
+        slvr.add(ctx.mkEq(nan, nan));
+        if (slvr.check() != Status.SATISFIABLE)
+            throw new TestFailedException();
+        System.out.printf("OK, sat:%n%s%n", slvr);
+
+        /* Let's prove -1e1 * -1.25e3 == +100 */
+        x = (FPNum)ctx.mkNumeral("-1e1", s);
+        y = (FPNum)ctx.mkNumeral("-1.25p3", s);
+        FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s);
+        FPNum r = (FPNum)ctx.mkNumeral("100", s);
+        slvr = ctx.mkSolver("QF_FP");
+
+        slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y)));
+        slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r)));
+        if (slvr.check() != Status.UNSATISFIABLE)
+            throw new TestFailedException();
+        System.out.printf("OK, unsat:%n%s%n", slvr);
+    }
+
+    public void floatingPointExample2(Context ctx) throws TestFailedException
+    {
+        System.out.println("FloatingPointExample2");
+        Log.append("FloatingPointExample2");
+        FPSort double_sort = ctx.mkFPSort(11, 53);
+        FPRMSort rm_sort = ctx.mkFPRoundingModeSort();
+
+        FPRMExpr rm = (FPRMExpr)ctx.mkConst(ctx.mkSymbol("rm"), rm_sort);
+        BitVecExpr x = (BitVecExpr)ctx.mkConst(ctx.mkSymbol("x"), ctx.mkBitVecSort(64));
+        FPExpr y = (FPExpr)ctx.mkConst(ctx.mkSymbol("y"), double_sort);
+        FPExpr fp_val = ctx.mkFP(42, double_sort);
+
+        BoolExpr c1 = ctx.mkEq(y, fp_val);
+        BoolExpr c2 = ctx.mkEq(x, ctx.mkFPToBV(rm, y, 64, false));
+        BoolExpr c3 = ctx.mkEq(x, ctx.mkBV(42, 64));
+        BoolExpr c4 = ctx.mkEq(ctx.mkNumeral(42, ctx.getRealSort()), ctx.mkFPToReal(fp_val));
+        BoolExpr c5 = ctx.mkAnd(c1, c2, c3, c4);
+        System.out.printf("c5 = %s%n", c5);
+
+        /* Generic solver */
+        Solver s = ctx.mkSolver();
+        s.add(c5);
+
+        if (s.check() != Status.SATISFIABLE)
+            throw new TestFailedException();
+
+        System.out.printf("OK, model: %s%n", s.getModel());
+    }
+
+    @SuppressWarnings("unchecked")
+    public void optimizeExample(Context ctx)
+    {
+        System.out.println("Opt");
+
+        Optimize opt = ctx.mkOptimize();
+
+        // Set constraints.
+        IntExpr xExp = ctx.mkIntConst("x");
+        IntExpr yExp = ctx.mkIntConst("y");
+
+        opt.Add(ctx.mkEq(ctx.mkAdd(xExp, yExp), ctx.mkInt(10)),
+                ctx.mkGe(xExp, ctx.mkInt(0)),
+                ctx.mkGe(yExp, ctx.mkInt(0)));
+
+        // Set objectives.
+        Optimize.Handle<IntSort> mx = opt.MkMaximize(xExp);
+        Optimize.Handle<IntSort> my = opt.MkMaximize(yExp);
+
+        System.out.println(opt.Check());
+        System.out.println(mx);
+        System.out.println(my);
+    }
+
+    public void translationExample() {
+        Context ctx1 = new Context();
+        Context ctx2 = new Context();
+
+        Sort s1 = ctx1.getIntSort();
+        Sort s2 = ctx2.getIntSort();
+        Sort s3 = s1.translate(ctx2);
+
+        System.out.println(s1 == s2);
+        System.out.println(s1.equals(s2));
+        System.out.println(s2.equals(s3));
+        System.out.println(s1.equals(s3));
+
+        IntExpr e1 = ctx1.mkIntConst("e1");
+        IntExpr e2 = ctx2.mkIntConst("e1");
+        Expr<IntSort> e3 = e1.translate(ctx2);
+
+        System.out.println(e1 == e2);
+        System.out.println(e1.equals(e2));
+        System.out.println(e2.equals(e3));
+        System.out.println(e1.equals(e3));
+    }
+
+    public static void main(String[] args)
+    {
+        JavaGenericExample p = new JavaGenericExample();
+        try
+        {
+            Global.ToggleWarningMessages(true);
+            Log.open("test.log");
+
+            System.out.print("Z3 Major Version: ");
+            System.out.println(Version.getMajor());
+            System.out.print("Z3 Full Version: ");
+            System.out.println(Version.getString());
+            System.out.print("Z3 Full Version String: ");
+            System.out.println(Version.getFullVersion());
+
+            p.simpleExample();
+
+            { // These examples need model generation turned on.
+                HashMap<String, String> cfg = new HashMap<>();
+                cfg.put("model", "true");
+                Context ctx = new Context(cfg);
+
+                p.optimizeExample(ctx);
+                p.basicTests(ctx);
+                p.sudokuExample(ctx);
+                p.quantifierExample1(ctx);
+                p.quantifierExample2(ctx);
+                p.logicExample(ctx);
+                p.parOrExample(ctx);
+                p.findModelExample1(ctx);
+                p.findModelExample2(ctx);
+                p.pushPopExample1(ctx);
+                p.arrayExample1(ctx);
+                p.arrayExample3(ctx);
+                p.bitvectorExample1(ctx);
+                p.bitvectorExample2(ctx);
+                p.parserExample1(ctx);
+                p.parserExample2(ctx);
+                p.parserExample5(ctx);
+                p.iteExample(ctx);
+                p.evalExample1(ctx);
+                p.evalExample2(ctx);
+                p.findSmallModelExample(ctx);
+                p.simplifierExample(ctx);
+                p.finiteDomainExample(ctx);
+                p.floatingPointExample1(ctx);
+                // core dumps: p.floatingPointExample2(ctx);
+            }
+
+            { // These examples need proof generation turned on.
+                HashMap<String, String> cfg = new HashMap<>();
+                cfg.put("proof", "true");
+                Context ctx = new Context(cfg);
+                p.proveExample1(ctx);
+                p.proveExample2(ctx);
+                p.arrayExample2(ctx);
+                p.tupleExample(ctx);
+                // throws p.parserExample3(ctx);
+                p.enumExampleTyped(ctx);
+                p.enumExampleUntyped(ctx);
+                p.listExample(ctx);
+                p.treeExample(ctx);
+                p.forestExample(ctx);
+                p.unsatCoreAndProofExample(ctx);
+                p.unsatCoreAndProofExample2(ctx);
+            }
+
+            { // These examples need proof generation turned on and auto-config
+              // set to false.
+                HashMap<String, String> cfg = new HashMap<>();
+                cfg.put("proof", "true");
+                cfg.put("auto-config", "false");
+                Context ctx = new Context(cfg);
+                p.quantifierExample3(ctx);
+                p.quantifierExample4(ctx);
+            }
+
+            p.translationExample();
+
+            Log.close();
+            if (Log.isOpen())
+                System.out.println("Log is still open!");
+        } catch (Z3Exception ex)
+        {
+            System.out.printf("Z3 Managed Exception: %s%n", ex.getMessage());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);
+        } catch (TestFailedException ex)
+        {
+            System.out.printf("TEST CASE FAILED: %s%n", ex.getMessage());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);
+        } catch (Exception ex)
+        {
+            System.out.printf("Unknown Exception: %s%n", ex.getMessage());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);
+        }
+    }
+}
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 350830443f3..c28c0cfcba7 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -204,7 +204,7 @@ static AST create(Context ctx, long obj)
         switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
         {
         case Z3_FUNC_DECL_AST:
-            return new FuncDecl(ctx, obj);
+            return new FuncDecl<>(ctx, obj);
         case Z3_QUANTIFIER_AST:
             return new Quantifier(ctx, obj);
         case Z3_SORT_AST:
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 4ee53103503..a6b436a99f4 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -126,9 +126,9 @@ public AST[] ToArray()
     /**
      * Translates the AST vector into an Expr[]
      * */
-    public Expr[] ToExprArray() {
+    public Expr<?>[] ToExprArray() {
         int n = size();
-        Expr[] res = new Expr[n];
+        Expr<?>[] res = new Expr[n];
         for (int i = 0; i < n; i++)
             res[i] = Expr.create(getContext(), get(i).getNativeObject());
         return res;    
@@ -161,36 +161,36 @@ public BitVecExpr[] ToBitVecExprArray()
     /**
      * Translates the AST vector into an ArithExpr[]
      * */   
-    public ArithExpr[] ToArithExprExprArray()
+    public ArithExpr<?>[] ToArithExprExprArray()
     {
         int n = size();
-        ArithExpr[] res = new ArithExpr[n];
+        ArithExpr<?>[] res = new ArithExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (ArithExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 
     /**
      * Translates the AST vector into an ArrayExpr[]
      * */  
-    public ArrayExpr[] ToArrayExprArray()
+    public ArrayExpr<?, ?>[] ToArrayExprArray()
     {
         int n = size();
-        ArrayExpr[] res = new ArrayExpr[n];
+        ArrayExpr<?, ?>[] res = new ArrayExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (ArrayExpr<?, ?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 
     /**
      * Translates the AST vector into an DatatypeExpr[]
      * */ 
-    public DatatypeExpr[] ToDatatypeExprArray()
+    public DatatypeExpr<?>[] ToDatatypeExprArray()
     {
         int n = size();
-        DatatypeExpr[] res = new DatatypeExpr[n];
+        DatatypeExpr<?>[] res = new DatatypeExpr[n];
         for (int i = 0; i < n; i++)
-            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
+            res[i] = (DatatypeExpr<?>)Expr.create(getContext(), get(i).getNativeObject());
         return res;
     }
 
diff --git a/src/api/java/ArithExpr.java b/src/api/java/ArithExpr.java
index d92d8523bb3..f26eb8b6b61 100644
--- a/src/api/java/ArithExpr.java
+++ b/src/api/java/ArithExpr.java
@@ -20,7 +20,7 @@
 /**
  * Arithmetic expressions (int/real)
  **/
-public class ArithExpr extends Expr
+public class ArithExpr<R extends ArithSort> extends Expr<R>
 {
     /**
      * Constructor for ArithExpr
diff --git a/src/api/java/ArrayExpr.java b/src/api/java/ArrayExpr.java
index b8318b648a7..fe6c511811c 100644
--- a/src/api/java/ArrayExpr.java
+++ b/src/api/java/ArrayExpr.java
@@ -21,7 +21,7 @@
 /**
  * Array expressions
  **/
-public class ArrayExpr extends Expr
+public class ArrayExpr<D extends Sort, R extends Sort> extends Expr<ArraySort<D, R>>
 {
     /**
      * Constructor for ArrayExpr
diff --git a/src/api/java/ArraySort.java b/src/api/java/ArraySort.java
index db4d992ed0b..30f4178fac5 100644
--- a/src/api/java/ArraySort.java
+++ b/src/api/java/ArraySort.java
@@ -20,7 +20,8 @@
 /**
  * Array sorts.
  **/
-public class ArraySort extends Sort
+@SuppressWarnings("unchecked")
+public class ArraySort<D extends Sort, R extends Sort> extends Sort
 {
     /**
      * The domain of the array sort.
@@ -28,9 +29,9 @@ public class ArraySort extends Sort
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getDomain()
+    public D getDomain()
     {
-        return Sort.create(getContext(),
+        return (D) Sort.create(getContext(),
                 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
     }
 
@@ -40,9 +41,9 @@ public Sort getDomain()
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getRange()
+    public R getRange()
     {
-        return Sort.create(getContext(),
+        return (R) Sort.create(getContext(),
                 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
     }
 
@@ -51,13 +52,13 @@ public Sort getRange()
         super(ctx, obj);
     }
 
-    ArraySort(Context ctx, Sort domain, Sort range)
+    ArraySort(Context ctx, D domain, R range)
     {
         super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
                 range.getNativeObject()));
     }
 
-    ArraySort(Context ctx, Sort[] domains, Sort range)
+    ArraySort(Context ctx, Sort[] domains, R range)
     {
         super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
                 range.getNativeObject()));
diff --git a/src/api/java/BitVecExpr.java b/src/api/java/BitVecExpr.java
index 175da9d6692..b4d62b2d618 100644
--- a/src/api/java/BitVecExpr.java
+++ b/src/api/java/BitVecExpr.java
@@ -20,7 +20,7 @@
 /**
  * Bit-vector expressions
  **/
-public class BitVecExpr extends Expr
+public class BitVecExpr extends Expr<BitVecSort>
 {
 
     /**
diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java
index dc75b2e7c36..7907ca28693 100644
--- a/src/api/java/BoolExpr.java
+++ b/src/api/java/BoolExpr.java
@@ -20,7 +20,7 @@
 /**
  * Boolean expressions
  **/
-public class BoolExpr extends Expr {
+public class BoolExpr extends Expr<BoolSort> {
 
     /**
      * Constructor for BoolExpr
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index 87ab86c3fdc..59565f56509 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -20,7 +20,7 @@
 /**
  * Constructors are used for datatype sorts.
  **/
-public class Constructor extends Z3Object {
+public class Constructor<R> extends Z3Object {
     private final int n;
 
     Constructor(Context ctx, int n, long nativeObj) {
@@ -44,13 +44,13 @@ public int getNumFields()
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl ConstructorDecl()
+    public FuncDecl<DatatypeSort<R>> ConstructorDecl()
     {
         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);         
+        return new FuncDecl<>(getContext(), constructor.value);
     }
 
     /**
@@ -58,13 +58,13 @@ public FuncDecl ConstructorDecl()
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl getTesterDecl()
+    public FuncDecl<BoolSort> getTesterDecl()
     {
         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);
+        return new FuncDecl<>(getContext(), tester.value);
     }
 
     /**
@@ -72,15 +72,15 @@ public FuncDecl getTesterDecl()
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getAccessorDecls()
+    public FuncDecl<?>[] getAccessorDecls()
     {
         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);
-        FuncDecl[] t = new FuncDecl[n];
+        FuncDecl<?>[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            t[i] = new FuncDecl(getContext(), accessors[i]); 
+            t[i] = new FuncDecl<>(getContext(), accessors[i]);
         return t;
     }
 
@@ -94,7 +94,7 @@ void addToReferenceQueue() {
         getContext().getConstructorDRQ().storeReference(getContext(), this);
     }
 
-    static Constructor of(Context ctx, Symbol name, Symbol recognizer,
+    static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) {
         int n = AST.arrayLength(fieldNames);
 
@@ -111,7 +111,7 @@ static Constructor of(Context ctx, Symbol name, Symbol recognizer,
         long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
                 recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
                 Sort.arrayToNative(sorts), sortRefs);
-        return new Constructor(ctx, n, nativeObj);
+        return new Constructor<>(ctx, n, nativeObj);
 
     }
 }
diff --git a/src/api/java/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java
index 5003dde5f2c..a76b26bb73c 100644
--- a/src/api/java/ConstructorDecRefQueue.java
+++ b/src/api/java/ConstructorDecRefQueue.java
@@ -1,6 +1,6 @@
 package com.microsoft.z3;
 
-public class ConstructorDecRefQueue extends IDecRefQueue<Constructor> {
+public class ConstructorDecRefQueue extends IDecRefQueue<Constructor<?>> {
     public ConstructorDecRefQueue() {
         super();
     }
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index c79e08d9e32..d015c51c0ad 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -20,7 +20,7 @@
 /**
  * Lists of constructors
  **/
-public class ConstructorList extends Z3Object {
+public class ConstructorList<R> extends Z3Object {
 
     ConstructorList(Context ctx, long obj)
     {
@@ -37,7 +37,7 @@ void addToReferenceQueue() {
         getContext().getConstructorListDRQ().storeReference(getContext(), this);
     }
 
-    ConstructorList(Context ctx, Constructor[] constructors)
+    ConstructorList(Context ctx, Constructor<R>[] constructors)
     {
         super(ctx, Native.mkConstructorList(ctx.nCtx(),
                 constructors.length,
diff --git a/src/api/java/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java
index 1a24607313c..2f5dfcb3526 100644
--- a/src/api/java/ConstructorListDecRefQueue.java
+++ b/src/api/java/ConstructorListDecRefQueue.java
@@ -1,6 +1,6 @@
 package com.microsoft.z3;
 
-public class ConstructorListDecRefQueue extends IDecRefQueue<ConstructorList> {
+public class ConstructorListDecRefQueue extends IDecRefQueue<ConstructorList<?>> {
     public ConstructorListDecRefQueue() {
         super();
     }
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 06e4a0f60e1..dc3b2a0c393 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -32,6 +32,7 @@
  * related to terms and formulas that are created relative
  * to them. 
  **/
+@SuppressWarnings("unchecked")
 public class Context implements AutoCloseable {
     private long m_ctx;
     static final Object creation_lock = new Object();
@@ -119,7 +120,7 @@ Symbol[] mkSymbols(String[] names)
     private BoolSort m_boolSort = null;
     private IntSort m_intSort = null;
     private RealSort m_realSort = null;
-    private SeqSort m_stringSort = null;
+    private SeqSort<BitVecSort> m_stringSort = null;
 
     /**
      * Retrieves the Boolean sort of the context.
@@ -165,7 +166,7 @@ public BoolSort mkBoolSort()
     /**
      * Retrieves the Integer sort of the context.
      **/
-    public SeqSort getStringSort()
+    public SeqSort<BitVecSort> getStringSort()
     {
         if (m_stringSort == null) {
             m_stringSort = mkStringSort();
@@ -217,46 +218,46 @@ public BitVecSort mkBitVecSort(int size)
     /**
      * Create a new array sort.
      **/
-    public ArraySort mkArraySort(Sort domain, Sort range)
+    public <D extends Sort, R extends Sort> ArraySort<D, R> mkArraySort(D domain, R range)
     {
         checkContextMatch(domain);
         checkContextMatch(range);
-        return new ArraySort(this, domain, range);
+        return new ArraySort<>(this, domain, range);
     }
 
 
     /**
      * Create a new array sort.
      **/
-    public ArraySort mkArraySort(Sort[] domains, Sort range)
+    public <R extends Sort> ArraySort<?, R> mkArraySort(Sort[] domains, R range)
     {
         checkContextMatch(domains);
         checkContextMatch(range);
-        return new ArraySort(this, domains, range);
+        return new ArraySort<>(this, domains, range);
     }
 
     /**
      * Create a new string sort
      **/
-    public SeqSort mkStringSort()
+    public SeqSort<BitVecSort> mkStringSort()
     {
-        return new SeqSort(this, Native.mkStringSort(nCtx()));
+        return new SeqSort<>(this, Native.mkStringSort(nCtx()));
     }
 
     /**
      * Create a new sequence sort
      **/
-    public SeqSort mkSeqSort(Sort s)
+    public <R extends Sort> SeqSort<R> mkSeqSort(R s)
     {
-        return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
+        return new SeqSort<>(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
     }
 
     /**
      * Create a new regular expression sort
      **/
-    public ReSort mkReSort(Sort s)
+    public <R extends Sort> ReSort<R> mkReSort(R s)
     {
-        return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
+        return new ReSort<>(this, Native.mkReSort(nCtx(), s.getNativeObject()));
     }
 
 
@@ -276,59 +277,59 @@ public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
     /**
      * Create a new enumeration sort.
      **/
-    public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
+    public <R> EnumSort<R> mkEnumSort(Symbol name, Symbol... enumNames)
 
     {
         checkContextMatch(name);
         checkContextMatch(enumNames);
-        return new EnumSort(this, name, enumNames);
+        return new EnumSort<>(this, name, enumNames);
     }
 
     /**
      * Create a new enumeration sort.
      **/
-    public EnumSort mkEnumSort(String name, String... enumNames)
+    public <R> EnumSort<R> mkEnumSort(String name, String... enumNames)
 
     {
-        return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
+        return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames));
     }
 
     /**
      * Create a new list sort.
      **/
-    public ListSort mkListSort(Symbol name, Sort elemSort)
+    public <R extends Sort> ListSort<R> mkListSort(Symbol name, R elemSort)
     {
         checkContextMatch(name);
         checkContextMatch(elemSort);
-        return new ListSort(this, name, elemSort);
+        return new ListSort<>(this, name, elemSort);
     }
 
     /**
      * Create a new list sort.
      **/
-    public ListSort mkListSort(String name, Sort elemSort)
+    public <R extends Sort> ListSort<R> mkListSort(String name, R elemSort)
     {
         checkContextMatch(elemSort);
-        return new ListSort(this, mkSymbol(name), elemSort);
+        return new ListSort<>(this, mkSymbol(name), elemSort);
     }
 
     /**
      * Create a new finite domain sort.
      **/
-    public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
+    public <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name, long size)
 
     {
         checkContextMatch(name);
-        return new FiniteDomainSort(this, name, size);
+        return new FiniteDomainSort<>(this, name, size);
     }
 
     /**
      * Create a new finite domain sort.
      **/
-    public FiniteDomainSort mkFiniteDomainSort(String name, long size)
+    public <R> FiniteDomainSort<R> mkFiniteDomainSort(String name, long size)
 
     {
-        return new FiniteDomainSort(this, mkSymbol(name), size);
+        return new FiniteDomainSort<>(this, mkSymbol(name), size);
     }
 
     /**
@@ -342,43 +343,40 @@ public FiniteDomainSort mkFiniteDomainSort(String name, long size)
      * an index referring to one of the recursive datatypes that is
      * declared.
      **/
-    public Constructor mkConstructor(Symbol name, Symbol recognizer,
+    public <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer,
             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
 
     {
-        return of(this, name, recognizer, fieldNames, sorts,
-                sortRefs);
+        return of(this, name, recognizer, fieldNames, sorts, sortRefs);
     }
 
     /**
      * Create a datatype constructor. 
      **/
-    public Constructor mkConstructor(String name, String recognizer,
+    public <R> Constructor<R> mkConstructor(String name, String recognizer,
             String[] fieldNames, Sort[] sorts, int[] sortRefs)
     {
-        return of(this, mkSymbol(name), mkSymbol(recognizer),
-                mkSymbols(fieldNames), sorts, sortRefs);
+        return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
     }
 
     /**
      * Create a new datatype sort.
      **/
-    public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
-
+    public <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
     {
         checkContextMatch(name);
         checkContextMatch(constructors);
-        return new DatatypeSort(this, name, constructors);
+        return new DatatypeSort<>(this, name, constructors);
     }
 
     /**
      * Create a new datatype sort.
      **/
-    public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
+    public <R> DatatypeSort<R> mkDatatypeSort(String name, Constructor<R>[] constructors)
 
     {
         checkContextMatch(constructors);
-        return new DatatypeSort(this, mkSymbol(name), constructors);
+        return new DatatypeSort<>(this, mkSymbol(name), constructors);
     }
 
     /**
@@ -386,34 +384,33 @@ public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
      * @param names names of datatype sorts 
      * @param c list of constructors, one list per sort.
      **/
-    public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
-
+    public DatatypeSort<Object>[] mkDatatypeSorts(Symbol[] names, Constructor<Object>[][] c)
     {
         checkContextMatch(names);
         int n = names.length;
-        ConstructorList[] cla = new ConstructorList[n];
+        ConstructorList<Object>[] cla = new ConstructorList[n];
         long[] n_constr = new long[n];
         for (int i = 0; i < n; i++)
         {
-            Constructor[] constructor = c[i];
+            Constructor<Object>[] constructor = c[i];
 
             checkContextMatch(constructor);
-            cla[i] = new ConstructorList(this, constructor);
+            cla[i] = new ConstructorList<>(this, constructor);
             n_constr[i] = cla[i].getNativeObject();
         }
         long[] n_res = new long[n];
         Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
                 n_constr);
-        DatatypeSort[] res = new DatatypeSort[n];
+        DatatypeSort<Object>[] res = new DatatypeSort[n];
         for (int i = 0; i < n; i++)
-            res[i] = new DatatypeSort(this, n_res[i]);
+            res[i] = new DatatypeSort<>(this, n_res[i]);
         return res;
     }
 
     /**
      * Create mutually recursive data-types. 
      **/
-    public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
+    public DatatypeSort<Object>[] mkDatatypeSorts(String[] names, Constructor<Object>[][] c)
 
     {
         return mkDatatypeSorts(mkSymbols(names), c);
@@ -425,10 +422,10 @@ public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
      * that is passed in as argument is updated with value v,
      * the remaining fields of t are unchanged.
      **/
-    public Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
+    public <F extends Sort, R extends Sort> Expr<R> mkUpdateField(FuncDecl<F> field, Expr<R> t, Expr<F> v)
         throws Z3Exception
     {
-        return Expr.create (this,
+        return (Expr<R>) Expr.create(this,
                             Native.datatypeUpdateField
                             (nCtx(), field.getNativeObject(),
                              t.getNativeObject(), v.getNativeObject()));
@@ -438,59 +435,59 @@ public Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
     /**
      * Creates a new function declaration.
      **/
-    public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort[] domain, R range)
     {
         checkContextMatch(name);
         checkContextMatch(domain);
         checkContextMatch(range);
-        return new FuncDecl(this, name, domain, range);
+        return new FuncDecl<>(this, name, domain, range);
     }
 
     /**
      * Creates a new function declaration.
      **/
-    public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort domain, R range)
 
     {
         checkContextMatch(name);
         checkContextMatch(domain);
         checkContextMatch(range);
         Sort[] q = new Sort[] { domain };
-        return new FuncDecl(this, name, q, range);
+        return new FuncDecl<>(this, name, q, range);
     }
 
     /**
      * Creates a new function declaration.
      **/
-    public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort[] domain, R range)
 
     {
         checkContextMatch(domain);
         checkContextMatch(range);
-        return new FuncDecl(this, mkSymbol(name), domain, range);
+        return new FuncDecl<>(this, mkSymbol(name), domain, range);
     }
 
     /**
      * Creates a new function declaration.
      **/
-    public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort domain, R range)
 
     {
         checkContextMatch(domain);
         checkContextMatch(range);
         Sort[] q = new Sort[] { domain };
-        return new FuncDecl(this, mkSymbol(name), q, range);
+        return new FuncDecl<>(this, mkSymbol(name), q, range);
     }
 
     /**
      * Creates a new recursive function declaration.
      **/
-    public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R range)
     {
         checkContextMatch(name);
         checkContextMatch(domain);
         checkContextMatch(range);
-        return new FuncDecl(this, name, domain, range, true);
+        return new FuncDecl<>(this, name, domain, range, true);
     }
 
 
@@ -500,14 +497,14 @@ public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, Sort range)
      * MkRecFuncDecl. The body may contain recursive uses of the function or
      * other mutually recursive functions. 
      */
-    public void AddRecDef(FuncDecl f, Expr[] args, Expr body) 
+    public <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> body)
     {
 	checkContextMatch(f);
 	checkContextMatch(args);
 	checkContextMatch(body);
 	long[] argsNative = AST.arrayToNative(args);
 	Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
-    }	
+    }
 
     /**
      * Creates a fresh function declaration with a name prefixed with
@@ -515,31 +512,31 @@ public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
      * @see #mkFuncDecl(String,Sort,Sort)
      * @see #mkFuncDecl(String,Sort[],Sort)
      **/
-    public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFreshFuncDecl(String prefix, Sort[] domain, R range)
 
     {
         checkContextMatch(domain);
         checkContextMatch(range);
-        return new FuncDecl(this, prefix, domain, range);
+        return new FuncDecl<>(this, prefix, domain, range);
     }
 
     /**
      * Creates a new constant function declaration.
      **/
-    public FuncDecl mkConstDecl(Symbol name, Sort range)
+    public <R extends Sort> FuncDecl<R> mkConstDecl(Symbol name, R range)
     {
         checkContextMatch(name);
         checkContextMatch(range);
-        return new FuncDecl(this, name, null, range);
+        return new FuncDecl<>(this, name, null, range);
     }
 
     /**
      * Creates a new constant function declaration.
      **/
-    public FuncDecl mkConstDecl(String name, Sort range)
+    public <R extends Sort> FuncDecl<R> mkConstDecl(String name, R range)
     {
         checkContextMatch(range);
-        return new FuncDecl(this, mkSymbol(name), null, range);
+        return new FuncDecl<>(this, mkSymbol(name), null, range);
     }
 
     /**
@@ -548,11 +545,11 @@ public FuncDecl mkConstDecl(String name, Sort range)
      * @see #mkFuncDecl(String,Sort,Sort)
      * @see #mkFuncDecl(String,Sort[],Sort)
      **/
-    public FuncDecl mkFreshConstDecl(String prefix, Sort range)
+    public <R extends Sort> FuncDecl<R> mkFreshConstDecl(String prefix, R range)
 
     {
         checkContextMatch(range);
-        return new FuncDecl(this, prefix, null, range);
+        return new FuncDecl<>(this, prefix, null, range);
     }
 
     /**
@@ -560,16 +557,16 @@ public FuncDecl mkFreshConstDecl(String prefix, Sort range)
      * @param index The de-Bruijn index of the variable 
      * @param ty The sort of the variable
      **/
-    public Expr mkBound(int index, Sort ty)
+    public <R extends Sort> Expr<R> mkBound(int index, R ty)
     {
-        return Expr.create(this,
+        return (Expr<R>) Expr.create(this,
                 Native.mkBound(nCtx(), index, ty.getNativeObject()));
     }
 
     /**
      * Create a quantifier pattern.
      **/
-    public Pattern mkPattern(Expr... terms)
+    public Pattern mkPattern(Expr<?>... terms)
     {
         if (terms.length == 0)
             throw new Z3Exception("Cannot create a pattern from zero terms");
@@ -583,12 +580,12 @@ public Pattern mkPattern(Expr... terms)
      * Creates a new Constant of sort {@code range} and named
      * {@code name}.
      **/
-    public Expr mkConst(Symbol name, Sort range)
+    public <R extends Sort> Expr<R> mkConst(Symbol name, R range)
     {
         checkContextMatch(name);
         checkContextMatch(range);
 
-        return Expr.create(
+        return (Expr<R>) Expr.create(
                 this,
                 Native.mkConst(nCtx(), name.getNativeObject(),
                         range.getNativeObject()));
@@ -598,7 +595,7 @@ public Expr mkConst(Symbol name, Sort range)
      * Creates a new Constant of sort {@code range} and named
      * {@code name}.
      **/
-    public Expr mkConst(String name, Sort range)
+    public <R extends Sort> Expr<R> mkConst(String name, R range)
     {
         return mkConst(mkSymbol(name), range);
     }
@@ -607,10 +604,10 @@ public Expr mkConst(String name, Sort range)
      * Creates a fresh Constant of sort {@code range} and a name
      * prefixed with {@code prefix}.
      **/
-    public Expr mkFreshConst(String prefix, Sort range)
+    public <R extends Sort> Expr<R> mkFreshConst(String prefix, R range)
     {
         checkContextMatch(range);
-        return Expr.create(this,
+        return (Expr<R>) Expr.create(this,
                 Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
     }
 
@@ -618,9 +615,9 @@ public Expr mkFreshConst(String prefix, Sort range)
      * Creates a fresh constant from the FuncDecl {@code f}. 
      * @param f A decl of a 0-arity function
      **/
-    public Expr mkConst(FuncDecl f)
+    public <R extends Sort> Expr<R> mkConst(FuncDecl<R> f)
     {
-        return mkApp(f, (Expr[]) null);
+        return mkApp(f, (Expr<?>[]) null);
     }
 
     /**
@@ -690,7 +687,7 @@ public BitVecExpr mkBVConst(String name, int size)
     /**
      * Create a new function application.
      **/
-    public Expr mkApp(FuncDecl f, Expr... args)
+    public <R extends Sort> Expr<R> mkApp(FuncDecl<R> f, Expr<?>... args)
     {
         checkContextMatch(f);
         checkContextMatch(args);
@@ -724,7 +721,7 @@ public BoolExpr mkBool(boolean value)
     /**
      * Creates the equality {@code x = y}
      **/
-    public BoolExpr mkEq(Expr x, Expr y)
+    public <R extends Sort> BoolExpr mkEq(Expr<R> x, Expr<R> y)
     {
         checkContextMatch(x);
         checkContextMatch(y);
@@ -735,7 +732,7 @@ public BoolExpr mkEq(Expr x, Expr y)
     /**
      * Creates a {@code distinct} term.
      **/
-    public BoolExpr mkDistinct(Expr... args)
+    public <R extends Sort> BoolExpr mkDistinct(Expr<R>... args)
     {
         checkContextMatch(args);
         return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
@@ -745,7 +742,7 @@ public BoolExpr mkDistinct(Expr... args)
     /**
      * Create an expression representing {@code not(a)}.
      **/
-    public BoolExpr mkNot(BoolExpr a)
+    public BoolExpr mkNot(Expr<BoolSort> a)
     {
         checkContextMatch(a);
         return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
@@ -758,19 +755,19 @@ public BoolExpr mkNot(BoolExpr a)
      * @param t2 An expression  
      * @param t3 An expression with the same sort as {@code t2}
      **/
-    public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
+    public <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<R> t2, Expr<R> t3)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
         checkContextMatch(t3);
-        return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
+        return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                 t2.getNativeObject(), t3.getNativeObject()));
     }
 
     /**
      * Create an expression representing {@code t1 iff t2}.
      **/
-    public BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
+    public BoolExpr mkIff(Expr<BoolSort> t1, Expr<BoolSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -781,7 +778,7 @@ public BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
     /**
      * Create an expression representing {@code t1 -> t2}.
      **/
-    public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
+    public BoolExpr mkImplies(Expr<BoolSort> t1, Expr<BoolSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -792,7 +789,7 @@ public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
     /**
      * Create an expression representing {@code t1 xor t2}.
      **/
-    public BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
+    public BoolExpr mkXor(Expr<BoolSort> t1, Expr<BoolSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -803,7 +800,7 @@ public BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
     /**
      * Create an expression representing {@code t[0] and t[1] and ...}.
      **/
-    public BoolExpr mkAnd(BoolExpr... t)
+    public BoolExpr mkAnd(Expr<BoolSort>... t)
     {
         checkContextMatch(t);
         return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
@@ -813,7 +810,7 @@ public BoolExpr mkAnd(BoolExpr... t)
     /**
      * Create an expression representing {@code t[0] or t[1] or ...}.
      **/
-    public BoolExpr mkOr(BoolExpr... t)
+    public BoolExpr mkOr(Expr<BoolSort>... t)
     {
         checkContextMatch(t);
         return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
@@ -823,51 +820,51 @@ public BoolExpr mkOr(BoolExpr... t)
     /**
      * Create an expression representing {@code t[0] + t[1] + ...}.
      **/
-    public ArithExpr mkAdd(ArithExpr... t)
+    public <R extends ArithSort> ArithExpr<R> mkAdd(Expr<R>... t)
     {
         checkContextMatch(t);
-        return (ArithExpr) Expr.create(this,
+        return (ArithExpr<R>) Expr.create(this,
                 Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create an expression representing {@code t[0] * t[1] * ...}.
      **/
-    public ArithExpr mkMul(ArithExpr... t)
+    public <R extends ArithSort> ArithExpr<R> mkMul(Expr<R>... t)
     {
         checkContextMatch(t);
-        return (ArithExpr) Expr.create(this,
+        return (ArithExpr<R>) Expr.create(this,
                 Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create an expression representing {@code t[0] - t[1] - ...}.
      **/
-    public ArithExpr mkSub(ArithExpr... t)
+    public <R extends ArithSort> ArithExpr<R> mkSub(Expr<R>... t)
     {
         checkContextMatch(t);
-        return (ArithExpr) Expr.create(this,
+        return (ArithExpr<R>) Expr.create(this,
                 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create an expression representing {@code -t}.
      **/
-    public ArithExpr mkUnaryMinus(ArithExpr t)
+    public <R extends ArithSort> ArithExpr<R> mkUnaryMinus(Expr<R> t)
     {
         checkContextMatch(t);
-        return (ArithExpr) Expr.create(this,
+        return (ArithExpr<R>) Expr.create(this,
                 Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
     }
 
     /**
      * Create an expression representing {@code t1 / t2}.
      **/
-    public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
-        return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
+        return (ArithExpr<R>) Expr.create(this, Native.mkDiv(nCtx(),
                 t1.getNativeObject(), t2.getNativeObject()));
     }
 
@@ -876,7 +873,7 @@ public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
      * Remarks: The
      * arguments must have int type.
      **/
-    public IntExpr mkMod(IntExpr t1, IntExpr t2)
+    public IntExpr mkMod(Expr<IntSort> t1, Expr<IntSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -889,7 +886,7 @@ public IntExpr mkMod(IntExpr t1, IntExpr t2)
      * Remarks: The
      * arguments must have int type.
      **/
-    public IntExpr mkRem(IntExpr t1, IntExpr t2)
+    public IntExpr mkRem(Expr<IntSort> t1, Expr<IntSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -900,11 +897,11 @@ public IntExpr mkRem(IntExpr t1, IntExpr t2)
     /**
      * Create an expression representing {@code t1 ^ t2}.
      **/
-    public ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> ArithExpr<R> mkPower(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
-        return (ArithExpr) Expr.create(
+        return (ArithExpr<R>) Expr.create(
                 this,
                 Native.mkPower(nCtx(), t1.getNativeObject(),
                         t2.getNativeObject()));
@@ -913,7 +910,7 @@ public ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
     /**
      * Create an expression representing {@code t1 &lt; t2}
      **/
-    public BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> BoolExpr mkLt(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -924,7 +921,7 @@ public BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
     /**
      * Create an expression representing {@code t1 &lt;= t2}
      **/
-    public BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> BoolExpr mkLe(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -935,7 +932,7 @@ public BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
     /**
      * Create an expression representing {@code t1 &gt; t2}
      **/
-    public BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> BoolExpr mkGt(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -946,7 +943,7 @@ public BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
     /**
      * Create an expression representing {@code t1 &gt;= t2}
      **/
-    public BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
+    public <R extends ArithSort> BoolExpr mkGe(Expr<R> t1, Expr<R> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -964,7 +961,7 @@ public BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
      * {@code MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1}. The argument
      * must be of integer sort. 
      **/
-    public RealExpr mkInt2Real(IntExpr t)
+    public RealExpr mkInt2Real(Expr<IntSort> t)
     {
         checkContextMatch(t);
         return new RealExpr(this,
@@ -977,7 +974,7 @@ public RealExpr mkInt2Real(IntExpr t)
      * follows the SMT-LIB standard for the function to_int. The argument must
      * be of real sort. 
      **/
-    public IntExpr mkReal2Int(RealExpr t)
+    public IntExpr mkReal2Int(Expr<RealSort> t)
     {
         checkContextMatch(t);
         return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
@@ -986,7 +983,7 @@ public IntExpr mkReal2Int(RealExpr t)
     /**
      * Creates an expression that checks whether a real number is an integer.
      **/
-    public BoolExpr mkIsInteger(RealExpr t)
+    public BoolExpr mkIsInteger(Expr<RealSort> t)
     {
         checkContextMatch(t);
         return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
@@ -997,7 +994,7 @@ public BoolExpr mkIsInteger(RealExpr t)
      * Remarks: The argument must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVNot(BitVecExpr t)
+    public BitVecExpr mkBVNot(Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
@@ -1008,7 +1005,7 @@ public BitVecExpr mkBVNot(BitVecExpr t)
      *
      * Remarks: The argument must have a bit-vector sort.
      **/
-    public BitVecExpr mkBVRedAND(BitVecExpr t)
+    public BitVecExpr mkBVRedAND(Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkBvredand(nCtx(),
@@ -1020,7 +1017,7 @@ public BitVecExpr mkBVRedAND(BitVecExpr t)
      *
      * Remarks: The argument must have a bit-vector sort.
      **/
-    public BitVecExpr mkBVRedOR(BitVecExpr t)
+    public BitVecExpr mkBVRedOR(Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkBvredor(nCtx(),
@@ -1032,7 +1029,7 @@ public BitVecExpr mkBVRedOR(BitVecExpr t)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1045,7 +1042,7 @@ public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1058,7 +1055,7 @@ public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVXOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1071,7 +1068,7 @@ public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVNAND(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1084,7 +1081,7 @@ public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1097,7 +1094,7 @@ public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a bit-vector
      * sort.
      **/
-    public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVXNOR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1110,7 +1107,7 @@ public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have a
      * bit-vector sort.
      **/
-    public BitVecExpr mkBVNeg(BitVecExpr t)
+    public BitVecExpr mkBVNeg(Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
@@ -1121,7 +1118,7 @@ public BitVecExpr mkBVNeg(BitVecExpr t)
      * Remarks: The arguments must have the same
      * bit-vector sort.
      **/
-    public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVAdd(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1134,7 +1131,7 @@ public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have the same
      * bit-vector sort.
      **/
-    public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVSub(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1147,7 +1144,7 @@ public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
      * Remarks: The arguments must have the
      * same bit-vector sort.
      **/
-    public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVMul(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1162,7 +1159,7 @@ public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
      * zero, then the result is undefined. The arguments must have the same
      * bit-vector sort. 
      **/
-    public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVUDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1183,7 +1180,7 @@ public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
      * If {@code t2} is zero, then the result is undefined. The arguments
      * must have the same bit-vector sort. 
      **/
-    public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVSDiv(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1198,7 +1195,7 @@ public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
      * unsigned division. If {@code t2} is zero, then the result is
      * undefined. The arguments must have the same bit-vector sort. 
      **/
-    public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVURem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1216,7 +1213,7 @@ public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
      * If {@code t2} is zero, then the result is undefined. The arguments
      * must have the same bit-vector sort. 
      **/
-    public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVSRem(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1230,7 +1227,7 @@ public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
      * {@code t2} is zero, then the result is undefined. The arguments must
      * have the same bit-vector sort. 
      **/
-    public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVSMod(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1243,7 +1240,7 @@ public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have the same bit-vector
      * sort. 
      **/
-    public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVULT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1256,7 +1253,7 @@ public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
-    public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSLT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1269,7 +1266,7 @@ public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
-    public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVULE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1282,7 +1279,7 @@ public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments
      * must have the same bit-vector sort. 
      **/
-    public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSLE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1295,7 +1292,7 @@ public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have the
      * same bit-vector sort. 
      **/
-    public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVUGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1308,7 +1305,7 @@ public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments
      * must have the same bit-vector sort. 
      **/
-    public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSGE(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1321,7 +1318,7 @@ public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have the same
      * bit-vector sort. 
      **/
-    public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVUGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1334,7 +1331,7 @@ public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
      * Remarks:  The arguments must have
      * the same bit-vector sort. 
      **/
-    public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSGT(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1352,7 +1349,7 @@ public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
      *         ({@code t2}).
      *
      **/
-    public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkConcat(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1368,7 +1365,7 @@ public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
      * {@code n = high - low + 1}. The argument {@code t} must
      * have a bit-vector sort. 
      **/
-    public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
+    public BitVecExpr mkExtract(int high, int low, Expr<BitVecSort> t)
 
     {
         checkContextMatch(t);
@@ -1383,7 +1380,7 @@ public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
      * the size of the given bit-vector. The argument {@code t} must
      * have a bit-vector sort. 
      **/
-    public BitVecExpr mkSignExt(int i, BitVecExpr t)
+    public BitVecExpr mkSignExt(int i, Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
@@ -1397,7 +1394,7 @@ public BitVecExpr mkSignExt(int i, BitVecExpr t)
      * where \c m is the size of the given bit-vector. The argument {@code t}
      * must have a bit-vector sort. 
      **/
-    public BitVecExpr mkZeroExt(int i, BitVecExpr t)
+    public BitVecExpr mkZeroExt(int i, Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
@@ -1409,7 +1406,7 @@ public BitVecExpr mkZeroExt(int i, BitVecExpr t)
      * Remarks:  The argument {@code t} must
      * have a bit-vector sort. 
      **/
-    public BitVecExpr mkRepeat(int i, BitVecExpr t)
+    public BitVecExpr mkRepeat(int i, Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
@@ -1427,7 +1424,7 @@ public BitVecExpr mkRepeat(int i, BitVecExpr t)
      *
      * The arguments must have a bit-vector sort. 
      **/
-    public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVSHL(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1446,7 +1443,7 @@ public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
      *
      * The arguments must have a bit-vector sort. 
      **/
-    public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVLSHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1466,7 +1463,7 @@ public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
      *
      * The arguments must have a bit-vector sort. 
      **/
-    public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVASHR(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
     {
         checkContextMatch(t1);
         checkContextMatch(t2);
@@ -1479,7 +1476,7 @@ public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
      * 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)
+    public BitVecExpr mkBVRotateLeft(int i, Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
@@ -1491,7 +1488,7 @@ public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
      * 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)
+    public BitVecExpr mkBVRotateRight(int i, Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
@@ -1504,7 +1501,7 @@ public BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
      * {@code t2} times. The arguments must have the same bit-vector
      * sort. 
      **/
-    public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVRotateLeft(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1519,7 +1516,7 @@ public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
      * right{@code t2} times. The arguments must have the same
      * bit-vector sort. 
      **/
-    public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
+    public BitVecExpr mkBVRotateRight(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1537,7 +1534,7 @@ public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
      *
      * The argument must be of integer sort. 
      **/
-    public BitVecExpr mkInt2BV(int n, IntExpr t)
+    public BitVecExpr mkInt2BV(int n, Expr<IntSort> t)
     {
         checkContextMatch(t);
         return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
@@ -1558,7 +1555,7 @@ public BitVecExpr mkInt2BV(int n, IntExpr t)
      *
      * The argument must be of bit-vector sort. 
      **/
-    public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
+    public IntExpr mkBV2Int(Expr<BitVecSort> t, boolean signed)
     {
         checkContextMatch(t);
         return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
@@ -1570,7 +1567,7 @@ public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
      * overflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2,
+    public BoolExpr mkBVAddNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
             boolean isSigned)
     {
         checkContextMatch(t1);
@@ -1584,7 +1581,7 @@ public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2,
      * underflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVAddNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1598,7 +1595,7 @@ public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
      * overflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSubNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1612,7 +1609,7 @@ public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
      * underflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2,
+    public BoolExpr mkBVSubNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
             boolean isSigned)
     {
         checkContextMatch(t1);
@@ -1626,7 +1623,7 @@ public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2,
      * overflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVSDivNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1640,7 +1637,7 @@ public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
      * overflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVNegNoOverflow(BitVecExpr t)
+    public BoolExpr mkBVNegNoOverflow(Expr<BitVecSort> t)
     {
         checkContextMatch(t);
         return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
@@ -1652,7 +1649,7 @@ public BoolExpr mkBVNegNoOverflow(BitVecExpr t)
      * overflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2,
+    public BoolExpr mkBVMulNoOverflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2,
             boolean isSigned)
     {
         checkContextMatch(t1);
@@ -1666,7 +1663,7 @@ public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2,
      * underflow. 
      * Remarks:  The arguments must be of bit-vector sort. 
      **/
-    public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
+    public BoolExpr mkBVMulNoUnderflow(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
 
     {
         checkContextMatch(t1);
@@ -1678,19 +1675,19 @@ public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
     /**
      * Create an array constant.
      **/
-    public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
+    public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(Symbol name, D domain, R range)
 
     {
-        return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
+        return (ArrayExpr<D, R>) mkConst(name, mkArraySort(domain, range));
     }
 
     /**
      * Create an array constant.
      **/
-    public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
+    public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(String name, D domain, R range)
 
     {
-        return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
+        return (ArrayExpr<D, R>) mkConst(mkSymbol(name), mkArraySort(domain, range));
     }
 
     /**
@@ -1706,11 +1703,11 @@ public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
      * @see #mkStore
 
      **/
-    public Expr mkSelect(ArrayExpr a, Expr i)
+    public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
     {
         checkContextMatch(a);
         checkContextMatch(i);
-        return Expr.create(
+        return (Expr<R>) Expr.create(
                 this,
                 Native.mkSelect(nCtx(), a.getNativeObject(),
                         i.getNativeObject()));
@@ -1727,13 +1724,12 @@ public Expr mkSelect(ArrayExpr a, Expr i)
      *
      * @see #mkArraySort
      * @see #mkStore
-
      **/
-    public Expr mkSelect(ArrayExpr a, Expr[] args)
+    public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<?, R>> a, Expr<?>[] args)
     {
         checkContextMatch(a);
         checkContextMatch(args);
-        return Expr.create(
+        return (Expr<R>) Expr.create(
                 this,
                 Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
     }
@@ -1754,12 +1750,12 @@ public Expr mkSelect(ArrayExpr a, Expr[] args)
      * @see #mkSelect
 
      **/
-    public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
+    public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
     {
         checkContextMatch(a);
         checkContextMatch(i);
         checkContextMatch(v);
-        return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
+        return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(),
                 i.getNativeObject(), v.getNativeObject()));
     }
 
@@ -1779,12 +1775,12 @@ public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
      * @see #mkSelect
 
      **/
-    public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
+    public <R extends Sort> ArrayExpr<?, R> mkStore(Expr<ArraySort<?, R>> a, Expr<?>[] args, Expr<R> v)
     {
         checkContextMatch(a);
         checkContextMatch(args);
         checkContextMatch(v);
-        return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
+        return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
                              args.length, AST.arrayToNative(args), v.getNativeObject()));
     }
 
@@ -1797,11 +1793,11 @@ public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
      * @see #mkSelect
      *
      **/
-    public ArrayExpr mkConstArray(Sort domain, Expr v)
+    public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, Expr<R> v)
     {
         checkContextMatch(domain);
         checkContextMatch(v);
-        return new ArrayExpr(this, Native.mkConstArray(nCtx(),
+        return new ArrayExpr<>(this, Native.mkConstArray(nCtx(),
                 domain.getNativeObject(), v.getNativeObject()));
     }
 
@@ -1818,11 +1814,11 @@ public ArrayExpr mkConstArray(Sort domain, Expr v)
      * @see #mkStore
 
      **/
-    public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
+    public <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)
     {
         checkContextMatch(f);
         checkContextMatch(args);
-        return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
+        return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
                 f.getNativeObject(), AST.arrayLength(args),
                 AST.arrayToNative(args)));
     }
@@ -1833,61 +1829,61 @@ public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
      * value, for arrays that can be represented as finite maps with a default
      * range value. 
      **/
-    public Expr mkTermArray(ArrayExpr array)
+    public <D extends Sort, R extends Sort> Expr<R> mkTermArray(Expr<ArraySort<D, R>> array)
     {
         checkContextMatch(array);
-        return Expr.create(this,
+        return (Expr<R>) Expr.create(this,
                 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
     }
 
     /**
      * Create Extentionality index. Two arrays are equal if and only if they are equal on the index returned by MkArrayExt.
      **/
-    public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
+    public <D extends Sort, R extends Sort> Expr<D> mkArrayExt(Expr<ArraySort<D, R>> arg1, Expr<ArraySort<D, R>> arg2)
     {
     checkContextMatch(arg1);
     checkContextMatch(arg2);
-    return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
+    return (Expr<D>) Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
     }
 
 
     /**
      * Create a set type.
      **/
-    public SetSort mkSetSort(Sort ty)
+    public <D extends Sort> SetSort<D> mkSetSort(D ty)
     {
         checkContextMatch(ty);
-        return new SetSort(this, ty);
+        return new SetSort<>(this, ty);
     }
 
     /**
      * Create an empty set.
      **/
-    public ArrayExpr mkEmptySet(Sort domain)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkEmptySet(D domain)
     {
         checkContextMatch(domain);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
     }
 
     /**
      * Create the full set.
      **/
-    public ArrayExpr mkFullSet(Sort domain)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkFullSet(D domain)
     {
         checkContextMatch(domain);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                 Native.mkFullSet(nCtx(), domain.getNativeObject()));
     }
 
     /**
      * Add an element to the set.
      **/
-    public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetAdd(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
     {
         checkContextMatch(set);
         checkContextMatch(element);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                 Native.mkSetAdd(nCtx(), set.getNativeObject(),
                         element.getNativeObject()));
     }
@@ -1895,11 +1891,11 @@ public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
     /**
      * Remove an element from a set.
      **/
-    public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetDel(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
     {
         checkContextMatch(set);
         checkContextMatch(element);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                 Native.mkSetDel(nCtx(), set.getNativeObject(),
                         element.getNativeObject()));
     }
@@ -1907,10 +1903,10 @@ public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
     /**
      * Take the union of a list of sets.
      **/
-    public ArrayExpr mkSetUnion(ArrayExpr... args)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetUnion(Expr<ArraySort<D, BoolSort>>... args)
     {
         checkContextMatch(args);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                 Native.mkSetUnion(nCtx(), args.length,
                         AST.arrayToNative(args)));
     }
@@ -1918,10 +1914,10 @@ public ArrayExpr mkSetUnion(ArrayExpr... args)
     /**
      * Take the intersection of a list of sets.
      **/
-    public ArrayExpr mkSetIntersection(ArrayExpr... args)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetIntersection(Expr<ArraySort<D, BoolSort>>... args)
     {
         checkContextMatch(args);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                 Native.mkSetIntersect(nCtx(), args.length,
                         AST.arrayToNative(args)));
     }
@@ -1929,11 +1925,11 @@ public ArrayExpr mkSetIntersection(ArrayExpr... args)
     /**
      * Take the difference between two sets.
      **/
-    public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetDifference(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
     {
         checkContextMatch(arg1);
         checkContextMatch(arg2);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>) Expr.create(this,
                 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                         arg2.getNativeObject()));
     }
@@ -1941,17 +1937,17 @@ public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
     /**
      * Take the complement of a set.
      **/
-    public ArrayExpr mkSetComplement(ArrayExpr arg)
+    public <D extends Sort> ArrayExpr<D, BoolSort> mkSetComplement(Expr<ArraySort<D, BoolSort>> arg)
     {
         checkContextMatch(arg);
-        return (ArrayExpr)Expr.create(this,
+        return (ArrayExpr<D, BoolSort>)Expr.create(this,
                 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
     }
 
     /**
      * Check for set membership.
      **/
-    public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
+    public <D extends Sort> BoolExpr mkSetMembership(Expr<D> elem, Expr<ArraySort<D, BoolSort>> set)
     {
         checkContextMatch(elem);
         checkContextMatch(set);
@@ -1963,7 +1959,7 @@ public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
     /**
      * Check for subsetness of sets.
      **/
-    public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
+    public <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
     {
         checkContextMatch(arg1);
         checkContextMatch(arg2);
@@ -1980,41 +1976,41 @@ public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
     /**
      * Create the empty sequence.
     */
-    public SeqExpr mkEmptySeq(Sort s)
+    public <R extends Sort> SeqExpr<R> mkEmptySeq(R s)
     {
         checkContextMatch(s);
-        return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
     }
 
     /**
      * Create the singleton sequence.
      */
-    public SeqExpr mkUnit(Expr elem)
+    public <R extends Sort> SeqExpr<R> mkUnit(Expr<R> elem)
     {
         checkContextMatch(elem);
-        return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
     }
 
     /**
      * Create a string constant.
      */
-    public SeqExpr mkString(String s)
+    public SeqExpr<BitVecSort> mkString(String s)
     {
-        return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
+        return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkString(nCtx(), s));
     }
 
     /**
      * Convert an integer expression to a string.
      */
-    public SeqExpr intToString(Expr e)
+    public SeqExpr<BitVecSort> intToString(Expr<IntSort> e)
     {
-	return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
+	return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
     }
 
     /**
      * Convert an integer expression to a string.
      */
-    public IntExpr stringToInt(Expr e)
+    public IntExpr stringToInt(Expr<SeqSort<BitVecSort>> e)
     {
 	return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
     }
@@ -2022,17 +2018,17 @@ public IntExpr stringToInt(Expr e)
     /**
      * Concatenate sequences.
      */
-    public SeqExpr mkConcat(SeqExpr... t)
+    public <R extends Sort> SeqExpr<R> mkConcat(SeqSort<R>... t)
     {
         checkContextMatch(t);
-        return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
 
     /**
      * Retrieve the length of a given sequence.
      */
-    public IntExpr mkLength(SeqExpr s)
+    public <R extends Sort> IntExpr mkLength(Expr<SeqSort<BitVecSort>> s)
     {
         checkContextMatch(s);
         return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
@@ -2041,7 +2037,7 @@ public IntExpr mkLength(SeqExpr s)
     /**
      * Check for sequence prefix.
      */
-    public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
+    public <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
     {
         checkContextMatch(s1, s2);
         return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2050,7 +2046,7 @@ public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
     /**
      * Check for sequence suffix.
      */
-    public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
+    public <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
     {
         checkContextMatch(s1, s2);
         return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2059,7 +2055,7 @@ public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
     /**
      * Check for sequence containment of s2 in s1.
      */
-    public BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
+    public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
     {
         checkContextMatch(s1, s2);
         return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
@@ -2068,35 +2064,35 @@ public BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
     /**
      * Retrieve sequence of length one at index.
      */
-    public SeqExpr mkAt(SeqExpr s, IntExpr index)
+    public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
     {
         checkContextMatch(s, index);
-        return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
     }
 
     /**
      *  Retrieve element at index.
      */
-    public Expr MkNth(SeqExpr s, Expr index)
+    public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
     {
         checkContextMatch(s, index);
-        return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
+        return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
     }
 
 
     /**
      * Extract subsequence.
      */
-    public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
+    public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> offset, Expr<IntSort> length)
     {
         checkContextMatch(s, offset, length);
-        return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
     }
 
     /**
      * Extract index of sub-string starting at offset.
      */
-    public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
+    public <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> substr, Expr<IntSort> offset)
     {
         checkContextMatch(s, substr, offset);
         return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
@@ -2105,26 +2101,26 @@ public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
     /**
      * Replace the first occurrence of src by dst in s.
      */
-    public SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
+    public <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> src, Expr<SeqSort<BitVecSort>> dst)
     {
         checkContextMatch(s, src, dst);
-        return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
+        return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
     }
 
     /**
      * Convert a regular expression that accepts sequence s.
      */
-    public ReExpr mkToRe(SeqExpr s)
+    public <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<BitVecSort>> s)
     {
         checkContextMatch(s);
-        return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
     }
 
 
     /**
      * Check for regular expression membership.
      */
-    public BoolExpr mkInRe(SeqExpr s, ReExpr re)
+    public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<BitVecSort>> s, Expr<ReSort<R>> re)
     {
         checkContextMatch(s, re);
         return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
@@ -2133,114 +2129,113 @@ public BoolExpr mkInRe(SeqExpr s, ReExpr re)
     /**
      * Take the Kleene star of a regular expression.
      */
-    public ReExpr mkStar(ReExpr re)
+    public <R extends Sort> ReExpr<R> mkStar(Expr<ReSort<R>> re)
     {
         checkContextMatch(re);
-        return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
     }
 
     /**
      * Take the lower and upper-bounded Kleene star of a regular expression.
      */
-    public ReExpr mkLoop(ReExpr re, int lo, int hi)
+    public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo, int hi)
     {
-        return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
+        return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
     }
 
     /**
      * Take the lower-bounded Kleene star of a regular expression.
      */
-    public ReExpr mkLoop(ReExpr re, int lo)
+    public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo)
     {
-        return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
+        return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
     }
 
 
     /**
      * Take the Kleene plus of a regular expression.
      */
-    public ReExpr mkPlus(ReExpr re)
+    public <R extends Sort> ReExpr<R> mkPlus(Expr<ReSort<R>> re)
     {
         checkContextMatch(re);
-        return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
     }
 
     /**
      * Create the optional regular expression.
      */
-    public ReExpr mkOption(ReExpr re)
+    public <R extends Sort> ReExpr<R> mkOption(Expr<ReSort<R>> re)
     {
         checkContextMatch(re);
-        return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
     }
 
-
     /**
      * Create the complement regular expression.
      */
-    public ReExpr mkComplement(ReExpr re)
+    public <R extends Sort> ReExpr<R> mkComplement(Expr<ReSort<R>> re)
     {
         checkContextMatch(re);
-        return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
     }
 
     /**
      * Create the concatenation of regular languages.
      */
-    public ReExpr mkConcat(ReExpr... t)
+    public <R extends Sort> ReExpr<R> mkConcat(ReExpr<R>... t)
     {
         checkContextMatch(t);
-        return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
+        return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create the union of regular languages.
      */
-    public ReExpr mkUnion(ReExpr... t)
+    public <R extends Sort> ReExpr<R> mkUnion(Expr<ReSort<R>>... t)
     {
         checkContextMatch(t);
-        return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
+        return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create the intersection of regular languages.
      */
-    public ReExpr mkIntersect(ReExpr... t)
+    public <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
     {
         checkContextMatch(t);
-        return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
+        return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
     }
 
     /**
      * Create the empty regular expression.
      */
-    public ReExpr mkEmptyRe(Sort s)
+    public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
     {
-	return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
+	return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
     }
 
     /**
      * Create the full regular expression.
      */
-    public ReExpr mkFullRe(Sort s)
+    public <R extends Sort> ReExpr<R> mkFullRe(R s)
     {
-	return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
+	return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
     }
 
     /**
      * Create a range expression.
      */
-    public ReExpr mkRange(SeqExpr lo, SeqExpr hi)
+    public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<BitVecSort>> lo, Expr<SeqSort<BitVecSort>> hi)
     {
         checkContextMatch(lo, hi);
-        return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
+        return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
     }
 
 
     /**
      * Create an at-most-k constraint.
      */
-    public BoolExpr mkAtMost(BoolExpr[] args, int k)
+    public BoolExpr mkAtMost(Expr<BoolSort>[] args, int k)
     {
         checkContextMatch(args);
         return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
@@ -2249,7 +2244,7 @@ public BoolExpr mkAtMost(BoolExpr[] args, int k)
     /**
      * Create an at-least-k constraint.
      */
-    public BoolExpr mkAtLeast(BoolExpr[] args, int k)
+    public BoolExpr mkAtLeast(Expr<BoolSort>[] args, int k)
     {
         checkContextMatch(args);
         return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
@@ -2258,7 +2253,7 @@ public BoolExpr mkAtLeast(BoolExpr[] args, int k)
     /**
      * Create a pseudo-Boolean less-or-equal constraint.
      */
-    public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
+    public BoolExpr mkPBLe(int[] coeffs, Expr<BoolSort>[] args, int k)
     {
         checkContextMatch(args);
         return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
@@ -2267,7 +2262,7 @@ public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
     /**
      * Create a pseudo-Boolean greater-or-equal constraint.
      */
-    public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
+    public BoolExpr mkPBGe(int[] coeffs, Expr<BoolSort>[] args, int k)
     {
         checkContextMatch(args);
         return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
@@ -2276,13 +2271,12 @@ public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
     /**
      * Create a pseudo-Boolean equal constraint.
      */
-    public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
+    public BoolExpr mkPBEq(int[] coeffs, Expr<BoolSort>[] args, int k)
     {
         checkContextMatch(args);
         return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
     }
 
-
     /**
      * 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
@@ -2294,10 +2288,10 @@ public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
      *
      * @return A Term with value {@code v} and sort {@code ty}
      **/
-    public Expr mkNumeral(String v, Sort ty)
+    public <R extends Sort> Expr<R> mkNumeral(String v, R ty)
     {
         checkContextMatch(ty);
-        return Expr.create(this,
+        return (Expr<R>) Expr.create(this,
                 Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
     }
 
@@ -2311,10 +2305,10 @@ public Expr mkNumeral(String v, Sort ty)
      *
      * @return A Term with value {@code v} and type {@code ty}
      **/
-    public Expr mkNumeral(int v, Sort ty)
+    public <R extends Sort> Expr<R> mkNumeral(int v, R ty)
     {
         checkContextMatch(ty);
-        return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
+        return (Expr<R>) Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
     }
 
     /**
@@ -2327,10 +2321,10 @@ public Expr mkNumeral(int v, Sort ty)
      *
      * @return A Term with value {@code v} and type {@code ty}
      **/
-    public Expr mkNumeral(long v, Sort ty)
+    public <R extends Sort> Expr<R> mkNumeral(long v, R ty)
     {
         checkContextMatch(ty);
-        return Expr.create(this,
+        return (Expr<R>) Expr.create(this,
                 Native.mkInt64(nCtx(), v, ty.getNativeObject()));
     }
 
@@ -2483,11 +2477,10 @@ public BitVecNum mkBV(long v, int size)
      * of {@code names} and {@code sorts} refers to the variable 
      * with index 1, etc. 
      **/
-    public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
-                               int weight, Pattern[] patterns, Expr[] noPatterns,
+    public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr<BoolSort> body,
+                               int weight, Pattern[] patterns, Expr<?>[] noPatterns,
                                Symbol quantifierID, Symbol skolemID)
     {
-
         return Quantifier.of(this, true, sorts, names, body, weight, patterns,
                 noPatterns, quantifierID, skolemID);
     }
@@ -2496,8 +2489,8 @@ public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
      * Creates a universal quantifier using a list of constants that will form the set of bound variables. 
      * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
-    public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
-                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+    public Quantifier mkForall(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
+                               Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
                                Symbol skolemID)
     {
 
@@ -2509,8 +2502,8 @@ public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
      * Creates an existential quantifier using de-Bruijn indexed variables.
      * @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,
+    public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr<BoolSort> body,
+                               int weight, Pattern[] patterns, Expr<?>[] noPatterns,
                                Symbol quantifierID, Symbol skolemID)
     {
 
@@ -2522,8 +2515,8 @@ public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
      * Creates an existential quantifier using a list of constants that will form the set of bound variables. 
      * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
-    public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
-                               Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
+    public Quantifier mkExists(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
+                               Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
                                Symbol skolemID)
     {
 
@@ -2536,8 +2529,8 @@ public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
      * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
     public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
-                                   Symbol[] names, Expr body, int weight, Pattern[] patterns,
-                                   Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
+                                   Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns,
+                                   Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
 
     {
 
@@ -2553,8 +2546,8 @@ public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
      * Create a Quantifier
      * @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
      **/
-    public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
-                                   Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
+    public Quantifier mkQuantifier(boolean universal, Expr<?>[] boundConstants,
+                                   Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
                                    Symbol quantifierID, Symbol skolemID)
     {
 
@@ -2583,7 +2576,7 @@ public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
      * @param names names of the bound variables.
      * @param body the body of the quantifier.
      **/
-     public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
+     public <R extends Sort> Lambda<R> mkLambda(Sort[] sorts, Symbol[] names, Expr<R> body)
      {
          return Lambda.of(this, sorts, names, body);
      }
@@ -2594,7 +2587,7 @@ public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
      * Creates a lambda expression using a list of constants that will
      * form the set of bound variables.
      **/
-     public Lambda mkLambda(Expr[] boundConstants, Expr body)
+     public <R extends Sort> Lambda<R> mkLambda(Expr<?>[] boundConstants, Expr<R> body)
      {
          return Lambda.of(this, boundConstants, body);
      }
@@ -2633,8 +2626,8 @@ public void setPrintMode(Z3_ast_print_mode value)
      * @return A string representation of the benchmark.
      **/
     public String benchmarkToSMTString(String name, String logic,
-            String status, String attributes, BoolExpr[] assumptions,
-            BoolExpr formula)
+            String status, String attributes, Expr<BoolSort>[] assumptions,
+                                       Expr<BoolSort> formula)
     {
 
         return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
@@ -2652,8 +2645,7 @@ public String benchmarkToSMTString(String name, String logic,
      * last scope level.
      **/
     public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
-            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
-
+            Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
     {
         int csn = Symbol.arrayLength(sortNames);
         int cs = Sort.arrayLength(sorts);
@@ -2674,8 +2666,7 @@ public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
      * @see #parseSMTLIB2String
      **/
     public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
-            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
-
+            Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
     {
         int csn = Symbol.arrayLength(sortNames);
         int cs = Sort.arrayLength(sorts);
@@ -2702,7 +2693,6 @@ public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
      * enabled.
      **/
     public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
-
     {
         return new Goal(this, models, unsatCores, proofs);
     }
@@ -3505,7 +3495,7 @@ public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPAbs(FPExpr t)
+    public FPExpr mkFPAbs(Expr<FPSort> t)
     {
         return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
     }
@@ -3515,7 +3505,7 @@ public FPExpr mkFPAbs(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPNeg(FPExpr t)
+    public FPExpr mkFPNeg(Expr<FPSort> t)
     {
         return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
     }
@@ -3527,7 +3517,7 @@ public FPExpr mkFPNeg(FPExpr t)
      * @param t2 floating-point term     
      * @throws Z3Exception
      **/
-    public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
+    public FPExpr mkFPAdd(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3539,7 +3529,7 @@ public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
+    public FPExpr mkFPSub(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3551,7 +3541,7 @@ public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
+    public FPExpr mkFPMul(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3563,7 +3553,7 @@ public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
+    public FPExpr mkFPDiv(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3578,7 +3568,7 @@ public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
      * The result is round((t1 * t2) + t3)
      * @throws Z3Exception
      **/
-    public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
+    public FPExpr mkFPFMA(Expr<FPRMSort> rm, Expr<FPSort> t1, Expr<FPSort> t2, Expr<FPSort> t3)
     {
         return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
     }
@@ -3589,7 +3579,7 @@ public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
+    public FPExpr mkFPSqrt(Expr<FPRMSort> rm, Expr<FPSort> t)
     {
         return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
     }
@@ -3600,7 +3590,7 @@ public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
+    public FPExpr mkFPRem(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3612,7 +3602,7 @@ public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
+    public FPExpr mkFPRoundToIntegral(Expr<FPRMSort> rm, Expr<FPSort> t)
     {
         return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
     }
@@ -3623,7 +3613,7 @@ public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
+    public FPExpr mkFPMin(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3634,7 +3624,7 @@ public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
+    public FPExpr mkFPMax(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3645,7 +3635,7 @@ public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
+    public BoolExpr mkFPLEq(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3656,7 +3646,7 @@ public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
+    public BoolExpr mkFPLt(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3667,7 +3657,7 @@ public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
+    public BoolExpr mkFPGEq(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3678,7 +3668,7 @@ public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
      * @param t2 floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
+    public BoolExpr mkFPGt(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3691,7 +3681,7 @@ public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
      * Note that this is IEEE 754 equality (as opposed to standard =).
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
+    public BoolExpr mkFPEq(Expr<FPSort> t1, Expr<FPSort> t2)
     {
         return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
     }
@@ -3701,7 +3691,7 @@ public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsNormal(FPExpr t)
+    public BoolExpr mkFPIsNormal(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
     }
@@ -3711,7 +3701,7 @@ public BoolExpr mkFPIsNormal(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsSubnormal(FPExpr t)
+    public BoolExpr mkFPIsSubnormal(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
     }
@@ -3721,7 +3711,7 @@ public BoolExpr mkFPIsSubnormal(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsZero(FPExpr t)
+    public BoolExpr mkFPIsZero(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
     }
@@ -3731,7 +3721,7 @@ public BoolExpr mkFPIsZero(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsInfinite(FPExpr t)
+    public BoolExpr mkFPIsInfinite(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
     }
@@ -3741,7 +3731,7 @@ public BoolExpr mkFPIsInfinite(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsNaN(FPExpr t)
+    public BoolExpr mkFPIsNaN(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
     }
@@ -3751,7 +3741,7 @@ public BoolExpr mkFPIsNaN(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsNegative(FPExpr t)
+    public BoolExpr mkFPIsNegative(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
     }
@@ -3761,7 +3751,7 @@ public BoolExpr mkFPIsNegative(FPExpr t)
      * @param t floating-point term
      * @throws Z3Exception
      **/
-    public BoolExpr mkFPIsPositive(FPExpr t)
+    public BoolExpr mkFPIsPositive(Expr<FPSort> t)
     {
         return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
     }
@@ -3779,7 +3769,7 @@ public BoolExpr mkFPIsPositive(FPExpr t)
      * of the arguments.
      * @throws Z3Exception
      **/
-    public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
+    public FPExpr mkFP(Expr<BitVecSort> sgn, Expr<BitVecSort> sig, Expr<BitVecSort> exp)
     {
         return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
     }
@@ -3795,7 +3785,7 @@ public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
      * IEEE 754-2008 interchange format.
      * @throws Z3Exception
      **/
-    public FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
+    public FPExpr mkFPToFP(Expr<BitVecSort> bv, FPSort s)
     {
         return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
     }
@@ -3811,7 +3801,7 @@ public FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
      * to rounding mode rm.
      * @throws Z3Exception
      **/
-    public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
+    public FPExpr mkFPToFP(Expr<FPRMSort> rm, FPExpr t, FPSort s)
     {
         return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
     }
@@ -3827,7 +3817,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
      * to rounding mode rm.
      * @throws Z3Exception
      **/
-    public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
+    public FPExpr mkFPToFP(Expr<FPRMSort> rm, RealExpr t, FPSort s)
     {
         return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
     }
@@ -3845,7 +3835,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
      * result will be rounded according to rounding mode rm.
      * @throws Z3Exception
      **/
-    public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
+    public FPExpr mkFPToFP(Expr<FPRMSort> rm, Expr<BitVecSort> t, FPSort s, boolean signed)
     {
         if (signed)
             return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
@@ -3863,7 +3853,7 @@ public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
      * FloatingPoint sort s. If necessary, rounding according to rm is applied. 
      * @throws Z3Exception
      **/
-    public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
+    public FPExpr mkFPToFP(FPSort s, Expr<FPRMSort> rm, Expr<FPSort> t)
     {
         return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
     }
@@ -3880,7 +3870,7 @@ public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
      * the result will be rounded according to rounding mode rm.        
      * @throws Z3Exception
      **/
-    public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
+    public BitVecExpr mkFPToBV(Expr<FPRMSort> rm, Expr<FPSort> t, int sz, boolean signed)
     {
         if (signed)
             return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
@@ -3897,7 +3887,7 @@ public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
      * constraints over real terms.
      * @throws Z3Exception
      **/
-    public RealExpr mkFPToReal(FPExpr t)
+    public RealExpr mkFPToReal(Expr<FPSort> t)
     {
         return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
     }
@@ -3912,7 +3902,7 @@ public RealExpr mkFPToReal(FPExpr t)
      * that NaN. 
      * @throws Z3Exception
      **/
-    public BitVecExpr mkFPToIEEEBV(FPExpr t)
+    public BitVecExpr mkFPToIEEEBV(Expr<FPSort> t)
     {
         return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
     }
@@ -3930,7 +3920,7 @@ public BitVecExpr mkFPToIEEEBV(FPExpr t)
      * @throws Z3Exception
      **/
 
-    public BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
+    public BitVecExpr mkFPToFP(Expr<FPRMSort> rm, Expr<IntSort> exp, Expr<RealSort> sig, FPSort s)
     {
         return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
     }
@@ -4053,11 +4043,11 @@ void checkContextMatch(Z3Object[] arr)
     private ConstructorListDecRefQueue m_ConstructorList_DRQ =
             new ConstructorListDecRefQueue();
 
-    public IDecRefQueue<Constructor> getConstructorDRQ() {
+    public IDecRefQueue<Constructor<?>> getConstructorDRQ() {
         return m_Constructor_DRQ;
     }
 
-    public IDecRefQueue<ConstructorList> getConstructorListDRQ() {
+    public IDecRefQueue<ConstructorList<?>> getConstructorListDRQ() {
         return m_ConstructorList_DRQ;
     }
 
@@ -4081,12 +4071,12 @@ public IDecRefQueue<ApplyResult> getApplyResultDRQ()
         return m_ApplyResult_DRQ;
     }
 
-    public IDecRefQueue<FuncInterp.Entry> getFuncEntryDRQ()
+    public IDecRefQueue<FuncInterp.Entry<?>> getFuncEntryDRQ()
     {
         return m_FuncEntry_DRQ;
     }
 
-    public IDecRefQueue<FuncInterp> getFuncInterpDRQ()
+    public IDecRefQueue<FuncInterp<?>> getFuncInterpDRQ()
     {
         return m_FuncInterp_DRQ;
     }
diff --git a/src/api/java/DatatypeExpr.java b/src/api/java/DatatypeExpr.java
index 9abe230f6ae..7db3bf0834b 100644
--- a/src/api/java/DatatypeExpr.java
+++ b/src/api/java/DatatypeExpr.java
@@ -20,7 +20,7 @@
 /**
  * Datatype expressions
  **/
-public class DatatypeExpr extends Expr
+public class DatatypeExpr<R extends Sort> extends Expr<DatatypeSort<R>>
 {
     /**
      * Constructor for DatatypeExpr
diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java
index 644d434d32c..8d7f53c2460 100644
--- a/src/api/java/DatatypeSort.java
+++ b/src/api/java/DatatypeSort.java
@@ -20,7 +20,7 @@
 /**
  * Datatype sorts.
  **/
-public class DatatypeSort extends Sort
+public class DatatypeSort<R> extends Sort
 {
     /**
      * The number of constructors of the datatype sort.
@@ -39,12 +39,13 @@ public int getNumConstructors()
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getConstructors()
+    @SuppressWarnings("unchecked")
+    public FuncDecl<DatatypeSort<R>>[] getConstructors()
     {
         int n = getNumConstructors();
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<DatatypeSort<R>>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
+            res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
                     getContext().nCtx(), getNativeObject(), i));
         return res;
     }
@@ -55,12 +56,13 @@ public FuncDecl[] getConstructors()
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getRecognizers()
+    @SuppressWarnings("unchecked")
+    public FuncDecl<BoolSort>[] getRecognizers()
     {
         int n = getNumConstructors();
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<BoolSort>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
+            res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(
                     getContext().nCtx(), getNativeObject(), i));
         return res;
     }
@@ -71,20 +73,20 @@ public FuncDecl[] getRecognizers()
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[][] getAccessors()
+    public FuncDecl<?>[][] getAccessors()
     {
 
         int n = getNumConstructors();
-        FuncDecl[][] res = new FuncDecl[n][];
+        FuncDecl<?>[][] res = new FuncDecl[n][];
         for (int i = 0; i < n; i++)
         {
-            FuncDecl fd = new FuncDecl(getContext(),
+            FuncDecl<?> fd = new FuncDecl<>(getContext(),
                     Native.getDatatypeSortConstructor(getContext().nCtx(),
                             getNativeObject(), i));
             int ds = fd.getDomainSize();
-            FuncDecl[] tmp = new FuncDecl[ds];
+            FuncDecl<?>[] tmp = new FuncDecl[ds];
             for (int j = 0; j < ds; j++)
-                tmp[j] = new FuncDecl(getContext(),
+                tmp[j] = new FuncDecl<>(getContext(),
                         Native.getDatatypeSortConstructorAccessor(getContext()
                                 .nCtx(), getNativeObject(), i, j));
             res[i] = tmp;
@@ -97,7 +99,7 @@ public FuncDecl[][] getAccessors()
         super(ctx, obj);
     }
 
-    DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
+    DatatypeSort(Context ctx, Symbol name, Constructor<R>[] constructors)
            
     {
         super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java
index e0bd0f617be..5cd11ba08bd 100644
--- a/src/api/java/EnumSort.java
+++ b/src/api/java/EnumSort.java
@@ -20,28 +20,29 @@
 /**
  * Enumeration sorts.
  **/
-public class EnumSort extends Sort
+@SuppressWarnings("unchecked")
+public class EnumSort<R> extends Sort
 {
     /**
      * The function declarations of the constants in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getConstDecls()
+    public FuncDecl<EnumSort<R>>[] getConstDecls()
     {
         int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
-        FuncDecl[] t = new FuncDecl[n];
+        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;
+            t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
+        return (FuncDecl<EnumSort<R>>[]) t;
     }
     
     /**
      * Retrieves the inx'th constant declaration in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl getConstDecl(int inx)
+    public FuncDecl<EnumSort<R>> getConstDecl(int inx)
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
     }
 
     /**
@@ -49,13 +50,13 @@ public FuncDecl getConstDecl(int inx)
      * @throws Z3Exception on error
      * @return an Expr[]
      **/
-    public Expr[] getConsts()
+    public Expr<EnumSort<R>>[] getConsts()
     {        
-        FuncDecl[] cds = getConstDecls();
-        Expr[] t = new Expr[cds.length];
+        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;
+        return (Expr<EnumSort<R>>[]) t;
     }
     
     /**
@@ -63,7 +64,7 @@ public Expr[] getConsts()
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr getConst(int inx)
+    public Expr<EnumSort<R>> getConst(int inx)
     {        
         return getContext().mkApp(getConstDecl(inx));
     }
@@ -72,12 +73,13 @@ public Expr getConst(int inx)
      * The test predicates for the constants in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getTesterDecls()
+    @SuppressWarnings("unchecked")
+    public FuncDecl<BoolSort>[] getTesterDecls()
     {
         int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
-        FuncDecl[] t = new FuncDecl[n];
+        FuncDecl<BoolSort>[] t = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
+            t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
         return t;
     }
     
@@ -85,9 +87,9 @@ public FuncDecl[] getTesterDecls()
      * Retrieves the inx'th tester/recognizer declaration in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl getTesterDecl(int inx)
+    public FuncDecl<BoolSort> getTesterDecl(int inx)
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
     }
 
     EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index d1d554b54f1..f2f64efee2b 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -27,14 +27,15 @@
 /**
  * Expressions are terms.
  **/
-public class Expr extends AST
+@SuppressWarnings("unchecked")
+public class Expr<R extends Sort> extends AST
 {
     /**
      * Returns a simplified version of the expression
      * @return Expr
      * @throws Z3Exception on error
      **/
-    public Expr simplify()
+    public Expr<R> simplify()
     {
         return simplify(null);
     }
@@ -48,15 +49,15 @@ public Expr simplify()
      * @return an Expr
      * @throws Z3Exception on error
      **/
-    public Expr simplify(Params p)
+    public Expr<R> simplify(Params p)
     {
 
         if (p == null) {
-            return Expr.create(getContext(),
+            return (Expr<R>) Expr.create(getContext(),
                 Native.simplify(getContext().nCtx(), getNativeObject()));
         }
         else {
-            return Expr.create(
+            return (Expr<R>) Expr.create(
                 getContext(),
                 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
                     p.getNativeObject()));
@@ -69,9 +70,9 @@ public Expr simplify(Params p)
      * @return a FuncDecl
      * @throws Z3Exception on error 
      **/
-    public FuncDecl getFuncDecl()
+    public FuncDecl<R> getFuncDecl()
     {
-        return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
+        return new FuncDecl<>(getContext(), Native.getAppDecl(getContext().nCtx(),
                 getNativeObject()));
     }
 
@@ -102,10 +103,10 @@ public int getNumArgs()
      * @throws Z3Exception on error
      * @return an Expr[]
      **/
-    public Expr[] getArgs()
+    public Expr<?>[] getArgs()
     {
         int n = getNumArgs();
-        Expr[] res = new Expr[n];
+        Expr<?>[] res = new Expr[n];
         for (int i = 0; i < n; i++) {
             res[i] = Expr.create(getContext(),
                 Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
@@ -120,13 +121,13 @@ public Expr[] getArgs()
      * @param args arguments
      * @throws Z3Exception on error
      **/
-    public Expr update(Expr[] args)
+    public Expr<R> update(Expr<?>[] args)
     {
         getContext().checkContextMatch(args);
         if (isApp() && args.length != getNumArgs()) {
             throw new Z3Exception("Number of arguments does not match");
         }
-        return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
+        return (Expr<R>) Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
                 args.length, Expr.arrayToNative(args)));
     }
 
@@ -142,14 +143,14 @@ public Expr update(Expr[] args)
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr substitute(Expr[] from, Expr[] to)
+    public Expr<R> substitute(Expr<?>[] from, Expr<?>[] to)
     {
         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(),
+        return (Expr<R>) Expr.create(getContext(), Native.substitute(getContext().nCtx(),
                 getNativeObject(), from.length, Expr.arrayToNative(from),
                 Expr.arrayToNative(to)));
     }
@@ -161,7 +162,7 @@ public Expr substitute(Expr[] from, Expr[] to)
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr substitute(Expr from, Expr to)
+    public Expr<R> substitute(Expr<?> from, Expr<?> to)
     {
         return substitute(new Expr[] { from }, new Expr[] { to });
     }
@@ -176,11 +177,11 @@ public Expr substitute(Expr from, Expr to)
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr substituteVars(Expr[] to)
+    public Expr<R> substituteVars(Expr<?>[] to)
     {
 
         getContext().checkContextMatch(to);
-        return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
+        return (Expr<R>) Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
                 getNativeObject(), to.length, Expr.arrayToNative(to)));
     }
 
@@ -192,9 +193,9 @@ public Expr substituteVars(Expr[] to)
      * @return A copy of the term which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
-    public Expr translate(Context ctx)
+    public Expr<R> translate(Context ctx)
     {
-        return (Expr) super.translate(ctx);
+        return (Expr<R>) super.translate(ctx);
     }
 
     /**
@@ -232,9 +233,9 @@ public boolean isWellSorted()
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getSort()
+    public R getSort()
     {
-        return Sort.create(getContext(),
+        return (R) Sort.create(getContext(),
                 Native.getSort(getContext().nCtx(), getNativeObject()));
     }
 
@@ -1635,7 +1636,7 @@ public boolean isProofLemma()
 
     /**
      * 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') 
+     * Remarks:  T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... R(n+1): (not l_n) * [unit-resolution T1 ... R(n+1)]: (or l_1' ... l_m')
      * @throws Z3Exception on error
      * @return a boolean
      **/
@@ -1770,8 +1771,8 @@ public boolean isProofIFFOEQ()
      * 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))
+     * eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x R) q)
+     * (forall (x R) q_new))
      * 
      * (b) When recursively creating NNF over Boolean formulas, where the
      * top-level connective is changed during NNF conversion. The relevant
@@ -2107,15 +2108,15 @@ void checkNativeObject(long obj) {
         super.checkNativeObject(obj);
     }
 
-    static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
-           
+    static <U extends Sort> Expr<U> create(Context ctx, FuncDecl<U> f, Expr<?> ... arguments)
     {
         long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
                 AST.arrayLength(arguments), AST.arrayToNative(arguments));
-        return create(ctx, obj);
+        return (Expr<U>) create(ctx, obj);
     }
 
-    static Expr create(Context ctx, long obj)
+    // TODO generify, but it conflicts with AST.create
+    static Expr<?> create(Context ctx, long obj)
     {
         Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
         if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
@@ -2143,7 +2144,7 @@ static Expr create(Context ctx, long obj)
                 return new FPRMNum(ctx, obj);
             case Z3_FINITE_DOMAIN_SORT:
                 return new FiniteDomainNum(ctx, obj);
-            default: ;
+            default:
             }
         }
 
@@ -2158,9 +2159,9 @@ static Expr create(Context ctx, long obj)
         case Z3_BV_SORT:
             return new BitVecExpr(ctx, obj);
         case Z3_ARRAY_SORT:
-            return new ArrayExpr(ctx, obj);
+            return new ArrayExpr<>(ctx, obj);
         case Z3_DATATYPE_SORT:
-            return new DatatypeExpr(ctx, obj);
+            return new DatatypeExpr<>(ctx, obj);
         case Z3_FLOATING_POINT_SORT:
             return new FPExpr(ctx, obj);
         case Z3_ROUNDING_MODE_SORT:
@@ -2168,12 +2169,12 @@ static Expr create(Context ctx, long obj)
         case Z3_FINITE_DOMAIN_SORT:
             return new FiniteDomainExpr(ctx, obj);
         case Z3_SEQ_SORT:
-            return new SeqExpr(ctx, obj);
+            return new SeqExpr<>(ctx, obj);
         case Z3_RE_SORT:
-            return new ReExpr(ctx, obj);
-        default: ;
+            return new ReExpr<>(ctx, obj);
+        default:
         }
 
-        return new Expr(ctx, obj);
+        return new Expr<>(ctx, obj);
     }
 }
diff --git a/src/api/java/FPExpr.java b/src/api/java/FPExpr.java
index 8218f0f79a7..c348e642045 100644
--- a/src/api/java/FPExpr.java
+++ b/src/api/java/FPExpr.java
@@ -19,7 +19,7 @@ Christoph Wintersteiger (cwinter) 2013-06-10
 /**
  * FloatingPoint Expressions
  */
-public class FPExpr extends Expr
+public class FPExpr extends Expr<FPSort>
 {   
     /**
      * The number of exponent bits.
diff --git a/src/api/java/FPRMExpr.java b/src/api/java/FPRMExpr.java
index 08db43b8aae..fd88c9a0ea7 100644
--- a/src/api/java/FPRMExpr.java
+++ b/src/api/java/FPRMExpr.java
@@ -19,7 +19,7 @@ Christoph Wintersteiger (cwinter) 2013-06-10
 /**
  * FloatingPoint RoundingMode Expressions
  */
-public class FPRMExpr extends Expr
+public class FPRMExpr extends Expr<FPRMSort>
 {       
     public FPRMExpr(Context ctx, long obj)
     {
diff --git a/src/api/java/FiniteDomainExpr.java b/src/api/java/FiniteDomainExpr.java
index f7d9307583b..b3da5cf9dbe 100644
--- a/src/api/java/FiniteDomainExpr.java
+++ b/src/api/java/FiniteDomainExpr.java
@@ -20,7 +20,7 @@
 /**
  * Finite-domain expressions
  **/
-public class FiniteDomainExpr extends Expr
+public class FiniteDomainExpr<R> extends Expr<FiniteDomainSort<R>>
 {
     /**
      * Constructor for FiniteDomainExpr
diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java
index 68467e408ad..fec44017db8 100644
--- a/src/api/java/FiniteDomainNum.java
+++ b/src/api/java/FiniteDomainNum.java
@@ -22,7 +22,7 @@
 /**
  * Finite-domain Numerals
  **/
-public class FiniteDomainNum extends FiniteDomainExpr
+public class FiniteDomainNum<R> extends FiniteDomainExpr<R>
 {
 
     FiniteDomainNum(Context ctx, long obj)
diff --git a/src/api/java/FiniteDomainSort.java b/src/api/java/FiniteDomainSort.java
index dcb52cd2211..ede57ac5493 100644
--- a/src/api/java/FiniteDomainSort.java
+++ b/src/api/java/FiniteDomainSort.java
@@ -20,7 +20,7 @@
 /**
  * Finite domain sorts.
  **/
-public class FiniteDomainSort extends Sort
+public class FiniteDomainSort<R> extends Sort
 {
     /**
      * The size of the finite domain sort.
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 8560b6292a2..96e1dd0cb21 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -62,10 +62,11 @@ public ParamDescrs getParameterDescriptions()
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr ... constraints)
+    @SafeVarargs
+    public final void add(Expr<BoolSort>... constraints)
     {
         getContext().checkContextMatch(constraints);
-        for (BoolExpr a : constraints)
+        for (Expr<BoolSort> a : constraints)
         {
             Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
                     a.getNativeObject());
@@ -77,9 +78,8 @@ public void add(BoolExpr ... constraints)
      * 
      * @throws Z3Exception
      **/
-    public void registerRelation(FuncDecl f)
+    public void registerRelation(FuncDecl<BoolSort> f)
     {
-
         getContext().checkContextMatch(f);
         Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
                 f.getNativeObject());
@@ -92,7 +92,7 @@ public void registerRelation(FuncDecl f)
      * @param name Nullable rule name.
      * @throws Z3Exception
      **/
-    public void addRule(BoolExpr rule, Symbol name) {
+    public void addRule(Expr<BoolSort> rule, Symbol name) {
         getContext().checkContextMatch(rule);
         Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                 rule.getNativeObject(), AST.getNativeObject(name));
@@ -103,7 +103,7 @@ public void addRule(BoolExpr rule, Symbol name) {
      * 
      * @throws Z3Exception
      **/
-    public void addFact(FuncDecl pred, int ... args) {
+    public void addFact(FuncDecl<BoolSort> pred, int ... args) {
         getContext().checkContextMatch(pred);
         Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                 pred.getNativeObject(), args.length, args);
@@ -118,7 +118,7 @@ public void addFact(FuncDecl pred, int ... args) {
      * 
      * @throws Z3Exception
      **/
-    public Status query(BoolExpr query) {
+    public Status query(Expr<BoolSort> query) {
         getContext().checkContextMatch(query);
         Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
                 getNativeObject(), query.getNativeObject()));
@@ -141,7 +141,7 @@ public Status query(BoolExpr query) {
      * 
      * @throws Z3Exception
      **/
-    public Status query(FuncDecl[] relations) {
+    public Status query(FuncDecl<BoolSort>[] relations) {
         getContext().checkContextMatch(relations);
         Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
                 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
@@ -164,7 +164,7 @@ public Status query(FuncDecl[] relations) {
      * @param name Nullable rule name.
      * @throws Z3Exception
      **/
-    public void updateRule(BoolExpr rule, Symbol name) {
+    public void updateRule(Expr<BoolSort> rule, Symbol name) {
         getContext().checkContextMatch(rule);
         Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
                 rule.getNativeObject(), AST.getNativeObject(name));
@@ -176,7 +176,7 @@ public void updateRule(BoolExpr rule, Symbol name) {
      * 
      * @throws Z3Exception
      **/
-    public Expr getAnswer()
+    public Expr<?> getAnswer()
     {
         long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
         return (ans == 0) ? null : Expr.create(getContext(), ans);
@@ -194,7 +194,7 @@ public String getReasonUnknown()
     /**
      * Retrieve the number of levels explored for a given predicate.
      **/
-    public int getNumLevels(FuncDecl predicate)
+    public int getNumLevels(FuncDecl<BoolSort> predicate)
     {
         return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                 predicate.getNativeObject());
@@ -205,7 +205,7 @@ public int getNumLevels(FuncDecl predicate)
      * 
      * @throws Z3Exception
      **/
-    public Expr getCoverDelta(int level, FuncDecl predicate)
+    public Expr<?> getCoverDelta(int level, FuncDecl<BoolSort> predicate)
     {
         long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
                 getNativeObject(), level, predicate.getNativeObject());
@@ -216,7 +216,7 @@ public Expr getCoverDelta(int level, FuncDecl predicate)
      * Add <tt>property</tt> about the <tt>predicate</tt>. The property is added
      * at <tt>level</tt>.
      **/
-    public void addCover(int level, FuncDecl predicate, Expr property)
+    public void addCover(int level, FuncDecl<BoolSort> predicate, Expr<?> property)
            
     {
         Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
@@ -237,9 +237,8 @@ public String toString()
      * Instrument the Datalog engine on which table representation to use for
      * recursive predicate.
      **/
-    public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
+    public void setPredicateRepresentation(FuncDecl<BoolSort> f, Symbol[] kinds)
     {
-
         Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
                 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
                 Symbol.arrayToNative(kinds));
@@ -249,9 +248,8 @@ public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
     /**
      * Convert benchmark given as set of axioms, rules and queries to a string.
      **/
-    public String toString(BoolExpr[] queries)
+    public String toString(Expr<BoolSort>[] queries)
     {
-
         return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                 AST.arrayLength(queries), AST.arrayToNative(queries));
     }
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 8a19427bf79..57517219962 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -24,7 +24,7 @@
 /**
  * Function declarations.
  **/
-public class FuncDecl extends AST
+public class FuncDecl<R extends Sort> extends AST
 {
     /**
      * Object comparison.
@@ -34,7 +34,7 @@ public boolean equals(Object o)
     {
         if (o == this) return true;
         if (!(o instanceof FuncDecl)) return false;
-        FuncDecl other = (FuncDecl) o;
+        FuncDecl<?> other = (FuncDecl<?>) o;
 
         return
             (getContext().nCtx() == other.getContext().nCtx()) &&
@@ -66,9 +66,10 @@ public int getId()
      * @return A copy of the function declaration which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
-    public FuncDecl translate(Context ctx)
+    @SuppressWarnings("unchecked")
+    public FuncDecl<R> translate(Context ctx)
     {
-        return (FuncDecl) super.translate(ctx);
+        return (FuncDecl<R>) super.translate(ctx);
     }
 
     /**
@@ -106,10 +107,10 @@ public Sort[] getDomain()
     /**
      * The range of the function declaration
      **/
-    public Sort getRange()
+    @SuppressWarnings("unchecked")
+    public R getRange()
     {
-
-        return Sort.create(getContext(),
+        return (R) Sort.create(getContext(),
                 Native.getRange(getContext().nCtx(), getNativeObject()));
     }
 
@@ -178,7 +179,7 @@ public Parameter[] getParameters()
                                 getNativeObject(), i)));
                 break;
             case Z3_PARAMETER_FUNC_DECL:
-                res[i] = new Parameter(k, new FuncDecl(getContext(),
+                res[i] = new Parameter(k, new FuncDecl<>(getContext(),
                         Native.getDeclFuncDeclParameter(getContext().nCtx(),
                                 getNativeObject(), i)));
                 break;
@@ -197,7 +198,7 @@ public Parameter[] getParameters()
     /**
      * Function declarations can have Parameters associated with them.
      **/
-    public class Parameter
+    public static class Parameter
     {
         private Z3_parameter_kind kind;
         private int i;
@@ -205,7 +206,7 @@ public class Parameter
         private Symbol sym;
         private Sort srt;
         private AST ast;
-        private FuncDecl fd;
+        private FuncDecl<?> fd;
         private String r;
 
         /**
@@ -261,7 +262,7 @@ public AST getAST()
         /**
          * The FunctionDeclaration value of the parameter.
          **/
-        public FuncDecl getFuncDecl()
+        public FuncDecl<?> getFuncDecl()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL)
                 throw new Z3Exception("parameter is not a function declaration");
@@ -316,7 +317,7 @@ public Z3_parameter_kind getParameterKind()
             this.ast = a;
         }
 
-        Parameter(Z3_parameter_kind k, FuncDecl fd)
+        Parameter(Z3_parameter_kind k, FuncDecl<?> fd)
         {
             this.kind = k;
             this.fd = fd;
@@ -335,14 +336,14 @@ public Z3_parameter_kind getParameterKind()
 
     }
 
-    FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
+    FuncDecl(Context ctx, Symbol name, Sort[] domain, R range)
     {
         super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
                 AST.arrayLength(domain), AST.arrayToNative(domain),
                 range.getNativeObject()));
     }
 
-    FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, boolean is_rec)
+    FuncDecl(Context ctx, Symbol name, Sort[] domain, R range, boolean is_rec)
     {
         super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(),
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -350,8 +351,7 @@ public Z3_parameter_kind getParameterKind()
 
     }
 
-    FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
-
+    FuncDecl(Context ctx, String prefix, Sort[] domain, R range)
     {
         super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -371,7 +371,7 @@ void checkNativeObject(long obj)
     /**
      * Create expression that applies function to arguments.
      **/
-    public Expr apply(Expr ... args)
+    public Expr<R> apply(Expr<?> ... args)
     {
         getContext().checkContextMatch(args);
         return Expr.create(getContext(), this, args);
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index b5873d98e9e..64f96534b05 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -22,13 +22,14 @@
  * Each entry in the finite map represents the value of a function given a set
  * of arguments.
  **/
-public class FuncInterp extends Z3Object {
+@SuppressWarnings("unchecked")
+public class FuncInterp<R extends Sort> extends Z3Object {
 
     /**
      * An Entry object represents an element in the finite map used to encode a
      * function interpretation.
      **/
-    public static class Entry extends Z3Object {
+    public static class Entry<R extends Sort> extends Z3Object {
 
         /**
          * Return the (symbolic) value of this entry.
@@ -36,9 +37,9 @@ public static class Entry extends Z3Object {
          * @throws Z3Exception
          * @throws Z3Exception on error
          **/
-        public Expr getValue()
+        public Expr<R> getValue()
         {
-            return Expr.create(getContext(),
+            return (Expr<R>) Expr.create(getContext(),
                     Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
         }
 
@@ -57,10 +58,10 @@ public int getNumArgs()
          * @throws Z3Exception
          * @throws Z3Exception on error
          **/
-        public Expr[] getArgs()
+        public Expr<?>[] getArgs()
         {
             int n = getNumArgs();
-            Expr[] res = new Expr[n];
+            Expr<?>[] res = new Expr[n];
             for (int i = 0; i < n; i++)
                 res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
                         getContext().nCtx(), getNativeObject(), i));
@@ -75,7 +76,7 @@ public String toString()
         {
             int n = getNumArgs();
             String res = "[";
-            Expr[] args = getArgs();
+            Expr<?>[] args = getArgs();
             for (int i = 0; i < n; i++)
                 res += args[i] + ", ";
             return res + getValue() + "]";
@@ -112,12 +113,12 @@ public int getNumEntries()
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public Entry[] getEntries()
+    public Entry<R>[] getEntries()
     {
         int n = getNumEntries();
-        Entry[] res = new Entry[n];
+        Entry<R>[] res = new Entry[n];
         for (int i = 0; i < n; i++)
-            res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
+            res[i] = new Entry<>(getContext(), Native.funcInterpGetEntry(getContext()
                     .nCtx(), getNativeObject(), i));
         return res;
     }
@@ -129,9 +130,9 @@ public Entry[] getEntries()
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr getElse()
+    public Expr<R> getElse()
     {
-        return Expr.create(getContext(),
+        return (Expr<R>) Expr.create(getContext(),
                 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
     }
 
@@ -152,12 +153,12 @@ public String toString()
     {
         String res = "";
         res += "[";
-        for (Entry e : getEntries())
+        for (Entry<R> e : getEntries())
         {
             int n = e.getNumArgs();
             if (n > 1)
                 res += "[";
-            Expr[] args = e.getArgs();
+            Expr<?>[] args = e.getArgs();
             for (int i = 0; i < n; i++)
             {
                 if (i != 0)
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index d8715bd0eb6..06a6f2af851 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp>
+class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp<?>>
 {
     public FuncInterpDecRefQueue() 
     {
diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java
index a4d8a069040..77bb78f5b6c 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -17,7 +17,7 @@
 
 package com.microsoft.z3;
 
-class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry> {
+class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry<?>> {
     public FuncInterpEntryDecRefQueue() 
     {
         super();
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index f5fa35fdb5a..3326f81fe02 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -76,10 +76,11 @@ public boolean isGarbage()
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr ... constraints)
+    @SafeVarargs
+    public final void add(Expr<BoolSort>... constraints)
     {
         getContext().checkContextMatch(constraints);
-        for (BoolExpr c : constraints)
+        for (Expr<BoolSort> c : constraints)
         {
             Native.goalAssert(getContext().nCtx(), getNativeObject(),
                     c.getNativeObject());
diff --git a/src/api/java/IntExpr.java b/src/api/java/IntExpr.java
index 56ba9ccdf52..77e41302034 100644
--- a/src/api/java/IntExpr.java
+++ b/src/api/java/IntExpr.java
@@ -20,7 +20,7 @@
 /**
  * Int expressions
  **/
-public class IntExpr extends ArithExpr
+public class IntExpr extends ArithExpr<IntSort>
 {
     /**
      * Constructor for IntExpr
diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java
index cf9809a239e..780e543c863 100644
--- a/src/api/java/Lambda.java
+++ b/src/api/java/Lambda.java
@@ -19,12 +19,11 @@ Christoph Wintersteiger (cwinter) 2012-03-19
 
 package com.microsoft.z3;
 
-import com.microsoft.z3.enumerations.Z3_ast_kind;
-
 
 /**
  * Lambda expressions.
-*/public class Lambda extends ArrayExpr
+*/
+public class Lambda<R extends Sort> extends ArrayExpr<Sort, R>
 {
 
     /**
@@ -70,9 +69,10 @@ public Sort[] getBoundVariableSorts()
      * 
      * @throws Z3Exception
      **/
-    public Expr getBody()
+    @SuppressWarnings("unchecked")
+    public Expr<R> getBody()
     {
-        return Expr.create(getContext(), Native.getQuantifierBody(getContext()
+        return (Expr<R>) Expr.create(getContext(), Native.getQuantifierBody(getContext()
                 .nCtx(), getNativeObject()));
     }
 
@@ -81,17 +81,17 @@ public Expr getBody()
      * Translates (copies) the quantifier to the Context {@code ctx}.
      * 
      * @param ctx A context
-     * 
+     *
      * @return A copy of the quantifier which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
-    public Lambda translate(Context ctx)
+    public Lambda<R> translate(Context ctx)
     {
-        return (Lambda) super.translate(ctx);
+        return (Lambda<R>) super.translate(ctx);
     }
     
        
-    public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body) 
+    public static <R extends Sort> Lambda<R> of(Context ctx, Sort[] sorts, Symbol[] names, Expr<R> body)
     {
         ctx.checkContextMatch(sorts);
         ctx.checkContextMatch(names);
@@ -106,7 +106,7 @@ public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
 					    Symbol.arrayToNative(names),
 					    body.getNativeObject());
 	
-        return new Lambda(ctx, nativeObject);
+        return new Lambda<>(ctx, nativeObject);
     }
 
     /**
@@ -115,14 +115,14 @@ public static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
      * @param body Body of the lambda expression.
      */
 
-    public static Lambda of(Context ctx, Expr[] bound, Expr body) {
+    public static <R extends Sort> Lambda<R> of(Context ctx, Expr<?>[] bound, Expr<R> body) {
         ctx.checkContextMatch(body);
 
               
        long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
 					   AST.arrayLength(bound), AST.arrayToNative(bound),
 					   body.getNativeObject());
-       return new Lambda(ctx, nativeObject);
+       return new Lambda<>(ctx, nativeObject);
    }
 
 
diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java
index 0ff2c36cf5e..8b7582791b9 100644
--- a/src/api/java/ListSort.java
+++ b/src/api/java/ListSort.java
@@ -22,22 +22,22 @@
 /**
  * List sorts.
  **/
-public class ListSort extends Sort
+public class ListSort<R extends Sort> extends Sort
 {
     /**
      * The declaration of the nil function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getNilDecl()
+    public FuncDecl<ListSort<R>> getNilDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
     }
 
     /**
      * The empty list.
      * @throws Z3Exception 
      **/
-    public Expr getNil()
+    public Expr<ListSort<R>> getNil()
     {
         return getContext().mkApp(getNilDecl());
     }
@@ -46,18 +46,18 @@ public Expr getNil()
      * The declaration of the isNil function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getIsNilDecl()
+    public FuncDecl<BoolSort> getIsNilDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
     }
 
     /**
      * The declaration of the cons function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getConsDecl()
+    public FuncDecl<ListSort<R>> getConsDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
     }
 
     /**
@@ -65,27 +65,27 @@ public FuncDecl getConsDecl()
      * @throws Z3Exception 
      * 
      **/
-    public FuncDecl getIsConsDecl()
+    public FuncDecl<BoolSort> getIsConsDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
     }
 
     /**
      * The declaration of the head function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getHeadDecl()
+    public FuncDecl<R> getHeadDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
     }
 
     /**
      * The declaration of the tail function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getTailDecl()
+    public FuncDecl<ListSort<R>> getTailDecl()
     {
-        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
+        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
     }
 
     ListSort(Context ctx, Symbol name, Sort elemSort)
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 4c9abef7a4b..032745fc5f7 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -22,17 +22,18 @@
 /**
  * A Model contains interpretations (assignments) of constants and functions.
  **/
+@SuppressWarnings("unchecked")
 public class Model extends Z3Object {
     /**
      * Retrieves the interpretation (the assignment) of {@code a} in
      * the model. 
      * @param a A Constant
-     * 
+     *
      * @return An expression if the constant has an interpretation in the model,
      *         null otherwise.
      * @throws Z3Exception
      **/
-    public Expr getConstInterp(Expr a)
+    public <R extends Sort> Expr<R> getConstInterp(Expr<R> a)
     {
         getContext().checkContextMatch(a);
         return getConstInterp(a.getFuncDecl());
@@ -47,7 +48,7 @@ public Expr getConstInterp(Expr a)
      *         null otherwise.
      * @throws Z3Exception
      **/
-    public Expr getConstInterp(FuncDecl f)
+    public <R extends Sort> Expr<R> getConstInterp(FuncDecl<R> f)
     {
         getContext().checkContextMatch(f);
         if (f.getArity() != 0)
@@ -59,7 +60,7 @@ public Expr getConstInterp(FuncDecl f)
         if (n == 0)
             return null;
         else
-            return Expr.create(getContext(), n);
+            return (Expr<R>) Expr.create(getContext(), n);
     }
 
     /**
@@ -70,7 +71,7 @@ public Expr getConstInterp(FuncDecl f)
      *         the model, null otherwise.
      * @throws Z3Exception
      **/
-    public FuncInterp getFuncInterp(FuncDecl f)
+    public <R extends Sort> FuncInterp<R> getFuncInterp(FuncDecl<R> f)
     {
         getContext().checkContextMatch(f);
 
@@ -90,7 +91,7 @@ public FuncInterp getFuncInterp(FuncDecl f)
                 {
                     if (Native.isAsArray(getContext().nCtx(), n)) {
                       long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
-                      return getFuncInterp(new FuncDecl(getContext(), fd));
+                      return getFuncInterp(new FuncDecl<>(getContext(), fd));
                     }
 		    return null;
                 }
@@ -106,7 +107,7 @@ public FuncInterp getFuncInterp(FuncDecl f)
             if (n == 0)
                 return null;
             else
-                return new FuncInterp(getContext(), n);
+                return new FuncInterp<>(getContext(), n);
         }
     }
 
@@ -123,12 +124,12 @@ public int getNumConsts()
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getConstDecls()
+    public FuncDecl<?>[] getConstDecls()
     {
         int n = getNumConsts();
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<?>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
+            res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
                     .nCtx(), getNativeObject(), i));
         return res;
     }
@@ -146,12 +147,12 @@ public int getNumFuncs()
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getFuncDecls()
+    public FuncDecl<?>[] getFuncDecls()
     {
         int n = getNumFuncs();
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<?>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
+            res[i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext()
                     .nCtx(), getNativeObject(), i));
         return res;
     }
@@ -161,17 +162,17 @@ public FuncDecl[] getFuncDecls()
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getDecls()
+    public FuncDecl<?>[] getDecls()
     {
         int nFuncs = getNumFuncs();
         int nConsts = getNumConsts();
         int n = nFuncs + nConsts;
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<?>[] res = new FuncDecl[n];
         for (int i = 0; i < nConsts; i++)
-            res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
+            res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
                     .nCtx(), getNativeObject(), i));
         for (int i = 0; i < nFuncs; i++)
-            res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
+            res[nConsts + i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(
                     getContext().nCtx(), getNativeObject(), i));
         return res;
     }
@@ -205,14 +206,14 @@ public ModelEvaluationFailedException()
      * @return The evaluation of {@code t} in the model.
      * @throws Z3Exception
      **/
-    public Expr eval(Expr t, boolean completion)
+    public <R extends Sort> Expr<R> eval(Expr<R> t, boolean completion)
     {
         Native.LongPtr v = new Native.LongPtr();
         if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
             t.getNativeObject(), (completion), v))
             throw new ModelEvaluationFailedException();
         else
-            return Expr.create(getContext(), v.value);
+            return (Expr<R>) Expr.create(getContext(), v.value);
     }
 
     /**
@@ -220,7 +221,7 @@ public Expr eval(Expr t, boolean completion)
      * 
      * @throws Z3Exception
      **/
-    public Expr evaluate(Expr t, boolean completion)
+    public <R extends Sort> Expr<R> evaluate(Expr<R> t, boolean completion)
     {
         return eval(t, completion);
     }
@@ -265,12 +266,12 @@ public Sort[] getSorts()
      *         of {@code s}
      * @throws Z3Exception
      **/
-    public Expr[] getSortUniverse(Sort s)
+    public <R extends Sort>  Expr<R>[] getSortUniverse(R s)
     {
 
         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
-        return nUniv.ToExprArray();
+        return (Expr<R>[]) nUniv.ToExprArray();
     }
 
     /**
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index ae50d7f33b0..741dd08d99d 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -24,6 +24,7 @@ Nikolaj Bjorner (nbjorner) 2015-07-16
 /**
  * Object for managing optimization context
  **/
+@SuppressWarnings("unchecked")
 public class Optimize extends Z3Object {
 
     /**
@@ -55,10 +56,10 @@ public ParamDescrs getParameterDescriptions()
     /**
      * Assert a constraint (or multiple) into the optimize solver.
      **/
-    public void Assert(BoolExpr ... constraints)
+    public void Assert(Expr<BoolSort> ... constraints)
     {
         getContext().checkContextMatch(constraints);
-        for (BoolExpr a : constraints)
+        for (Expr<BoolSort> a : constraints)
         {
             Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
         }
@@ -67,7 +68,7 @@ public void Assert(BoolExpr ... constraints)
     /**
      * Alias for Assert.
      **/
-    public void Add(BoolExpr ... constraints)
+    public void Add(Expr<BoolSort> ... constraints)
     {
         Assert(constraints);
     }
@@ -75,7 +76,7 @@ public void Add(BoolExpr ... constraints)
     /**
      * Handle to objectives returned by objective functions.
      **/
-    public static class Handle {
+    public static class Handle<R extends Sort> {
 
         private final Optimize opt;
         private final int handle;
@@ -89,7 +90,7 @@ public static class Handle {
         /**
          * Retrieve a lower bound for the objective handle.
          **/
-        public Expr getLower()
+        public Expr<R> getLower()
         {
             return opt.GetLower(handle);
         }
@@ -97,7 +98,7 @@ public Expr getLower()
         /**
          * Retrieve an upper bound for the objective handle.
          **/
-        public Expr getUpper()
+        public Expr<R> getUpper()
         {
             return opt.GetUpper(handle);
         }
@@ -110,7 +111,7 @@ public Expr getUpper()
          * and otherwise is represented by the expression {@code value + eps * EPSILON},
          * where {@code EPSILON} is an arbitrarily small real number.
          */
-        public Expr[] getUpperAsVector()
+        public Expr<?>[] getUpperAsVector()
         {
             return opt.GetUpperAsVector(handle);
         }
@@ -120,7 +121,7 @@ public Expr[] getUpperAsVector()
          *
          * <p>See {@link #getUpperAsVector()} for triple semantics.
          */
-        public Expr[] getLowerAsVector()
+        public Expr<?>[] getLowerAsVector()
         {
             return opt.GetLowerAsVector(handle);
         }
@@ -128,7 +129,7 @@ public Expr[] getLowerAsVector()
         /**
          * Retrieve the value of an objective.
          **/
-        public Expr getValue()
+        public Expr<R> getValue()
         {
             return getLower();
         }
@@ -149,11 +150,11 @@ public String toString()
      * Return an objective which associates with the group of constraints.
      *
      **/
-    public Handle AssertSoft(BoolExpr constraint, int weight, String group)
+    public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group)
     {
         getContext().checkContextMatch(constraint);
         Symbol s = getContext().mkSymbol(group);
-        return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
+        return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
     }
 
     /**
@@ -161,7 +162,7 @@ public Handle AssertSoft(BoolExpr constraint, int weight, String group)
      * Produce a model that (when the objectives are bounded and 
      * don't use strict inequalities) meets the objectives.
      **/
-    public Status Check(Expr... assumptions)
+    public Status Check(Expr<BoolSort>... assumptions)
     {
         Z3_lbool r;
         if (assumptions == null) {
@@ -243,34 +244,34 @@ public BoolExpr[] getUnsatCore()
      *  Return a handle to the objective. The handle is used as
      *  to retrieve the values of objectives after calling Check.
      **/            
-    public Handle MkMaximize(Expr e)
+    public <R extends Sort> Handle<R> MkMaximize(Expr<R> e)
     {
-        return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle<>(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
 
     /**
      *  Declare an arithmetical minimization objective. 
      *  Similar to MkMaximize.
      **/
-    public Handle MkMinimize(Expr e)
+    public <R extends Sort> Handle<R> MkMinimize(Expr<R> e)
     {
-        return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+        return new Handle<>(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
     
     /**
      *  Retrieve a lower bound for the objective handle.
      **/
-    private Expr GetLower(int index)
+    private <R extends Sort> Expr<R> GetLower(int index)
     {
-        return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
+        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
      *  Retrieve an upper bound for the objective handle.
      **/
-    private Expr GetUpper(int index)
+    private <R extends Sort> Expr<R> GetUpper(int index)
     {
-        return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
+        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
@@ -278,7 +279,7 @@ private Expr GetUpper(int index)
      *
      * <p>See {@link Handle#getUpperAsVector}.
      */
-    private Expr[] GetUpperAsVector(int index) {
+    private Expr<?>[] GetUpperAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetUpperAsVector(
                         getContext().nCtx(), getNativeObject(), index
@@ -291,7 +292,7 @@ private Expr[] GetUpperAsVector(int index) {
      *
      * <p>See {@link Handle#getLowerAsVector}.
      */
-    private Expr[] GetLowerAsVector(int index) {
+    private Expr<?>[] GetLowerAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetLowerAsVector(
                         getContext().nCtx(), getNativeObject(), index
@@ -299,12 +300,12 @@ private Expr[] GetLowerAsVector(int index) {
         );
     }
 
-    private Expr[] unpackObjectiveValueVector(long nativeVec) {
+    private Expr<?>[] unpackObjectiveValueVector(long nativeVec) {
         ASTVector vec = new ASTVector(
                 getContext(), nativeVec
         );
         return new Expr[] {
-                (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
+                (Expr<?>) vec.get(0), (Expr<?>) vec.get(1), (Expr<?>) vec.get(2)
         };
 
     }
@@ -355,7 +356,7 @@ public BoolExpr[] getAssertions()
     /**
      * The set of asserted formulas.
      */
-    public Expr[] getObjectives() 
+    public Expr<?>[] getObjectives()
     {
         ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
         return objectives.ToExprArray();
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index 852ffcd0f53..ae29d8b7d83 100644
--- a/src/api/java/Pattern.java
+++ b/src/api/java/Pattern.java
@@ -36,11 +36,11 @@ public int getNumTerms()
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getTerms()
+    public Expr<?>[] getTerms()
     {
 
         int n = getNumTerms();
-        Expr[] res = new Expr[n];
+        Expr<?>[] res = new Expr[n];
         for (int i = 0; i < n; i++)
             res[i] = Expr.create(getContext(),
                     Native.getPattern(getContext().nCtx(), getNativeObject(), i));
diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java
index 6b2f1d4fcc1..89ff61a3dc0 100644
--- a/src/api/java/Quantifier.java
+++ b/src/api/java/Quantifier.java
@@ -139,9 +139,9 @@ public Sort[] getBoundVariableSorts()
      * 
      * @throws Z3Exception
      **/
-    public Expr getBody()
+    public BoolExpr getBody()
     {
-        return Expr.create(getContext(), Native.getQuantifierBody(getContext()
+        return (BoolExpr) Expr.create(getContext(), Native.getQuantifierBody(getContext()
                 .nCtx(), getNativeObject()));
     }
 
@@ -168,7 +168,7 @@ public Quantifier translate(Context ctx)
      */
     public static Quantifier of(
             Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
-            Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
+            Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
             Symbol quantifierID, Symbol skolemID) {
         ctx.checkContextMatch(patterns);
         ctx.checkContextMatch(noPatterns);
@@ -212,8 +212,8 @@ public static Quantifier of(
      * @param quantifierID Nullable quantifier identifier.
      * @param skolemID Nullable skolem identifier.
      */
-    public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body,
-            int weight, Pattern[] patterns, Expr[] noPatterns,
+    public static Quantifier of(Context ctx, boolean isForall, Expr<?>[] bound, Expr<BoolSort> body,
+            int weight, Pattern[] patterns, Expr<?>[] noPatterns,
             Symbol quantifierID, Symbol skolemID) {
         ctx.checkContextMatch(noPatterns);
         ctx.checkContextMatch(patterns);
diff --git a/src/api/java/ReExpr.java b/src/api/java/ReExpr.java
index 60dc2bf96f3..fa3d85b542e 100644
--- a/src/api/java/ReExpr.java
+++ b/src/api/java/ReExpr.java
@@ -20,7 +20,7 @@
 /**
  * Re expressions
  **/
-public class ReExpr extends Expr
+public class ReExpr<R extends Sort> extends Expr<ReSort<R>>
 {
     /**
      * Constructor for ReExpr
diff --git a/src/api/java/ReSort.java b/src/api/java/ReSort.java
index 74e7c5c5fde..250eb42522c 100644
--- a/src/api/java/ReSort.java
+++ b/src/api/java/ReSort.java
@@ -20,7 +20,7 @@
 /**
  * A Regular expression sort
  **/
-public class ReSort extends Sort
+public class ReSort<R extends Sort> extends Sort
 {
     ReSort(Context ctx, long obj)
     {
diff --git a/src/api/java/RealExpr.java b/src/api/java/RealExpr.java
index c977e2ac0e0..cae9865a599 100644
--- a/src/api/java/RealExpr.java
+++ b/src/api/java/RealExpr.java
@@ -20,7 +20,7 @@
 /**
  * Real expressions
  **/
-public class RealExpr extends ArithExpr
+public class RealExpr extends ArithExpr<RealSort>
 {
     /**
      * Constructor for RealExpr
diff --git a/src/api/java/SeqExpr.java b/src/api/java/SeqExpr.java
index 47976dd5eb1..56980856059 100644
--- a/src/api/java/SeqExpr.java
+++ b/src/api/java/SeqExpr.java
@@ -20,7 +20,7 @@
 /**
  * Seq expressions
  **/
-public class SeqExpr extends Expr
+public class SeqExpr<R extends Sort> extends Expr<SeqSort<R>>
 {
     /**
      * Constructor for SeqExpr
diff --git a/src/api/java/SeqSort.java b/src/api/java/SeqSort.java
index 5c7a549c910..28b865733a9 100644
--- a/src/api/java/SeqSort.java
+++ b/src/api/java/SeqSort.java
@@ -20,7 +20,7 @@
 /**
  * A Sequence sort
  **/
-public class SeqSort extends Sort
+public class SeqSort<R extends Sort> extends Sort
 {
     SeqSort(Context ctx, long obj)
     {
diff --git a/src/api/java/SetSort.java b/src/api/java/SetSort.java
index 2aa821250e0..bb89a735060 100644
--- a/src/api/java/SetSort.java
+++ b/src/api/java/SetSort.java
@@ -20,14 +20,14 @@
 /**
  * Set sorts.
  **/
-public class SetSort extends Sort
+public class SetSort<D extends Sort> extends ArraySort<D, BoolSort>
 {
     SetSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    SetSort(Context ctx, Sort ty)
+    SetSort(Context ctx, D ty)
     {
         super(ctx, Native.mkSetSort(ctx.nCtx(), ty.getNativeObject()));
     }
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 7711adb3633..ce795d75833 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -24,6 +24,7 @@
 /**
  * Solvers.
  **/
+@SuppressWarnings("unchecked")
 public class Solver extends Z3Object {
     /**
      * A string that describes all available solver parameters.
@@ -122,10 +123,10 @@ public void interrupt()
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr... constraints)
+    public void add(Expr<BoolSort>... constraints)
     {
         getContext().checkContextMatch(constraints);
-        for (BoolExpr a : constraints)
+        for (Expr<BoolSort> a : constraints)
         {
             Native.solverAssert(getContext().nCtx(), getNativeObject(),
                     a.getNativeObject());
@@ -147,7 +148,7 @@ public void add(BoolExpr... constraints)
      * and the Boolean literals
      * provided using {@link #check()} with assumptions.
      **/
-    public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
+    public void assertAndTrack(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)
     {
         getContext().checkContextMatch(constraints);
         getContext().checkContextMatch(ps);
@@ -174,7 +175,7 @@ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
      * and the Boolean literals
      * provided using {@link #check} with assumptions.
      */ 
-    public void assertAndTrack(BoolExpr constraint, BoolExpr p)
+    public void assertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
     {
         getContext().checkContextMatch(constraint);
         getContext().checkContextMatch(p);
@@ -229,7 +230,8 @@ public BoolExpr[] getAssertions()
      * @see #getUnsatCore
      * @see #getProof
      **/
-    public Status check(Expr... assumptions)
+    @SafeVarargs
+    public final Status check(Expr<BoolSort>... assumptions)
     {
         Z3_lbool r;
         if (assumptions == null) {
@@ -250,6 +252,7 @@ public Status check(Expr... assumptions)
      * @see #getUnsatCore
      * @see #getProof
      **/
+    @SuppressWarnings("rawtypes")
     public Status check()
     {
         return check((Expr[]) null);
@@ -266,13 +269,13 @@ public Status check()
      * is fixed.
      *
      */
-    public Status getConsequences(BoolExpr[] assumptions, Expr[] variables, List<BoolExpr> consequences) 
+    public Status getConsequences(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)
     {
 	ASTVector result = new ASTVector(getContext());
 	ASTVector asms = new ASTVector(getContext());
 	ASTVector vars = new ASTVector(getContext());
-	for (BoolExpr asm : assumptions) asms.push(asm);
-	for (Expr v : variables) vars.push(v);
+	for (Expr<BoolSort> asm : assumptions) asms.push(asm);
+	for (Expr<?> v : variables) vars.push(v);
 	int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
         for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
 	return lboolToStatus(Z3_lbool.fromInt(r));
@@ -307,7 +310,7 @@ public Model getModel()
      * 
      * @throws Z3Exception
      **/
-    public Expr getProof()
+    public Expr<?> getProof()
     {
         long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
         if (x == 0) {
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index a8941705910..f612b9031c9 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -119,13 +119,13 @@ static Sort create(Context ctx, long obj)
         switch (sk)
         {
         case Z3_ARRAY_SORT:
-            return new ArraySort(ctx, obj);
+            return new ArraySort<>(ctx, obj);
         case Z3_BOOL_SORT:
             return new BoolSort(ctx, obj);
         case Z3_BV_SORT:
             return new BitVecSort(ctx, obj);
         case Z3_DATATYPE_SORT:
-            return new DatatypeSort(ctx, obj);
+            return new DatatypeSort<>(ctx, obj);
         case Z3_INT_SORT:
             return new IntSort(ctx, obj);
         case Z3_REAL_SORT:
@@ -141,9 +141,9 @@ static Sort create(Context ctx, long obj)
         case Z3_ROUNDING_MODE_SORT:
             return new FPRMSort(ctx, obj);
         case Z3_SEQ_SORT:
-            return new SeqSort(ctx, obj);
+            return new SeqSort<>(ctx, obj);
         case Z3_RE_SORT:
-            return new ReSort(ctx, obj);
+            return new ReSort<>(ctx, obj);
         default:
             throw new Z3Exception("Unknown sort kind");
         }
diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java
index ede20d26055..3b600f0fac1 100644
--- a/src/api/java/TupleSort.java
+++ b/src/api/java/TupleSort.java
@@ -26,10 +26,10 @@ public class TupleSort extends Sort
      * The constructor function of the tuple.
      * @throws Z3Exception 
      **/
-    public FuncDecl mkDecl()
+    public FuncDecl<TupleSort> mkDecl()
     {
 
-        return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext()
+        return new FuncDecl<>(getContext(), Native.getTupleSortMkDecl(getContext()
                 .nCtx(), getNativeObject()));
     }
 
@@ -45,13 +45,13 @@ public int getNumFields()
      * The field declarations.
      * @throws Z3Exception 
      **/
-    public FuncDecl[] getFieldDecls()
+    public FuncDecl<?>[] getFieldDecls()
     {
 
         int n = getNumFields();
-        FuncDecl[] res = new FuncDecl[n];
+        FuncDecl<?>[] res = new FuncDecl[n];
         for (int i = 0; i < n; i++)
-            res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl(
+            res[i] = new FuncDecl<>(getContext(), Native.getTupleSortFieldDecl(
                     getContext().nCtx(), getNativeObject(), i));
         return res;
     }