diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 5c49b56ae..4a579f9da 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -41,7 +41,7 @@ class JavaExample
// / </code>
// / Where, <code>finv</code>is a fresh function declaration.
- public BoolExpr injAxiom(Context ctx, FuncDecl f, int i) throws Z3Exception
+ public BoolExpr injAxiom(Context ctx, FuncDecl f, int i)
{
Sort[] domain = f.getDomain();
int sz = f.getDomainSize();
@@ -102,7 +102,6 @@ class JavaExample
// / Where, <code>finv</code>is a fresh function declaration.
public BoolExpr injAxiomAbs(Context ctx, FuncDecl f, int i)
- throws Z3Exception
{
Sort[] domain = f.getDomain();
int sz = f.getDomainSize();
@@ -179,7 +178,7 @@ class JavaExample
// / "Hello world" example: create a Z3 logical context, and delete it.
- public void simpleExample() throws Z3Exception
+ public void simpleExample()
{
System.out.println("SimpleExample");
Log.append("SimpleExample");
@@ -193,8 +192,7 @@ class JavaExample
}
}
- Model check(Context ctx, BoolExpr f, Status sat) throws Z3Exception,
- TestFailedException
+ Model check(Context ctx, BoolExpr f, Status sat) throws TestFailedException
{
Solver s = ctx.mkSolver();
s.add(f);
@@ -207,7 +205,7 @@ class JavaExample
}
void solveTactical(Context ctx, Tactic t, Goal g, Status sat)
- throws Z3Exception, TestFailedException
+ throws TestFailedException
{
Solver s = ctx.mkSolver(t);
System.out.println("\nTactical solver: " + s);
@@ -220,7 +218,7 @@ class JavaExample
throw new TestFailedException();
}
- ApplyResult applyTactic(Context ctx, Tactic t, Goal g) throws Z3Exception
+ ApplyResult applyTactic(Context ctx, Tactic t, Goal g)
{
System.out.println("\nGoal: " + g);
@@ -250,15 +248,14 @@ class JavaExample
return res;
}
- void prove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
- TestFailedException
+ void prove(Context ctx, BoolExpr f, boolean useMBQI) throws TestFailedException
{
BoolExpr[] assumptions = new BoolExpr[0];
prove(ctx, f, useMBQI, assumptions);
}
void prove(Context ctx, BoolExpr f, boolean useMBQI,
- BoolExpr... assumptions) throws Z3Exception, TestFailedException
+ BoolExpr... assumptions) throws TestFailedException
{
System.out.println("Proving: " + f);
Solver s = ctx.mkSolver();
@@ -283,15 +280,15 @@ class JavaExample
}
}
- void disprove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
- TestFailedException
+ void disprove(Context ctx, BoolExpr f, boolean useMBQI)
+ throws TestFailedException
{
BoolExpr[] a = {};
disprove(ctx, f, useMBQI, a);
}
void disprove(Context ctx, BoolExpr f, boolean useMBQI,
- BoolExpr... assumptions) throws Z3Exception, TestFailedException
+ BoolExpr... assumptions) throws TestFailedException
{
System.out.println("Disproving: " + f);
Solver s = ctx.mkSolver();
@@ -316,8 +313,7 @@ class JavaExample
}
}
- void modelConverterTest(Context ctx) throws Z3Exception,
- TestFailedException
+ void modelConverterTest(Context ctx) throws TestFailedException
{
System.out.println("ModelConverterTest");
@@ -357,7 +353,7 @@ class JavaExample
// / A simple array example.
- void arrayExample1(Context ctx) throws Z3Exception, TestFailedException
+ void arrayExample1(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample1");
Log.append("ArrayExample1");
@@ -407,8 +403,7 @@ class JavaExample
// / <remarks>This example demonstrates how to use the array
// theory.</remarks>
- public void arrayExample2(Context ctx) throws Z3Exception,
- TestFailedException
+ public void arrayExample2(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample2");
Log.append("ArrayExample2");
@@ -457,8 +452,7 @@ class JavaExample
// / <remarks>This example also shows how to use the <code>distinct</code>
// construct.</remarks>
- public void arrayExample3(Context ctx) throws Z3Exception,
- TestFailedException
+ public void arrayExample3(Context ctx) throws TestFailedException
{
System.out.println("ArrayExample3");
Log.append("ArrayExample2");
@@ -497,7 +491,7 @@ class JavaExample
// / Sudoku solving example.
- void sudokuExample(Context ctx) throws Z3Exception, TestFailedException
+ void sudokuExample(Context ctx) throws TestFailedException
{
System.out.println("SudokuExample");
Log.append("SudokuExample");
@@ -600,7 +594,7 @@ class JavaExample
// / A basic example of how to use quantifiers.
- void quantifierExample1(Context ctx) throws Z3Exception
+ void quantifierExample1(Context ctx)
{
System.out.println("QuantifierExample");
Log.append("QuantifierExample");
@@ -638,7 +632,7 @@ class JavaExample
System.out.println("Quantifier Y: " + y.toString());
}
- void quantifierExample2(Context ctx) throws Z3Exception
+ void quantifierExample2(Context ctx)
{
System.out.println("QuantifierExample2");
@@ -694,8 +688,7 @@ class JavaExample
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
- public void quantifierExample3(Context ctx) throws Z3Exception,
- TestFailedException
+ public void quantifierExample3(Context ctx) throws TestFailedException
{
System.out.println("QuantifierExample3");
Log.append("QuantifierExample3");
@@ -736,8 +729,7 @@ class JavaExample
// / <code>f</code> is injective in the second argument. <seealso
// cref="inj_axiom"/>
- public void quantifierExample4(Context ctx) throws Z3Exception,
- TestFailedException
+ public void quantifierExample4(Context ctx) throws TestFailedException
{
System.out.println("QuantifierExample4");
Log.append("QuantifierExample4");
@@ -776,7 +768,7 @@ class JavaExample
// / Some basic tests.
- void basicTests(Context ctx) throws Z3Exception, TestFailedException
+ void basicTests(Context ctx) throws TestFailedException
{
System.out.println("BasicTests");
@@ -890,7 +882,7 @@ class JavaExample
// / Some basic expression casting tests.
- void castingTest(Context ctx) throws Z3Exception, TestFailedException
+ void castingTest(Context ctx) throws TestFailedException
{
System.out.println("CastingTest");
@@ -1038,7 +1030,7 @@ class JavaExample
// / Shows how to read an SMT1 file.
- void smt1FileTest(String filename) throws Z3Exception
+ void smt1FileTest(String filename)
{
System.out.print("SMT File test ");
@@ -1054,7 +1046,7 @@ class JavaExample
// / Shows how to read an SMT2 file.
- void smt2FileTest(String filename) throws Z3Exception
+ void smt2FileTest(String filename)
{
Date before = new Date();
@@ -1096,7 +1088,7 @@ class JavaExample
// / Shows how to use Solver(logic)
// / @param ctx
- void logicExample(Context ctx) throws Z3Exception, TestFailedException
+ void logicExample(Context ctx) throws TestFailedException
{
System.out.println("LogicTest");
Log.append("LogicTest");
@@ -1128,7 +1120,7 @@ class JavaExample
// / Demonstrates how to use the ParOr tactic.
- void parOrExample(Context ctx) throws Z3Exception, TestFailedException
+ void parOrExample(Context ctx) throws TestFailedException
{
System.out.println("ParOrExample");
Log.append("ParOrExample");
@@ -1151,7 +1143,7 @@ class JavaExample
throw new TestFailedException();
}
- void bigIntCheck(Context ctx, RatNum r) throws Z3Exception
+ void bigIntCheck(Context ctx, RatNum r)
{
System.out.println("Num: " + r.getBigIntNumerator());
System.out.println("Den: " + r.getBigIntDenominator());
@@ -1159,8 +1151,7 @@ class JavaExample
// / Find a model for <code>x xor y</code>.
- public void findModelExample1(Context ctx) throws Z3Exception,
- TestFailedException
+ public void findModelExample1(Context ctx) throws TestFailedException
{
System.out.println("FindModelExample1");
Log.append("FindModelExample1");
@@ -1177,8 +1168,7 @@ class JavaExample
// / 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 Z3Exception,
- TestFailedException
+ public void findModelExample2(Context ctx) throws TestFailedException
{
System.out.println("FindModelExample2");
Log.append("FindModelExample2");
@@ -1217,8 +1207,7 @@ class JavaExample
// / <remarks>This function demonstrates how to create uninterpreted
// / types and functions.</remarks>
- public void proveExample1(Context ctx) throws Z3Exception,
- TestFailedException
+ public void proveExample1(Context ctx) throws TestFailedException
{
System.out.println("ProveExample1");
Log.append("ProveExample1");
@@ -1264,8 +1253,7 @@ class JavaExample
// / <remarks>This example demonstrates how to combine uninterpreted
// functions
// / and arithmetic.</remarks>
- public void proveExample2(Context ctx) throws Z3Exception,
- TestFailedException
+ public void proveExample2(Context ctx) throws TestFailedException
{
System.out.println("ProveExample2");
Log.append("ProveExample2");
@@ -1319,8 +1307,7 @@ class JavaExample
// / <remarks>This example also demonstrates how big numbers can be
// / created in ctx.</remarks>
- public void pushPopExample1(Context ctx) throws Z3Exception,
- TestFailedException
+ public void pushPopExample1(Context ctx) throws TestFailedException
{
System.out.println("PushPopExample1");
Log.append("PushPopExample1");
@@ -1386,8 +1373,7 @@ class JavaExample
// / <remarks>Check that the projection of a tuple
// / returns the corresponding element.</remarks>
- public void tupleExample(Context ctx) throws Z3Exception,
- TestFailedException
+ public void tupleExample(Context ctx) throws TestFailedException
{
System.out.println("TupleExample");
Log.append("TupleExample");
@@ -1422,8 +1408,7 @@ class JavaExample
// / This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit)
// machine integers
// / </remarks>
- public void bitvectorExample1(Context ctx) throws Z3Exception,
- TestFailedException
+ public void bitvectorExample1(Context ctx) throws TestFailedException
{
System.out.println("BitvectorExample1");
Log.append("BitvectorExample1");
@@ -1444,8 +1429,7 @@ class JavaExample
// / Find x and y such that: x ^ y - 103 == x * y
- public void bitvectorExample2(Context ctx) throws Z3Exception,
- TestFailedException
+ public void bitvectorExample2(Context ctx) throws TestFailedException
{
System.out.println("BitvectorExample2");
Log.append("BitvectorExample2");
@@ -1470,8 +1454,7 @@ class JavaExample
// / Demonstrates how to use the SMTLIB parser.
- public void parserExample1(Context ctx) throws Z3Exception,
- TestFailedException
+ public void parserExample1(Context ctx) throws TestFailedException
{
System.out.println("ParserExample1");
Log.append("ParserExample1");
@@ -1489,8 +1472,7 @@ class JavaExample
// / Demonstrates how to initialize the parser symbol table.
- public void parserExample2(Context ctx) throws Z3Exception,
- TestFailedException
+ public void parserExample2(Context ctx) throws TestFailedException
{
System.out.println("ParserExample2");
Log.append("ParserExample2");
@@ -1532,7 +1514,7 @@ class JavaExample
// / Display the declarations, assumptions and formulas in a SMT-LIB string.
- public void parserExample4(Context ctx) throws Z3Exception
+ public void parserExample4(Context ctx)
{
System.out.println("ParserExample4");
Log.append("ParserExample4");
@@ -1579,7 +1561,7 @@ class JavaExample
// / Create an ite-Expr (if-then-else Exprs).
- public void iteExample(Context ctx) throws Z3Exception
+ public void iteExample(Context ctx)
{
System.out.println("ITEExample");
Log.append("ITEExample");
@@ -1594,8 +1576,7 @@ class JavaExample
// / Create an enumeration data type.
- public void enumExample(Context ctx) throws Z3Exception,
- TestFailedException
+ public void enumExample(Context ctx) throws TestFailedException
{
System.out.println("EnumExample");
Log.append("EnumExample");
@@ -1642,8 +1623,7 @@ class JavaExample
// / Create a list datatype.
- public void listExample(Context ctx) throws Z3Exception,
- TestFailedException
+ public void listExample(Context ctx) throws TestFailedException
{
System.out.println("ListExample");
Log.append("ListExample");
@@ -1706,8 +1686,7 @@ class JavaExample
// / Create a binary tree datatype.
- public void treeExample(Context ctx) throws Z3Exception,
- TestFailedException
+ public void treeExample(Context ctx) throws TestFailedException
{
System.out.println("TreeExample");
Log.append("TreeExample");
@@ -1779,8 +1758,7 @@ class JavaExample
// / forest ::= nil | cons(tree, forest)
// / tree ::= nil | cons(forest, forest)
// / </remarks>
- public void forestExample(Context ctx) throws Z3Exception,
- TestFailedException
+ public void forestExample(Context ctx) throws TestFailedException
{
System.out.println("ForestExample");
Log.append("ForestExample");
@@ -1899,7 +1877,7 @@ class JavaExample
// / Demonstrate how to use #Eval.
- public void evalExample1(Context ctx) throws Z3Exception
+ public void evalExample1(Context ctx)
{
System.out.println("EvalExample1");
Log.append("EvalExample1");
@@ -1939,7 +1917,7 @@ class JavaExample
// / Demonstrate how to use #Eval on tuples.
- public void evalExample2(Context ctx) throws Z3Exception
+ public void evalExample2(Context ctx)
{
System.out.println("EvalExample2");
Log.append("EvalExample2");
@@ -1990,8 +1968,7 @@ class JavaExample
// / 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) throws Z3Exception
+ public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize)
{
int num_Exprs = to_minimize.length;
int[] upper = new int[num_Exprs];
@@ -2063,7 +2040,7 @@ class JavaExample
// / Reduced-size model generation example.
- public void findSmallModelExample(Context ctx) throws Z3Exception
+ public void findSmallModelExample(Context ctx)
{
System.out.println("FindSmallModelExample");
Log.append("FindSmallModelExample");
@@ -2080,7 +2057,7 @@ class JavaExample
// / Simplifier example.
- public void simplifierExample(Context ctx) throws Z3Exception
+ public void simplifierExample(Context ctx)
{
System.out.println("SimplifierExample");
Log.append("SimplifierExample");
@@ -2098,7 +2075,7 @@ class JavaExample
// / Extract unsatisfiable core example
- public void unsatCoreAndProofExample(Context ctx) throws Z3Exception
+ public void unsatCoreAndProofExample(Context ctx)
{
System.out.println("UnsatCoreAndProofExample");
Log.append("UnsatCoreAndProofExample");
@@ -2140,7 +2117,7 @@ class JavaExample
/// Extract unsatisfiable core example with AssertAndTrack
- public void unsatCoreAndProofExample2(Context ctx) throws Z3Exception
+ public void unsatCoreAndProofExample2(Context ctx)
{
System.out.println("UnsatCoreAndProofExample2");
Log.append("UnsatCoreAndProofExample2");
@@ -2179,7 +2156,7 @@ class JavaExample
}
}
- public void finiteDomainExample(Context ctx) throws Z3Exception
+ public void finiteDomainExample(Context ctx)
{
System.out.println("FiniteDomainExample");
Log.append("FiniteDomainExample");
@@ -2198,7 +2175,7 @@ class JavaExample
// System.out.println(ctx.mkEq(s1, t1));
}
- public void floatingPointExample1(Context ctx) throws Z3Exception, TestFailedException
+ public void floatingPointExample1(Context ctx) throws TestFailedException
{
System.out.println("FloatingPointExample1");
Log.append("FloatingPointExample1");
@@ -2249,7 +2226,7 @@ class JavaExample
System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr);
}
- public void floatingPointExample2(Context ctx) throws Z3Exception, TestFailedException
+ public void floatingPointExample2(Context ctx) throws TestFailedException
{
System.out.println("FloatingPointExample2");
Log.append("FloatingPointExample2");