merge with unstable branch

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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,
+    Model check(Context ctx, BoolExpr f, Status sat) throws TestFailedException
-            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,
+    void prove(Context ctx, BoolExpr f, boolean useMBQI) throws TestFailedException
-            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,
+    void disprove(Context ctx, BoolExpr f, boolean useMBQI) 
-            TestFailedException
+		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,
+    void modelConverterTest(Context ctx) throws TestFailedException
-            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,
+    public void arrayExample2(Context ctx) throws TestFailedException
-            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,
+    public void arrayExample3(Context ctx) throws TestFailedException
-            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,
+    public void quantifierExample3(Context ctx) throws TestFailedException
-            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,
+    public void quantifierExample4(Context ctx) throws TestFailedException
-            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,
+    public void findModelExample1(Context ctx) throws TestFailedException
-            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,
+    public void findModelExample2(Context ctx) throws TestFailedException
-            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,
+    public void proveExample1(Context ctx) throws TestFailedException
-            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,
+    public void proveExample2(Context ctx) throws TestFailedException
-            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,
+    public void pushPopExample1(Context ctx) throws TestFailedException
-            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,
+    public void tupleExample(Context ctx) throws TestFailedException
-            TestFailedException
     {
         System.out.println("TupleExample");
         Log.append("TupleExample");
@@ -1422,8 +1408,7 @@ class JavaExample
     // / This example disproves that x - 10 &lt;= 0 IFF x &lt;= 10 for (32-bit)
     // machine integers
     // / </remarks>
-    public void bitvectorExample1(Context ctx) throws Z3Exception,
+    public void bitvectorExample1(Context ctx) throws TestFailedException
-            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,
+    public void bitvectorExample2(Context ctx) throws TestFailedException
-            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,
+    public void parserExample1(Context ctx) throws TestFailedException
-            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,
+    public void parserExample2(Context ctx) throws TestFailedException
-            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,
+    public void enumExample(Context ctx) throws TestFailedException
-            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,
+    public void listExample(Context ctx) throws TestFailedException
-            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,
+    public void treeExample(Context ctx) throws TestFailedException
-            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,
+    public void forestExample(Context ctx) throws TestFailedException
-            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,
+    public void checkSmall(Context ctx, Solver solver, BitVecExpr... to_minimize)
-            BitVecExpr... to_minimize) throws Z3Exception
     {
         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");

scripts/mk_util.py

@@ -572,7 +572,7 @@ def parse_options():
             LINUX_X64=False
         elif opt in ('-h', '--help'):
             display_help(0)
-        elif opt in ('-m', '--onlymakefiles'):
+        elif opt in ('-m', '--makefiles'):
             ONLY_MAKEFILES = True
         elif opt in ('-c', '--showcpp'):
             SHOW_CPPS = True
@@ -1275,6 +1275,7 @@ class JavaDLLComponent(Component):
         self.dll_name     = dll_name
         self.package_name = package_name
         self.manifest_file = manifest_file
+        self.install = not is_windows()
 
     def mk_makefile(self, out):
         global JAVAC
@@ -1345,6 +1346,18 @@ class JavaDLLComponent(Component):
             shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
                         os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
 
+    def mk_install(self, out):
+        if is_java_enabled() and self.install:
+            dllfile = '%s$(SO_EXT)' % self.dll_name
+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
+            out.write('\t@cp %s.jar %s.jar\n' % (self.package_name, os.path.join('$(PREFIX)', 'lib', self.package_name)))
+
+    def mk_uninstall(self, out):
+        if is_java_enabled() and self.install:
+            dllfile = '%s$(SO_EXT)' % self.dll_name
+            out.write('\t@rm %s\n' % (os.path.join('$(PREFIX)', 'lib', dllfile)))
+            out.write('\t@rm %s.jar\n' % (os.path.join('$(PREFIX)', 'lib', self.package_name)))
+
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
         Component.__init__(self, name, path, deps)
@@ -2797,19 +2810,19 @@ def mk_z3consts_ml(api_files):
                     if name not in DeprecatedEnums:
                         efile.write('(** %s *)\n' % name[3:])
                         efile.write('type %s =\n' % name[3:]) # strip Z3_
-                        for k, i in decls.iteritems():
+                        for k, i in decls.items():
                             efile.write('  | %s \n' % k[3:]) # strip Z3_
                         efile.write('\n')
                         efile.write('(** Convert %s to int*)\n' % name[3:])
                         efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
                         efile.write('  match x with\n')
-                        for k, i in decls.iteritems():
+                        for k, i in decls.items():
                             efile.write('  | %s -> %d\n' % (k[3:], i))
                         efile.write('\n')
                         efile.write('(** Convert int to %s*)\n' % name[3:])
                         efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
                         efile.write('  match x with\n')
-                        for k, i in decls.iteritems():
+                        for k, i in decls.items():
                             efile.write('  | %d -> %s\n' % (i, k[3:]))
                         # use Z3.Exception?
                         efile.write('  | _ -> raise (Failure "undefined enum value")\n\n')
@@ -2875,7 +2888,7 @@ def mk_z3consts_ml(api_files):
                     if name not in DeprecatedEnums:
                         efile.write('(** %s *)\n' % name[3:])
                         efile.write('type %s =\n' % name[3:]) # strip Z3_
-                        for k, i in decls.iteritems():
+                        for k, i in decls.items():
                             efile.write('  | %s \n' % k[3:]) # strip Z3_
                         efile.write('\n')
                         efile.write('(** Convert %s to int*)\n' % name[3:])

scripts/update_api.py

@@ -1174,7 +1174,7 @@ def mk_ml():
     ml_i.write('type ptr\n')
     ml_native.write('and z3_symbol = ptr\n')
     ml_i.write('and z3_symbol = ptr\n')
-    for k, v in Type2Str.iteritems():
+    for k, v in Type2Str.items():
         if is_obj(k):
             ml_native.write('and %s = ptr\n' % v.lower())
             ml_i.write('and %s = ptr\n' % v.lower())

src/api/api_interp.cpp

@@ -66,7 +66,6 @@ extern "C" {
         // Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
 
         Z3_context ctx = Z3_mk_context(cfg);
-        Z3_del_config(cfg);
         return ctx;
     }
 

src/api/dotnet/ASTVector.cs

@@ -25,7 +25,7 @@ namespace Microsoft.Z3
     /// <summary>
     /// Vectors of ASTs.
     /// </summary>
-    internal class ASTVector : Z3Object
+    public class ASTVector : Z3Object
     {
         /// <summary>
         /// The size of the vector

src/api/dotnet/InterpolationContext.cs

@@ -47,7 +47,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_get_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+        public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
@@ -72,7 +72,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);

src/api/java/AST.java

@@ -54,7 +54,7 @@ public class AST extends Z3Object
      * positive if after else zero.
      * @throws Z3Exception on error
      **/
-    public int compareTo(Object other) throws Z3Exception
+    public int compareTo(Object other)
     {
         if (other == null)
             return 1;
@@ -95,7 +95,7 @@ public class AST extends Z3Object
      * A unique identifier for the AST (unique among all ASTs).
      * @throws Z3Exception on error
      **/
-    public int getId() throws Z3Exception
+    public int getId()
     {
         return Native.getAstId(getContext().nCtx(), getNativeObject());
     }
@@ -107,7 +107,7 @@ public class AST extends Z3Object
      * @return A copy of the AST which is associated with {@code ctx}
      * @throws Z3Exception on error
      **/
-    public AST translate(Context ctx) throws Z3Exception
+    public AST translate(Context ctx)
     {
 
         if (getContext() == ctx)
@@ -121,7 +121,7 @@ public class AST extends Z3Object
      * The kind of the AST.
      * @throws Z3Exception on error
      **/
-    public Z3_ast_kind getASTKind() throws Z3Exception
+    public Z3_ast_kind getASTKind()
     {
         return Z3_ast_kind.fromInt(Native.getAstKind(getContext().nCtx(),
                 getNativeObject()));
@@ -132,7 +132,7 @@ public class AST extends Z3Object
      * @throws Z3Exception on error
      * @throws Z3Exception on error
      **/
-    public boolean isExpr() throws Z3Exception
+    public boolean isExpr()
     {
         switch (getASTKind())
         {
@@ -151,7 +151,7 @@ public class AST extends Z3Object
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isApp() throws Z3Exception
+    public boolean isApp()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_APP_AST;
     }
@@ -161,7 +161,7 @@ public class AST extends Z3Object
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isVar() throws Z3Exception
+    public boolean isVar()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_VAR_AST;
     }
@@ -171,7 +171,7 @@ public class AST extends Z3Object
      * @return a boolean
      * @throws Z3Exception on error
      **/
-    public boolean isQuantifier() throws Z3Exception
+    public boolean isQuantifier()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_QUANTIFIER_AST;
     }
@@ -179,7 +179,7 @@ public class AST extends Z3Object
     /**
      * Indicates whether the AST is a Sort
      **/
-    public boolean isSort() throws Z3Exception
+    public boolean isSort()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_SORT_AST;
     }
@@ -187,7 +187,7 @@ public class AST extends Z3Object
     /**
      * Indicates whether the AST is a FunctionDeclaration
      **/
-    public boolean isFuncDecl() throws Z3Exception
+    public boolean isFuncDecl()
     {
         return this.getASTKind() == Z3_ast_kind.Z3_FUNC_DECL_AST;
     }
@@ -209,7 +209,7 @@ public class AST extends Z3Object
     /**
      * A string representation of the AST in s-expression notation.
      **/
-    public String getSExpr() throws Z3Exception
+    public String getSExpr()
     {
         return Native.astToString(getContext().nCtx(), getNativeObject());
     }
@@ -219,12 +219,12 @@ public class AST extends Z3Object
         super(ctx);
     }
 
-    AST(Context ctx, long obj) throws Z3Exception
+    AST(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         // Console.WriteLine("AST IncRef()");
         if (getContext() == null || o == 0)
@@ -233,7 +233,7 @@ public class AST extends Z3Object
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         // Console.WriteLine("AST DecRef()");
         if (getContext() == null || o == 0)
@@ -242,7 +242,7 @@ public class AST extends Z3Object
         super.decRef(o);
     }
 
-    static AST create(Context ctx, long obj) throws Z3Exception
+    static AST create(Context ctx, long obj)
     {
         switch (Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj)))
         {

src/api/java/ASTMap.java

@@ -29,7 +29,7 @@ class ASTMap extends Z3Object
      * @return True if {@code k} is a key in the map, false
      *         otherwise.
      **/
-    public boolean contains(AST k) throws Z3Exception
+    public boolean contains(AST k)
     {
 
         return Native.astMapContains(getContext().nCtx(), getNativeObject(),
@@ -44,7 +44,7 @@ class ASTMap extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public AST find(AST k) throws Z3Exception
+    public AST find(AST k)
     {
         return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
                 getNativeObject(), k.getNativeObject()));
@@ -55,7 +55,7 @@ class ASTMap extends Z3Object
      * @param k The key AST
      * @param v The value AST
      **/
-    public void insert(AST k, AST v) throws Z3Exception
+    public void insert(AST k, AST v)
     {
 
         Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
@@ -66,7 +66,7 @@ class ASTMap extends Z3Object
      * Erases the key {@code k} from the map. 
      * @param k An AST
      **/
-    public void erase(AST k) throws Z3Exception
+    public void erase(AST k)
     {
         Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
     }
@@ -74,7 +74,7 @@ class ASTMap extends Z3Object
     /**
      * Removes all keys from the map.
      **/
-    public void reset() throws Z3Exception
+    public void reset()
     {
         Native.astMapReset(getContext().nCtx(), getNativeObject());
     }
@@ -82,7 +82,7 @@ class ASTMap extends Z3Object
     /**
      * The size of the map
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.astMapSize(getContext().nCtx(), getNativeObject());
     }
@@ -92,7 +92,7 @@ class ASTMap extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ASTVector getKeys() throws Z3Exception
+    public ASTVector getKeys()
     {
         return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
                 getNativeObject()));
@@ -112,23 +112,23 @@ class ASTMap extends Z3Object
         }
     }
 
-    ASTMap(Context ctx, long obj) throws Z3Exception
+    ASTMap(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ASTMap(Context ctx) throws Z3Exception
+    ASTMap(Context ctx)
     {
         super(ctx, Native.mkAstMap(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getASTMapDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getASTMapDRQ().add(o);
         super.decRef(o);

src/api/java/ASTVector.java

@@ -20,12 +20,12 @@ package com.microsoft.z3;
 /**
  * Vectors of ASTs.
  **/
-class ASTVector extends Z3Object
+public class ASTVector extends Z3Object
 {
     /**
      * The size of the vector
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.astVectorSize(getContext().nCtx(), getNativeObject());
     }
@@ -39,13 +39,13 @@ class ASTVector extends Z3Object
      * @return An AST
      * @throws Z3Exception
      **/
-    public AST get(int i) throws Z3Exception
+    public AST get(int i)
     {
         return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
                 getNativeObject(), i));
     }
 
-    public void set(int i, AST value) throws Z3Exception
+    public void set(int i, AST value)
     {
 
         Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
@@ -56,7 +56,7 @@ class ASTVector extends Z3Object
      * Resize the vector to {@code newSize}. 
      * @param newSize The new size of the vector.
      **/
-    public void resize(int newSize) throws Z3Exception
+    public void resize(int newSize)
     {
         Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
     }
@@ -66,7 +66,7 @@ class ASTVector extends Z3Object
      * increased by 1. 
      * @param a An AST
      **/
-    public void push(AST a) throws Z3Exception
+    public void push(AST a)
     {
         Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
     }
@@ -78,7 +78,7 @@ class ASTVector extends Z3Object
      * @return A new ASTVector
      * @throws Z3Exception
      **/
-    public ASTVector translate(Context ctx) throws Z3Exception
+    public ASTVector translate(Context ctx)
     {
         return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
                 .nCtx(), getNativeObject(), ctx.nCtx()));
@@ -98,23 +98,23 @@ class ASTVector extends Z3Object
         }
     }
 
-    ASTVector(Context ctx, long obj) throws Z3Exception
+    ASTVector(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ASTVector(Context ctx) throws Z3Exception
+    ASTVector(Context ctx)
     {
         super(ctx, Native.mkAstVector(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getASTVectorDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);

src/api/java/AlgebraicNum.java

@@ -32,7 +32,7 @@ public class AlgebraicNum extends ArithExpr
 	 * @return A numeral Expr of sort Real
 	 * @throws Z3Exception on error
 	 **/
-	public RatNum toUpper(int precision) throws Z3Exception
+	public RatNum toUpper(int precision)
 	{
 
 		return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
@@ -49,7 +49,7 @@ public class AlgebraicNum extends ArithExpr
 	 * @return A numeral Expr of sort Real
 	 * @throws Z3Exception on error
 	 **/
-	public RatNum toLower(int precision) throws Z3Exception
+	public RatNum toLower(int precision)
 	{
 
 		return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
@@ -63,14 +63,14 @@ public class AlgebraicNum extends ArithExpr
 	 * @return String
 	 * @throws Z3Exception on error
 	 **/
-	public String toDecimal(int precision) throws Z3Exception
+	public String toDecimal(int precision)
 	{
 
 		return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
 				precision);
 	}
 
-	AlgebraicNum(Context ctx, long obj) throws Z3Exception
+	AlgebraicNum(Context ctx, long obj)
 	{
 		super(ctx, obj);
 

src/api/java/ApplyResult.java

@@ -26,7 +26,7 @@ public class ApplyResult extends Z3Object
     /**
      * The number of Subgoals.
      **/
-    public int getNumSubgoals() throws Z3Exception
+    public int getNumSubgoals()
     {
         return Native.applyResultGetNumSubgoals(getContext().nCtx(),
                 getNativeObject());
@@ -37,7 +37,7 @@ public class ApplyResult extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Goal[] getSubgoals() throws Z3Exception
+    public Goal[] getSubgoals()
     {
         int n = getNumSubgoals();
         Goal[] res = new Goal[n];
@@ -54,7 +54,7 @@ public class ApplyResult extends Z3Object
      * @return A model for {@code g}
      * @throws Z3Exception
      **/
-    public Model convertModel(int i, Model m) throws Z3Exception
+    public Model convertModel(int i, Model m)
     {
         return new Model(getContext(), 
             Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
@@ -74,18 +74,18 @@ public class ApplyResult extends Z3Object
         }
     }
 
-    ApplyResult(Context ctx, long obj) throws Z3Exception
+    ApplyResult(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getApplyResultDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getApplyResultDRQ().add(o);
         super.decRef(o);

src/api/java/ArithExpr.java

@@ -25,7 +25,7 @@ public class ArithExpr extends Expr
     /**
      * Constructor for ArithExpr
      **/
-    ArithExpr(Context ctx, long obj) throws Z3Exception
+    ArithExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/ArithSort.java

@@ -22,7 +22,7 @@ package com.microsoft.z3;
  **/
 public class ArithSort extends Sort
 {
-    ArithSort(Context ctx, long obj) throws Z3Exception
+    ArithSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/ArrayExpr.java

@@ -26,7 +26,7 @@ public class ArrayExpr extends Expr
     /**
      * Constructor for ArrayExpr
      **/
-    ArrayExpr(Context ctx, long obj) throws Z3Exception
+    ArrayExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/ArraySort.java

@@ -28,7 +28,7 @@ public class ArraySort extends Sort
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getDomain() throws Z3Exception
+    public Sort getDomain()
     {
         return Sort.create(getContext(),
                 Native.getArraySortDomain(getContext().nCtx(), getNativeObject()));
@@ -40,18 +40,18 @@ public class ArraySort extends Sort
      * @throws Z3Exception on error
      * @return a sort
      **/
-    public Sort getRange() throws Z3Exception
+    public Sort getRange()
     {
         return Sort.create(getContext(),
                 Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
     }
 
-    ArraySort(Context ctx, long obj) throws Z3Exception
+    ArraySort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ArraySort(Context ctx, Sort domain, Sort range) throws Z3Exception
+    ArraySort(Context ctx, Sort domain, Sort range)
     {
         super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
                 range.getNativeObject()));

src/api/java/BitVecExpr.java

@@ -29,7 +29,7 @@ public class BitVecExpr extends Expr
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getSortSize() throws Z3Exception
+    public int getSortSize()
     {
         return ((BitVecSort) getSort()).getSize();
     }
@@ -37,7 +37,7 @@ public class BitVecExpr extends Expr
     /**
      * Constructor for BitVecExpr
      **/
-    BitVecExpr(Context ctx, long obj) throws Z3Exception
+    BitVecExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/BitVecNum.java

@@ -29,7 +29,7 @@ public class BitVecNum extends BitVecExpr
      * 
      * @throws Z3Exception
      **/
-    public int getInt() throws Z3Exception
+    public int getInt()
     {
         Native.IntPtr res = new Native.IntPtr();
         if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
@@ -42,7 +42,7 @@ public class BitVecNum extends BitVecExpr
      * 
      * @throws Z3Exception
      **/
-    public long getLong() throws Z3Exception
+    public long getLong()
     {
         Native.LongPtr res = new Native.LongPtr();
         if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
@@ -72,7 +72,7 @@ public class BitVecNum extends BitVecExpr
         }
     }
 
-    BitVecNum(Context ctx, long obj) throws Z3Exception
+    BitVecNum(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/BitVecSort.java

@@ -27,12 +27,12 @@ public class BitVecSort extends Sort
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getSize() throws Z3Exception
+    public int getSize()
     {
         return Native.getBvSortSize(getContext().nCtx(), getNativeObject());
     }
 
-    BitVecSort(Context ctx, long obj) throws Z3Exception
+    BitVecSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/BoolExpr.java

@@ -35,7 +35,7 @@ public class BoolExpr extends Expr
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    BoolExpr(Context ctx, long obj) throws Z3Exception
+    BoolExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/BoolSort.java

@@ -22,6 +22,6 @@ package com.microsoft.z3;
  **/
 public class BoolSort extends Sort
 {
-    BoolSort(Context ctx, long obj) throws Z3Exception { super(ctx, obj); {  }}
+    BoolSort(Context ctx, long obj) { super(ctx, obj); {  }}
-    BoolSort(Context ctx) throws Z3Exception { super(ctx, Native.mkBoolSort(ctx.nCtx())); {  }}
+    BoolSort(Context ctx) { super(ctx, Native.mkBoolSort(ctx.nCtx())); {  }}
 };

src/api/java/Constructor.java

@@ -28,7 +28,7 @@ public class Constructor extends Z3Object
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getNumFields() throws Z3Exception
+    public int getNumFields()
     {    
         return n;
     }
@@ -38,7 +38,7 @@ public class Constructor extends Z3Object
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl ConstructorDecl() throws Z3Exception
+    public FuncDecl ConstructorDecl()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
@@ -52,7 +52,7 @@ public class Constructor extends Z3Object
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl getTesterDecl() throws Z3Exception
+    public FuncDecl getTesterDecl()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
@@ -66,7 +66,7 @@ public class Constructor extends Z3Object
      * @throws Z3Exception 
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getAccessorDecls() throws Z3Exception
+    public FuncDecl[] getAccessorDecls()
     {
         Native.LongPtr constructor = new Native.LongPtr();
         Native.LongPtr tester = new Native.LongPtr();
@@ -82,7 +82,7 @@ public class Constructor extends Z3Object
      * Destructor.
      * @throws Z3Exception on error
      **/
-    protected void finalize() throws Z3Exception
+    protected void finalize()
     {
         Native.delConstructor(getContext().nCtx(), getNativeObject());
     }
@@ -91,7 +91,7 @@ public class Constructor extends Z3Object
 
     Constructor(Context ctx, Symbol name, Symbol recognizer,
             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
-            throws Z3Exception
+           
     {
         super(ctx);
 

src/api/java/ConstructorList.java

@@ -26,17 +26,17 @@ public class ConstructorList extends Z3Object
      * Destructor.
      * @throws Z3Exception on error
      **/
-    protected void finalize() throws Z3Exception
+    protected void finalize()
     {
         Native.delConstructorList(getContext().nCtx(), getNativeObject());
     }
 
-    ConstructorList(Context ctx, long obj) throws Z3Exception
+    ConstructorList(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    ConstructorList(Context ctx, Constructor[] constructors) throws Z3Exception
+    ConstructorList(Context ctx, Constructor[] constructors)
     {
         super(ctx);
 

src/api/java/DatatypeExpr.java

@@ -25,7 +25,7 @@ public class DatatypeExpr extends Expr
     /**
      * Constructor for DatatypeExpr
      **/
-    DatatypeExpr(Context ctx, long obj) throws Z3Exception
+    DatatypeExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/DatatypeSort.java

@@ -27,7 +27,7 @@ public class DatatypeSort extends Sort
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getNumConstructors() throws Z3Exception
+    public int getNumConstructors()
     {
         return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
                 getNativeObject());
@@ -39,7 +39,7 @@ public class DatatypeSort extends Sort
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getConstructors() throws Z3Exception
+    public FuncDecl[] getConstructors()
     {
         int n = getNumConstructors();
         FuncDecl[] res = new FuncDecl[n];
@@ -55,7 +55,7 @@ public class DatatypeSort extends Sort
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getRecognizers() throws Z3Exception
+    public FuncDecl[] getRecognizers()
     {
         int n = getNumConstructors();
         FuncDecl[] res = new FuncDecl[n];
@@ -71,7 +71,7 @@ public class DatatypeSort extends Sort
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public FuncDecl[][] getAccessors() throws Z3Exception
+    public FuncDecl[][] getAccessors()
     {
 
         int n = getNumConstructors();
@@ -92,13 +92,13 @@ public class DatatypeSort extends Sort
         return res;
     }
 
-    DatatypeSort(Context ctx, long obj) throws Z3Exception
+    DatatypeSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
     DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
-            throws Z3Exception
+           
     {
         super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
                 (int) constructors.length, arrayToNative(constructors)));

src/api/java/EnumSort.java

@@ -26,7 +26,7 @@ public class EnumSort extends Sort
      * The function declarations of the constants in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getConstDecls() throws Z3Exception
+    public FuncDecl[] getConstDecls()
     {
         int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
         FuncDecl[] t = new FuncDecl[n];
@@ -39,7 +39,7 @@ public class EnumSort extends Sort
      * Retrieves the inx'th constant declaration in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl getConstDecl(int inx) throws Z3Exception
+    public FuncDecl getConstDecl(int inx)
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
     }
@@ -49,7 +49,7 @@ public class EnumSort extends Sort
      * @throws Z3Exception on error
      * @return an Expr[]
      **/
-    public Expr[] getConsts() throws Z3Exception
+    public Expr[] getConsts()
     {        
         FuncDecl[] cds = getConstDecls();
         Expr[] t = new Expr[cds.length];
@@ -63,7 +63,7 @@ public class EnumSort extends Sort
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr getConst(int inx) throws Z3Exception
+    public Expr getConst(int inx)
     {        
     	return getContext().mkApp(getConstDecl(inx));
     }
@@ -72,7 +72,7 @@ public class EnumSort extends Sort
      * The test predicates for the constants in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl[] getTesterDecls() throws Z3Exception
+    public FuncDecl[] getTesterDecls()
     {
         int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
         FuncDecl[] t = new FuncDecl[n];
@@ -85,12 +85,12 @@ public class EnumSort extends Sort
      * Retrieves the inx'th tester/recognizer declaration in the enumeration.
      * @throws Z3Exception on error
      **/
-    public FuncDecl getTesterDecl(int inx) throws Z3Exception
+    public FuncDecl getTesterDecl(int inx)
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
     }
 
-    EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
+    EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
     {
         super(ctx, 0);
 

src/api/java/FPExpr.java

@@ -25,15 +25,15 @@ public class FPExpr extends Expr
      * The number of exponent bits.
      * @throws Z3Exception 
      */
-    public int getEBits() throws Z3Exception { return ((FPSort)getSort()).getEBits(); }
+    public int getEBits() { return ((FPSort)getSort()).getEBits(); }
 
     /**
      * The number of significand bits.
      * @throws Z3Exception 
      */
-    public int getSBits() throws Z3Exception { return ((FPSort)getSort()).getSBits(); }
+    public int getSBits() { return ((FPSort)getSort()).getSBits(); }
     
-    public FPExpr(Context ctx, long obj) throws Z3Exception
+    public FPExpr(Context ctx, long obj)
     {
         super(ctx, obj); 
     }

src/api/java/FPNum.java

@@ -26,7 +26,7 @@ public class FPNum extends FPExpr
      * Remarks: returns true if the numeral is negative 
      * @throws Z3Exception 
      */
-    public boolean getSign() throws Z3Exception {
+    public boolean getSign() {
         Native.IntPtr res = new Native.IntPtr();
         if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true)                
             throw new Z3Exception("Sign is not a Boolean value");
@@ -39,7 +39,7 @@ public class FPNum extends FPExpr
      * enough to represent the real significand precisely.
      * @throws Z3Exception 
      **/
-    public String getSignificand() throws Z3Exception {
+    public String getSignificand() {
         return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
     }
 
@@ -47,7 +47,7 @@ public class FPNum extends FPExpr
      * Return the exponent value of a floating-point numeral as a string
      * @throws Z3Exception 
      */
-    public String getExponent() throws Z3Exception {
+    public String getExponent() {
         return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
     }
 
@@ -55,14 +55,14 @@ public class FPNum extends FPExpr
      * Return the exponent value of a floating-point numeral as a signed 64-bit integer
      * @throws Z3Exception 
      */
-    public long getExponentInt64() throws Z3Exception  {
+    public long getExponentInt64()  {
         Native.LongPtr res = new Native.LongPtr();
         if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
             throw new Z3Exception("Exponent is not a 64 bit integer");
         return res.value;
     }
     
-    public FPNum(Context ctx, long obj) throws Z3Exception
+    public FPNum(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/FPRMExpr.java

@@ -21,7 +21,7 @@ package com.microsoft.z3;
  */
 public class FPRMExpr extends Expr
 {       
-    public FPRMExpr(Context ctx, long obj) throws Z3Exception
+    public FPRMExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/FPRMNum.java

@@ -27,63 +27,63 @@ public class FPRMNum extends FPRMExpr {
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
      * @throws Z3Exception 
      * **/
-    public boolean isRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+    public boolean isRoundNearestTiesToEven() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
      * @throws Z3Exception 
      */
-    public boolean isRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
+    public boolean isRNE() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
      * @throws Z3Exception 
      */
-    public boolean isRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
+    public boolean isRoundNearestTiesToAway() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
      * @throws Z3Exception 
      */
-    public boolean isRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
+    public boolean isRNA() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
      * @throws Z3Exception 
      */
-    public boolean isRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+    public boolean isRoundTowardPositive() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardPositive
      * @throws Z3Exception 
      */
-    public boolean isRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
+    public boolean isRTP() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
      * @throws Z3Exception 
      */
-    public boolean isRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
+    public boolean isRoundTowardNegative() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardNegative
      * @throws Z3Exception 
      */
-    public boolean isRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } 
+    public boolean isRTN() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } 
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardZero
      * @throws Z3Exception 
      */
-    public boolean isRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+    public boolean isRoundTowardZero() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
 
     /**
      * Indicates whether the term is the floating-point rounding numeral roundTowardZero
      * @throws Z3Exception 
      */
-    public boolean isRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
+    public boolean isRTZ() { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
     
-    public FPRMNum(Context ctx, long obj) throws Z3Exception {
+    public FPRMNum(Context ctx, long obj) {
         super(ctx, obj);
     }
 

src/api/java/FPRMSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
 public class FPRMSort extends Sort
 {
 
-    public FPRMSort(Context ctx) throws Z3Exception
+    public FPRMSort(Context ctx)
     {        
         super(ctx, Native.mkFpaRoundingModeSort(ctx.nCtx()));
     }
 
-    public FPRMSort(Context ctx, long obj) throws Z3Exception
+    public FPRMSort(Context ctx, long obj)
     {
         super(ctx, obj); 
     }

src/api/java/FPSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
 public class FPSort extends Sort
 {
 
-    public FPSort(Context ctx, long obj) throws Z3Exception
+    public FPSort(Context ctx, long obj)
     {
         super(ctx, obj);        
     }
     
-    public FPSort(Context ctx, int ebits, int sbits) throws Z3Exception
+    public FPSort(Context ctx, int ebits, int sbits)
     {
         super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));        
     }
@@ -35,14 +35,14 @@ public class FPSort extends Sort
     /**
      * The number of exponent bits.
      */
-    public int getEBits() throws Z3Exception {
+    public int getEBits() {
         return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
     }
     
     /**
      * The number of significand bits.
      */
-    public int getSBits() throws Z3Exception {
+    public int getSBits() {
         return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
     }
     

src/api/java/FiniteDomainSort.java

@@ -26,19 +26,19 @@ public class FiniteDomainSort extends Sort
      * The size of the finite domain sort.
      * @throws Z3Exception on error
      **/
-    public long getSize() throws Z3Exception
+    public long getSize()
     {
         Native.LongPtr res = new Native.LongPtr();
         Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
         return res.value;
     }
 
-    FiniteDomainSort(Context ctx, long obj) throws Z3Exception
+    FiniteDomainSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    FiniteDomainSort(Context ctx, Symbol name, long size) throws Z3Exception
+    FiniteDomainSort(Context ctx, Symbol name, long size)
     {
         super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
                 size));

src/api/java/Fixedpoint.java

@@ -28,7 +28,7 @@ public class Fixedpoint extends Z3Object
     /**
      * A string that describes all available fixedpoint solver parameters.
      **/
-    public String getHelp() throws Z3Exception
+    public String getHelp()
     {
         return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
     }
@@ -38,7 +38,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void setParameters(Params value) throws Z3Exception
+    public void setParameters(Params value)
     {
 
         getContext().checkContextMatch(value);
@@ -51,7 +51,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ParamDescrs getParameterDescriptions() throws Z3Exception
+    public ParamDescrs getParameterDescriptions()
     {
         return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
                 getContext().nCtx(), getNativeObject()));
@@ -62,7 +62,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr ... constraints) throws Z3Exception
+    public void add(BoolExpr ... constraints)
     {
         getContext().checkContextMatch(constraints);
         for (BoolExpr a : constraints)
@@ -77,7 +77,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void registerRelation(FuncDecl f) throws Z3Exception
+    public void registerRelation(FuncDecl f)
     {
 
         getContext().checkContextMatch(f);
@@ -90,7 +90,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void addRule(BoolExpr rule, Symbol name) throws Z3Exception
+    public void addRule(BoolExpr rule, Symbol name)
     {
 
         getContext().checkContextMatch(rule);
@@ -103,7 +103,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void addFact(FuncDecl pred, int ... args) throws Z3Exception
+    public void addFact(FuncDecl pred, int ... args)
     {
         getContext().checkContextMatch(pred);
         Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
@@ -119,7 +119,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Status query(BoolExpr query) throws Z3Exception
+    public Status query(BoolExpr query)
     {
 
         getContext().checkContextMatch(query);
@@ -144,7 +144,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Status query(FuncDecl[] relations) throws Z3Exception
+    public Status query(FuncDecl[] relations)
     {
 
         getContext().checkContextMatch(relations);
@@ -166,7 +166,7 @@ public class Fixedpoint extends Z3Object
      * Creates a backtracking point. 
      * @see pop
      **/
-    public void push() throws Z3Exception
+    public void push()
     {
         Native.fixedpointPush(getContext().nCtx(), getNativeObject());
     }
@@ -178,7 +178,7 @@ public class Fixedpoint extends Z3Object
      *  
      * @see push
      **/
-    public void pop() throws Z3Exception
+    public void pop()
     {
         Native.fixedpointPop(getContext().nCtx(), getNativeObject());
     }
@@ -188,7 +188,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void updateRule(BoolExpr rule, Symbol name) throws Z3Exception
+    public void updateRule(BoolExpr rule, Symbol name)
     {
 
         getContext().checkContextMatch(rule);
@@ -202,7 +202,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr getAnswer() throws Z3Exception
+    public Expr getAnswer()
     {
         long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
         return (ans == 0) ? null : Expr.create(getContext(), ans);
@@ -211,7 +211,7 @@ public class Fixedpoint extends Z3Object
     /**
      * Retrieve explanation why fixedpoint engine returned status Unknown.
      **/
-    public String getReasonUnknown() throws Z3Exception
+    public String getReasonUnknown()
     {
 
         return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
@@ -221,7 +221,7 @@ public class Fixedpoint extends Z3Object
     /**
      * Retrieve the number of levels explored for a given predicate.
      **/
-    public int getNumLevels(FuncDecl predicate) throws Z3Exception
+    public int getNumLevels(FuncDecl predicate)
     {
         return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                 predicate.getNativeObject());
@@ -232,7 +232,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr getCoverDelta(int level, FuncDecl predicate) throws Z3Exception
+    public Expr getCoverDelta(int level, FuncDecl predicate)
     {
         long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
                 getNativeObject(), level, predicate.getNativeObject());
@@ -244,7 +244,7 @@ public class Fixedpoint extends Z3Object
      * at <tt>level</tt>.
      **/
     public void addCover(int level, FuncDecl predicate, Expr property)
-            throws Z3Exception
+           
     {
         Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                 predicate.getNativeObject(), property.getNativeObject());
@@ -269,7 +269,7 @@ public class Fixedpoint extends Z3Object
      * Instrument the Datalog engine on which table representation to use for
      * recursive predicate.
      **/
-    public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception
+    public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds)
     {
 
         Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
@@ -281,7 +281,7 @@ public class Fixedpoint extends Z3Object
     /**
      * Convert benchmark given as set of axioms, rules and queries to a string.
      **/
-    public String toString(BoolExpr[] queries) throws Z3Exception
+    public String toString(BoolExpr[] queries)
     {
 
         return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
@@ -293,7 +293,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public BoolExpr[] getRules() throws Z3Exception
+    public BoolExpr[] getRules()
     {
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
@@ -310,7 +310,7 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public BoolExpr[] getAssertions() throws Z3Exception
+    public BoolExpr[] getAssertions()
     {
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
@@ -339,18 +339,18 @@ public class Fixedpoint extends Z3Object
         super(ctx, obj);
     }
 
-    Fixedpoint(Context ctx) throws Z3Exception
+    Fixedpoint(Context ctx)
     {
         super(ctx, Native.mkFixedpoint(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getFixedpointDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getFixedpointDRQ().add(o);
         super.decRef(o);

src/api/java/FuncDecl.java

@@ -78,7 +78,7 @@ public class FuncDecl extends AST
     /**
      * Returns a unique identifier for the function declaration.
      **/
-    public int getId() throws Z3Exception
+    public int getId()
     {
         return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
     }
@@ -86,7 +86,7 @@ public class FuncDecl extends AST
     /**
      * The arity of the function declaration
      **/
-    public int getArity() throws Z3Exception
+    public int getArity()
     {
         return Native.getArity(getContext().nCtx(), getNativeObject());
     }
@@ -95,7 +95,7 @@ public class FuncDecl extends AST
      * The size of the domain of the function declaration 
      * @see getArity
      **/
-    public int getDomainSize() throws Z3Exception
+    public int getDomainSize()
     {
         return Native.getDomainSize(getContext().nCtx(), getNativeObject());
     }
@@ -103,7 +103,7 @@ public class FuncDecl extends AST
     /**
      * The domain of the function declaration
      **/
-    public Sort[] getDomain() throws Z3Exception
+    public Sort[] getDomain()
     {
 
         int n = getDomainSize();
@@ -118,7 +118,7 @@ public class FuncDecl extends AST
     /**
      * The range of the function declaration
      **/
-    public Sort getRange() throws Z3Exception
+    public Sort getRange()
     {
 
         return Sort.create(getContext(),
@@ -128,7 +128,7 @@ public class FuncDecl extends AST
     /**
      * The kind of the function declaration.
      **/
-    public Z3_decl_kind getDeclKind() throws Z3Exception
+    public Z3_decl_kind getDeclKind()
     {
         return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
                 getNativeObject()));
@@ -137,7 +137,7 @@ public class FuncDecl extends AST
     /**
      * The name of the function declaration
      **/
-    public Symbol getName() throws Z3Exception
+    public Symbol getName()
     {
 
         return Symbol.create(getContext(),
@@ -147,7 +147,7 @@ public class FuncDecl extends AST
     /**
      * The number of parameters of the function declaration
      **/
-    public int getNumParameters() throws Z3Exception
+    public int getNumParameters()
     {
         return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
     }
@@ -155,7 +155,7 @@ public class FuncDecl extends AST
     /**
      * The parameters of the function declaration
      **/
-    public Parameter[] getParameters() throws Z3Exception
+    public Parameter[] getParameters()
     {
 
         int num = getNumParameters();
@@ -223,7 +223,7 @@ public class FuncDecl extends AST
         /**
          * The int value of the parameter.
          **/
-        public int getInt() throws Z3Exception
+        public int getInt()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT)
                 throw new Z3Exception("parameter is not an int");
@@ -233,7 +233,7 @@ public class FuncDecl extends AST
         /**
          * The double value of the parameter.
          **/
-        public double getDouble() throws Z3Exception
+        public double getDouble()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
                 throw new Z3Exception("parameter is not a double ");
@@ -243,7 +243,7 @@ public class FuncDecl extends AST
         /**
          * The Symbol value of the parameter.
          **/
-        public Symbol getSymbol() throws Z3Exception
+        public Symbol getSymbol()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL)
                 throw new Z3Exception("parameter is not a Symbol");
@@ -253,7 +253,7 @@ public class FuncDecl extends AST
         /**
          * The Sort value of the parameter.
          **/
-        public Sort getSort() throws Z3Exception
+        public Sort getSort()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT)
                 throw new Z3Exception("parameter is not a Sort");
@@ -263,7 +263,7 @@ public class FuncDecl extends AST
         /**
          * The AST value of the parameter.
          **/
-        public AST getAST() throws Z3Exception
+        public AST getAST()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST)
                 throw new Z3Exception("parameter is not an AST");
@@ -273,7 +273,7 @@ public class FuncDecl extends AST
         /**
          * The FunctionDeclaration value of the parameter.
          **/
-        public FuncDecl getFuncDecl() throws Z3Exception
+        public FuncDecl getFuncDecl()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL)
                 throw new Z3Exception("parameter is not a function declaration");
@@ -283,7 +283,7 @@ public class FuncDecl extends AST
         /**
          * The rational string value of the parameter.
          **/
-        public String getRational() throws Z3Exception
+        public String getRational()
         {
             if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL)
                 throw new Z3Exception("parameter is not a rational String");
@@ -293,7 +293,7 @@ public class FuncDecl extends AST
         /**
          * The kind of the parameter.
          **/
-        public Z3_parameter_kind getParameterKind() throws Z3Exception
+        public Z3_parameter_kind getParameterKind()
         {
             return kind;
         }
@@ -341,14 +341,14 @@ public class FuncDecl extends AST
         }
     }
 
-    FuncDecl(Context ctx, long obj) throws Z3Exception
+    FuncDecl(Context ctx, long obj)
     {
         super(ctx, obj);
 
     }
 
     FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
-            throws Z3Exception
+           
     {
         super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -357,7 +357,7 @@ public class FuncDecl extends AST
     }
 
     FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
-            throws Z3Exception
+           
     {
         super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
                 AST.arrayLength(domain), AST.arrayToNative(domain),
@@ -365,7 +365,7 @@ public class FuncDecl extends AST
 
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
                 .toInt())
@@ -380,7 +380,7 @@ public class FuncDecl extends AST
      * 
      * @return
      **/
-    public Expr apply(Expr ... args) throws Z3Exception
+    public Expr apply(Expr ... args)
     {
         getContext().checkContextMatch(args);
         return Expr.create(getContext(), this, args);

src/api/java/FuncInterp.java

@@ -36,7 +36,7 @@ public class FuncInterp extends Z3Object
          * @throws Z3Exception
          * @throws Z3Exception on error
      **/
-        public Expr getValue() throws Z3Exception
+        public Expr getValue()
         {
             return Expr.create(getContext(),
                     Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
@@ -46,7 +46,7 @@ public class FuncInterp extends Z3Object
          * The number of arguments of the entry.
          * @throws Z3Exception on error
      **/
-        public int getNumArgs() throws Z3Exception
+        public int getNumArgs()
         {
             return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
         }
@@ -57,7 +57,7 @@ public class FuncInterp extends Z3Object
          * @throws Z3Exception
          * @throws Z3Exception on error
      **/
-        public Expr[] getArgs() throws Z3Exception
+        public Expr[] getArgs()
         {
             int n = getNumArgs();
             Expr[] res = new Expr[n];
@@ -86,18 +86,18 @@ public class FuncInterp extends Z3Object
             }
         }
 
-        Entry(Context ctx, long obj) throws Z3Exception
+        Entry(Context ctx, long obj)
         {
             super(ctx, obj);
         }
 
-        void incRef(long o) throws Z3Exception
+        void incRef(long o)
         {
             getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
             super.incRef(o);
         }
 
-        void decRef(long o) throws Z3Exception
+        void decRef(long o)
         {
             getContext().getFuncEntryDRQ().add(o);
             super.decRef(o);
@@ -109,7 +109,7 @@ public class FuncInterp extends Z3Object
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getNumEntries() throws Z3Exception
+    public int getNumEntries()
     {
         return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
     }
@@ -120,7 +120,7 @@ public class FuncInterp extends Z3Object
      * @throws Z3Exception
      * @throws Z3Exception on error
      **/
-    public Entry[] getEntries() throws Z3Exception
+    public Entry[] getEntries()
     {
         int n = getNumEntries();
         Entry[] res = new Entry[n];
@@ -137,7 +137,7 @@ public class FuncInterp extends Z3Object
      * @throws Z3Exception on error
      * @return an Expr
      **/
-    public Expr getElse() throws Z3Exception
+    public Expr getElse()
     {
         return Expr.create(getContext(),
                 Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
@@ -148,7 +148,7 @@ public class FuncInterp extends Z3Object
      * @throws Z3Exception on error
      * @return an int
      **/
-    public int getArity() throws Z3Exception
+    public int getArity()
     {
         return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
     }
@@ -187,18 +187,18 @@ public class FuncInterp extends Z3Object
         }
     }
 
-    FuncInterp(Context ctx, long obj) throws Z3Exception
+    FuncInterp(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getFuncInterpDRQ().add(o);
         super.decRef(o);

src/api/java/Global.java

@@ -81,7 +81,7 @@ public final class Global
      * globally.
      **/
     public static void ToggleWarningMessages(boolean enabled)
-            throws Z3Exception
+           
     {
         Native.toggleWarningMessages((enabled) ? true : false);
     }

src/api/java/Goal.java

@@ -33,7 +33,7 @@ public class Goal extends Z3Object
      * applied when the objective is to find a proof for a given goal.
      * 
      **/
-    public Z3_goal_prec getPrecision() throws Z3Exception
+    public Z3_goal_prec getPrecision()
     {
         return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
                 getNativeObject()));
@@ -42,7 +42,7 @@ public class Goal extends Z3Object
     /**
      * Indicates whether the goal is precise.
      **/
-    public boolean isPrecise() throws Z3Exception
+    public boolean isPrecise()
     {
         return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
     }
@@ -50,7 +50,7 @@ public class Goal extends Z3Object
     /**
      * Indicates whether the goal is an under-approximation.
      **/
-    public boolean isUnderApproximation() throws Z3Exception
+    public boolean isUnderApproximation()
     {
         return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
     }
@@ -58,7 +58,7 @@ public class Goal extends Z3Object
     /**
      * Indicates whether the goal is an over-approximation.
      **/
-    public boolean isOverApproximation() throws Z3Exception
+    public boolean isOverApproximation()
     {
         return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
     }
@@ -67,7 +67,7 @@ public class Goal extends Z3Object
      * Indicates whether the goal is garbage (i.e., the product of over- and
      * under-approximations).
      **/
-    public boolean isGarbage() throws Z3Exception
+    public boolean isGarbage()
     {
         return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
     }
@@ -77,7 +77,7 @@ public class Goal extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr ... constraints) throws Z3Exception
+    public void add(BoolExpr ... constraints)
     {
         getContext().checkContextMatch(constraints);
         for (BoolExpr c : constraints)
@@ -90,7 +90,7 @@ public class Goal extends Z3Object
     /**
      * Indicates whether the goal contains `false'.
      **/
-    public boolean inconsistent() throws Z3Exception
+    public boolean inconsistent()
     {
         return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
     }
@@ -100,7 +100,7 @@ public class Goal extends Z3Object
      * Remarks:  This tracks how many transformations
      * were applied to it. 
      **/
-    public int getDepth() throws Z3Exception
+    public int getDepth()
     {
         return Native.goalDepth(getContext().nCtx(), getNativeObject());
     }
@@ -108,7 +108,7 @@ public class Goal extends Z3Object
     /**
      * Erases all formulas from the given goal.
      **/
-    public void reset() throws Z3Exception
+    public void reset()
     {
         Native.goalReset(getContext().nCtx(), getNativeObject());
     }
@@ -116,7 +116,7 @@ public class Goal extends Z3Object
     /**
      * The number of formulas in the goal.
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.goalSize(getContext().nCtx(), getNativeObject());
     }
@@ -126,7 +126,7 @@ public class Goal extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public BoolExpr[] getFormulas() throws Z3Exception
+    public BoolExpr[] getFormulas()
     {
         int n = size();
         BoolExpr[] res = new BoolExpr[n];
@@ -139,7 +139,7 @@ public class Goal extends Z3Object
     /**
      * The number of formulas, subformulas and terms in the goal.
      **/
-    public int getNumExprs() throws Z3Exception
+    public int getNumExprs()
     {
         return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
     }
@@ -148,7 +148,7 @@ public class Goal extends Z3Object
      * Indicates whether the goal is empty, and it is precise or the product of
      * an under approximation.
      **/
-    public boolean isDecidedSat() throws Z3Exception
+    public boolean isDecidedSat()
     {
         return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
     }
@@ -157,7 +157,7 @@ public class Goal extends Z3Object
      * Indicates whether the goal contains `false', and it is precise or the
      * product of an over approximation.
      **/
-    public boolean isDecidedUnsat() throws Z3Exception
+    public boolean isDecidedUnsat()
     {
         return Native
                 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
@@ -168,7 +168,7 @@ public class Goal extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Goal translate(Context ctx) throws Z3Exception
+    public Goal translate(Context ctx)
     {
         return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
                 getNativeObject(), ctx.nCtx()));
@@ -179,7 +179,7 @@ public class Goal extends Z3Object
      * Remarks: Essentially invokes the `simplify' tactic
      * on the goal.
      **/
-    public Goal simplify() throws Z3Exception
+    public Goal simplify()
     {
         Tactic t = getContext().mkTactic("simplify");
         ApplyResult res = t.apply(this);
@@ -195,7 +195,7 @@ public class Goal extends Z3Object
      * Remarks: Essentially invokes the `simplify' tactic
      * on the goal.
      **/
-    public Goal simplify(Params p) throws Z3Exception
+    public Goal simplify(Params p)
     {
         Tactic t = getContext().mkTactic("simplify");
         ApplyResult res = t.apply(this, p);
@@ -222,25 +222,25 @@ public class Goal extends Z3Object
         }
     }
 
-    Goal(Context ctx, long obj) throws Z3Exception
+    Goal(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
     Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
-            throws Z3Exception
+           
     {
         super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
                 (unsatCores) ? true : false, (proofs) ? true : false));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getGoalDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getGoalDRQ().add(o);
         super.decRef(o);

src/api/java/IDisposable.java

@@ -21,7 +21,7 @@ package com.microsoft.z3;
 
 public class IDisposable
 {
-    public void dispose() throws Z3Exception
+    public void dispose()
     {
     }
 }

src/api/java/IntExpr.java

@@ -26,7 +26,7 @@ public class IntExpr extends ArithExpr
      * Constructor for IntExpr
      * @throws Z3Exception on error
      **/
-    IntExpr(Context ctx, long obj) throws Z3Exception
+    IntExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/IntNum.java

@@ -25,7 +25,7 @@ import java.math.BigInteger;
 public class IntNum extends IntExpr
 {
 
-    IntNum(Context ctx, long obj) throws Z3Exception
+    IntNum(Context ctx, long obj)
     {
         super(ctx, obj);
     }
@@ -33,7 +33,7 @@ public class IntNum extends IntExpr
     /**
      * Retrieve the int value.
      **/
-    public int getInt() throws Z3Exception
+    public int getInt()
     {
         Native.IntPtr res = new Native.IntPtr();
         if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
@@ -44,7 +44,7 @@ public class IntNum extends IntExpr
     /**
      * Retrieve the 64-bit int value.
      **/
-    public long getInt64() throws Z3Exception
+    public long getInt64()
     {
         Native.LongPtr res = new Native.LongPtr();
         if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
@@ -55,7 +55,7 @@ public class IntNum extends IntExpr
     /**
      * Retrieve the BigInteger value.
      **/
-    public BigInteger getBigInteger() throws Z3Exception
+    public BigInteger getBigInteger()
     {
         return new BigInteger(this.toString());
     }

src/api/java/IntSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
  **/
 public class IntSort extends ArithSort
 {
-    IntSort(Context ctx, long obj) throws Z3Exception
+    IntSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    IntSort(Context ctx) throws Z3Exception
+    IntSort(Context ctx)
     {
         super(ctx, Native.mkIntSort(ctx.nCtx()));
     }

src/api/java/IntSymbol.java

@@ -29,24 +29,24 @@ public class IntSymbol extends Symbol
      * Remarks: Throws an exception if the symbol
      * is not of int kind. 
      **/
-    public int getInt() throws Z3Exception
+    public int getInt()
     {
         if (!isIntSymbol())
             throw new Z3Exception("Int requested from non-Int symbol");
         return Native.getSymbolInt(getContext().nCtx(), getNativeObject());
     }
 
-    IntSymbol(Context ctx, long obj) throws Z3Exception
+    IntSymbol(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    IntSymbol(Context ctx, int i) throws Z3Exception
+    IntSymbol(Context ctx, int i)
     {
         super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
         if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
                 .toInt())

src/api/java/InterpolationContext.java

@@ -33,7 +33,7 @@ public class InterpolationContext extends Context
     /**
      * Constructor.
      **/
-    public InterpolationContext() throws Z3Exception
+    public InterpolationContext()
     {
         m_ctx = Native.mkInterpolationContext(0);
         initContext(); 
@@ -46,7 +46,7 @@ public class InterpolationContext extends Context
      * Remarks: 
      * @see Context#Context
      **/
-    public InterpolationContext(Map<String, String> settings) throws Z3Exception
+    public InterpolationContext(Map<String, String> settings)
     { 
         long cfg = Native.mkConfig();
         for (Map.Entry<String, String> kv : settings.entrySet())
@@ -60,7 +60,7 @@ public class InterpolationContext extends Context
       * Create an expression that marks a formula position for interpolation.
       * @throws Z3Exception 
       **/
-    public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception
+    public BoolExpr MkInterpolant(BoolExpr a)
     {
         checkContextMatch(a);        
         return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
@@ -73,7 +73,7 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
+    public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
     {
         checkContextMatch(pf);
         checkContextMatch(pat);
@@ -94,7 +94,7 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
+    public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model)
     {
         checkContextMatch(pat);
         checkContextMatch(p);
@@ -113,7 +113,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_interpolation_profile in the C/C++ API, which is 
     /// well documented.
-    public String InterpolationProfile() throws Z3Exception
+    public String InterpolationProfile()
     {
         return Native.interpolationProfile(nCtx());
     }
@@ -124,7 +124,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_check_interpolant in the C/C++ API, which is 
     /// well documented.
-    public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception
+    public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
     {
         Native.StringPtr n_err_str = new Native.StringPtr();
         int r = Native.checkInterpolant(nCtx(),
@@ -145,7 +145,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_read_interpolation_problem in the C/C++ API, which is 
     /// well documented.
-    public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
+    public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
     {
         Native.IntPtr n_num = new Native.IntPtr();
         Native.IntPtr n_num_theory = new Native.IntPtr();
@@ -176,7 +176,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_write_interpolation_problem in the C/C++ API, which is 
     /// well documented.
-    public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
+    public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
     {
         Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));     
     }

src/api/java/ListSort.java

@@ -26,7 +26,7 @@ public class ListSort extends Sort
      * The declaration of the nil function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getNilDecl() throws Z3Exception
+    public FuncDecl getNilDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
     }
@@ -35,7 +35,7 @@ public class ListSort extends Sort
      * The empty list.
      * @throws Z3Exception 
      **/
-    public Expr getNil() throws Z3Exception
+    public Expr getNil()
     {
         return getContext().mkApp(getNilDecl());
     }
@@ -44,7 +44,7 @@ public class ListSort extends Sort
      * The declaration of the isNil function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getIsNilDecl() throws Z3Exception
+    public FuncDecl getIsNilDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
     }
@@ -53,7 +53,7 @@ public class ListSort extends Sort
      * The declaration of the cons function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getConsDecl() throws Z3Exception
+    public FuncDecl getConsDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
     }
@@ -63,7 +63,7 @@ public class ListSort extends Sort
      * @throws Z3Exception 
      * 
      **/
-    public FuncDecl getIsConsDecl() throws Z3Exception
+    public FuncDecl getIsConsDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
     }
@@ -72,7 +72,7 @@ public class ListSort extends Sort
      * The declaration of the head function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getHeadDecl() throws Z3Exception
+    public FuncDecl getHeadDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
     }
@@ -81,12 +81,12 @@ public class ListSort extends Sort
      * The declaration of the tail function of this list sort.
      * @throws Z3Exception 
      **/
-    public FuncDecl getTailDecl() throws Z3Exception
+    public FuncDecl getTailDecl()
     {
         return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
     }
 
-    ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception
+    ListSort(Context ctx, Symbol name, Sort elemSort)
     {
         super(ctx, 0);
 

src/api/java/Log.java

@@ -53,7 +53,7 @@ public final class Log
      * log.
      * @throws Z3Exception 
      **/
-    public static void append(String s) throws Z3Exception
+    public static void append(String s)
     {
         if (!m_is_open)
             throw new Z3Exception("Log cannot be closed.");

src/api/java/Model.java

@@ -33,7 +33,7 @@ public class Model extends Z3Object
      *         null otherwise.
      * @throws Z3Exception
      **/
-    public Expr getConstInterp(Expr a) throws Z3Exception
+    public Expr getConstInterp(Expr a)
     {
         getContext().checkContextMatch(a);
         return getConstInterp(a.getFuncDecl());
@@ -48,7 +48,7 @@ public class Model extends Z3Object
      *         null otherwise.
      * @throws Z3Exception
      **/
-    public Expr getConstInterp(FuncDecl f) throws Z3Exception
+    public Expr getConstInterp(FuncDecl f)
     {
         getContext().checkContextMatch(f);
         if (f.getArity() != 0
@@ -74,7 +74,7 @@ public class Model extends Z3Object
      *         the model, null otherwise.
      * @throws Z3Exception
      **/
-    public FuncInterp getFuncInterp(FuncDecl f) throws Z3Exception
+    public FuncInterp getFuncInterp(FuncDecl f)
     {
         getContext().checkContextMatch(f);
 
@@ -117,7 +117,7 @@ public class Model extends Z3Object
     /**
      * The number of constants that have an interpretation in the model.
      **/
-    public int getNumConsts() throws Z3Exception
+    public int getNumConsts()
     {
         return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
     }
@@ -127,7 +127,7 @@ public class Model extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getConstDecls() throws Z3Exception
+    public FuncDecl[] getConstDecls()
     {
         int n = getNumConsts();
         FuncDecl[] res = new FuncDecl[n];
@@ -140,7 +140,7 @@ public class Model extends Z3Object
     /**
      * The number of function interpretations in the model.
      **/
-    public int getNumFuncs() throws Z3Exception
+    public int getNumFuncs()
     {
         return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
     }
@@ -150,7 +150,7 @@ public class Model extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getFuncDecls() throws Z3Exception
+    public FuncDecl[] getFuncDecls()
     {
         int n = getNumFuncs();
         FuncDecl[] res = new FuncDecl[n];
@@ -165,7 +165,7 @@ public class Model extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public FuncDecl[] getDecls() throws Z3Exception
+    public FuncDecl[] getDecls()
     {
         int nFuncs = getNumFuncs();
         int nConsts = getNumConsts();
@@ -208,7 +208,7 @@ public class Model extends Z3Object
      * @return The evaluation of {@code t} in the model.
      * @throws Z3Exception
      **/
-    public Expr eval(Expr t, boolean completion) throws Z3Exception
+    public Expr eval(Expr t, boolean completion)
     {
         Native.LongPtr v = new Native.LongPtr();
         if (Native.modelEval(getContext().nCtx(), getNativeObject(),
@@ -223,7 +223,7 @@ public class Model extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr evaluate(Expr t, boolean completion) throws Z3Exception
+    public Expr evaluate(Expr t, boolean completion)
     {
         return eval(t, completion);
     }
@@ -232,7 +232,7 @@ public class Model extends Z3Object
      * The number of uninterpreted sorts that the model has an interpretation
      * for.
      **/
-    public int getNumSorts() throws Z3Exception
+    public int getNumSorts()
     {
         return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
     }
@@ -248,7 +248,7 @@ public class Model extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Sort[] getSorts() throws Z3Exception
+    public Sort[] getSorts()
     {
 
         int n = getNumSorts();
@@ -268,7 +268,7 @@ public class Model extends Z3Object
      *         of {@code s}
      * @throws Z3Exception
      **/
-    public Expr[] getSortUniverse(Sort s) throws Z3Exception
+    public Expr[] getSortUniverse(Sort s)
     {
 
         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
@@ -296,18 +296,18 @@ public class Model extends Z3Object
         }
     }
 
-    Model(Context ctx, long obj) throws Z3Exception
+    Model(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getModelDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getModelDRQ().add(o);
         super.decRef(o);

src/api/java/ParamDescrs.java

@@ -27,7 +27,7 @@ public class ParamDescrs extends Z3Object
     /**
      * validate a set of parameters.
      **/
-    public void validate(Params p) throws Z3Exception
+    public void validate(Params p)
     {
 
         Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
@@ -37,7 +37,7 @@ public class ParamDescrs extends Z3Object
     /**
      * Retrieve kind of parameter.
      **/
-    public Z3_param_kind getKind(Symbol name) throws Z3Exception
+    public Z3_param_kind getKind(Symbol name)
     {
 
         return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
@@ -49,7 +49,7 @@ public class ParamDescrs extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Symbol[] getNames() throws Z3Exception
+    public Symbol[] getNames()
     {
         int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
         Symbol[] names = new Symbol[sz];
@@ -64,7 +64,7 @@ public class ParamDescrs extends Z3Object
     /**
      * The size of the ParamDescrs.
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
     }
@@ -83,18 +83,18 @@ public class ParamDescrs extends Z3Object
         }
     }
 
-    ParamDescrs(Context ctx, long obj) throws Z3Exception
+    ParamDescrs(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getParamDescrsDRQ().add(o);
         super.decRef(o);

src/api/java/Params.java

@@ -26,7 +26,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(Symbol name, boolean value) throws Z3Exception
+    public void add(Symbol name, boolean value)
     {
         Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
                 name.getNativeObject(), (value) ? true : false);
@@ -35,7 +35,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(Symbol name, double value) throws Z3Exception
+    public void add(Symbol name, double value)
     {
         Native.paramsSetDouble(getContext().nCtx(), getNativeObject(),
                 name.getNativeObject(), value);
@@ -44,7 +44,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(Symbol name, String value) throws Z3Exception
+    public void add(Symbol name, String value)
     {
 
         Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
@@ -55,7 +55,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(Symbol name, Symbol value) throws Z3Exception
+    public void add(Symbol name, Symbol value)
     {
 
         Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
@@ -65,7 +65,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(String name, boolean value) throws Z3Exception
+    public void add(String name, boolean value)
     {
         Native.paramsSetBool(getContext().nCtx(), getNativeObject(), 
                 getContext().mkSymbol(name).getNativeObject(), value);
@@ -74,7 +74,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(String name, int value) throws Z3Exception
+    public void add(String name, int value)
     {
         Native.paramsSetUint(getContext().nCtx(), getNativeObject(), getContext()
                 .mkSymbol(name).getNativeObject(), value);
@@ -83,7 +83,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(String name, double value) throws Z3Exception
+    public void add(String name, double value)
     {
         Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), getContext()
                 .mkSymbol(name).getNativeObject(), value);
@@ -92,7 +92,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(String name, Symbol value) throws Z3Exception
+    public void add(String name, Symbol value)
     {
         Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(), getContext()
                 .mkSymbol(name).getNativeObject(), value.getNativeObject());
@@ -101,7 +101,7 @@ public class Params extends Z3Object
     /**
      * Adds a parameter setting.
      **/
-    public void add(String name, String value) throws Z3Exception
+    public void add(String name, String value)
     {
 
         Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
@@ -123,18 +123,18 @@ public class Params extends Z3Object
         }
     }
 
-    Params(Context ctx) throws Z3Exception
+    Params(Context ctx)
     {
         super(ctx, Native.mkParams(ctx.nCtx()));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getParamsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getParamsDRQ().add(o);
         super.decRef(o);

src/api/java/Pattern.java

@@ -26,7 +26,7 @@ public class Pattern extends AST
     /**
      * The number of terms in the pattern.
      **/
-    public int getNumTerms() throws Z3Exception
+    public int getNumTerms()
     {
         return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject());
     }
@@ -36,7 +36,7 @@ public class Pattern extends AST
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getTerms() throws Z3Exception
+    public Expr[] getTerms()
     {
 
         int n = getNumTerms();
@@ -61,7 +61,7 @@ public class Pattern extends AST
         }
     }
 
-    Pattern(Context ctx, long obj) throws Z3Exception
+    Pattern(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/Probe.java

@@ -34,30 +34,30 @@ public class Probe extends Z3Object
      *         0.0 for false, and a value different from 0.0 for true.
      * @throws Z3Exception 
      **/
-    public double apply(Goal g) throws Z3Exception
+    public double apply(Goal g)
     {
         getContext().checkContextMatch(g);
         return Native.probeApply(getContext().nCtx(), getNativeObject(),
                 g.getNativeObject());
     }
 
-    Probe(Context ctx, long obj) throws Z3Exception
+    Probe(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    Probe(Context ctx, String name) throws Z3Exception
+    Probe(Context ctx, String name)
     {
         super(ctx, Native.mkProbe(ctx.nCtx(), name));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getProbeDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getProbeDRQ().add(o);
         super.decRef(o);

src/api/java/Quantifier.java

@@ -27,7 +27,7 @@ public class Quantifier extends BoolExpr
     /**
      * Indicates whether the quantifier is universal.
      **/
-    public boolean isUniversal() throws Z3Exception
+    public boolean isUniversal()
     {
         return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
     }
@@ -35,7 +35,7 @@ public class Quantifier extends BoolExpr
     /**
      * Indicates whether the quantifier is existential.
      **/
-    public boolean isExistential() throws Z3Exception
+    public boolean isExistential()
     {
         return !isUniversal();
     }
@@ -43,7 +43,7 @@ public class Quantifier extends BoolExpr
     /**
      * The weight of the quantifier.
      **/
-    public int getWeight() throws Z3Exception
+    public int getWeight()
     {
         return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
     }
@@ -51,7 +51,7 @@ public class Quantifier extends BoolExpr
     /**
      * The number of patterns.
      **/
-    public int getNumPatterns() throws Z3Exception
+    public int getNumPatterns()
     {
         return Native
                 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
@@ -62,7 +62,7 @@ public class Quantifier extends BoolExpr
      * 
      * @throws Z3Exception
      **/
-    public Pattern[] getPatterns() throws Z3Exception
+    public Pattern[] getPatterns()
     {
         int n = getNumPatterns();
         Pattern[] res = new Pattern[n];
@@ -75,7 +75,7 @@ public class Quantifier extends BoolExpr
     /**
      * The number of no-patterns.
      **/
-    public int getNumNoPatterns() throws Z3Exception
+    public int getNumNoPatterns()
     {
         return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
                 getNativeObject());
@@ -86,7 +86,7 @@ public class Quantifier extends BoolExpr
      * 
      * @throws Z3Exception
      **/
-    public Pattern[] getNoPatterns() throws Z3Exception
+    public Pattern[] getNoPatterns()
     {
         int n = getNumNoPatterns();
         Pattern[] res = new Pattern[n];
@@ -99,7 +99,7 @@ public class Quantifier extends BoolExpr
     /**
      * The number of bound variables.
      **/
-    public int getNumBound() throws Z3Exception
+    public int getNumBound()
     {
         return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
     }
@@ -109,7 +109,7 @@ public class Quantifier extends BoolExpr
      * 
      * @throws Z3Exception
      **/
-    public Symbol[] getBoundVariableNames() throws Z3Exception
+    public Symbol[] getBoundVariableNames()
     {
         int n = getNumBound();
         Symbol[] res = new Symbol[n];
@@ -124,7 +124,7 @@ public class Quantifier extends BoolExpr
      * 
      * @throws Z3Exception
      **/
-    public Sort[] getBoundVariableSorts() throws Z3Exception
+    public Sort[] getBoundVariableSorts()
     {
         int n = getNumBound();
         Sort[] res = new Sort[n];
@@ -139,7 +139,7 @@ public class Quantifier extends BoolExpr
      * 
      * @throws Z3Exception
      **/
-    public BoolExpr getBody() throws Z3Exception
+    public BoolExpr getBody()
     {
         return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
                 .nCtx(), getNativeObject()));
@@ -147,7 +147,7 @@ public class Quantifier extends BoolExpr
 
     Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
             Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID) throws Z3Exception
+            Symbol quantifierID, Symbol skolemID)
     {
         super(ctx, 0);
 
@@ -183,7 +183,7 @@ public class Quantifier extends BoolExpr
 
     Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
             int weight, Pattern[] patterns, Expr[] noPatterns,
-            Symbol quantifierID, Symbol skolemID) throws Z3Exception
+            Symbol quantifierID, Symbol skolemID)
     {
         super(ctx, 0);
 
@@ -210,12 +210,12 @@ public class Quantifier extends BoolExpr
         }
     }
 
-    Quantifier(Context ctx, long obj) throws Z3Exception
+    Quantifier(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
                 .toInt())

src/api/java/RatNum.java

@@ -27,7 +27,7 @@ public class RatNum extends RealExpr
     /**
      * The numerator of a rational numeral.
      **/
-    public IntNum getNumerator() throws Z3Exception
+    public IntNum getNumerator()
     {
         return new IntNum(getContext(), Native.getNumerator(getContext().nCtx(),
                 getNativeObject()));
@@ -36,7 +36,7 @@ public class RatNum extends RealExpr
     /**
      * The denominator of a rational numeral.
      **/
-    public IntNum getDenominator() throws Z3Exception
+    public IntNum getDenominator()
     {
         return new IntNum(getContext(), Native.getDenominator(getContext().nCtx(),
                 getNativeObject()));
@@ -45,7 +45,7 @@ public class RatNum extends RealExpr
     /**
      * Converts the numerator of the rational to a BigInteger
      **/
-    public BigInteger getBigIntNumerator() throws Z3Exception
+    public BigInteger getBigIntNumerator()
     {
         IntNum n = getNumerator();
         return new BigInteger(n.toString());
@@ -54,7 +54,7 @@ public class RatNum extends RealExpr
     /**
      * Converts the denominator of the rational to a BigInteger
      **/
-    public BigInteger getBigIntDenominator() throws Z3Exception
+    public BigInteger getBigIntDenominator()
     {
         IntNum n = getDenominator();
         return new BigInteger(n.toString());
@@ -65,7 +65,7 @@ public class RatNum extends RealExpr
      * Remarks: The result
      * has at most {@code precision} decimal places.
      **/
-    public String toDecimalString(int precision) throws Z3Exception
+    public String toDecimalString(int precision)
     {
         return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
                 precision);
@@ -85,7 +85,7 @@ public class RatNum extends RealExpr
         }
     }
 
-    RatNum(Context ctx, long obj) throws Z3Exception
+    RatNum(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/RealExpr.java

@@ -25,7 +25,7 @@ public class RealExpr extends ArithExpr
     /**
      * Constructor for RealExpr
      **/
-    RealExpr(Context ctx, long obj) throws Z3Exception
+    RealExpr(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/RealSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
  **/
 public class RealSort extends ArithSort
 {
-    RealSort(Context ctx, long obj) throws Z3Exception
+    RealSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    RealSort(Context ctx) throws Z3Exception
+    RealSort(Context ctx)
     {
         super(ctx, Native.mkRealSort(ctx.nCtx()));
     }

src/api/java/RelationSort.java

@@ -25,7 +25,7 @@ public class RelationSort extends Sort
     /**
      * The arity of the relation sort.
      **/
-    public int getArity() throws Z3Exception
+    public int getArity()
     {
         return Native.getRelationArity(getContext().nCtx(), getNativeObject());
     }
@@ -34,7 +34,7 @@ public class RelationSort extends Sort
      * The sorts of the columns of the relation sort.
      * @throws Z3Exception 
      **/
-    public Sort[] getColumnSorts() throws Z3Exception
+    public Sort[] getColumnSorts()
     {
 
         if (m_columnSorts != null)
@@ -50,7 +50,7 @@ public class RelationSort extends Sort
 
     private Sort[] m_columnSorts = null;
 
-    RelationSort(Context ctx, long obj) throws Z3Exception
+    RelationSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/java/SetSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
  **/
 public class SetSort extends Sort
 {
-    SetSort(Context ctx, long obj) throws Z3Exception
+    SetSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    SetSort(Context ctx, Sort ty) throws Z3Exception
+    SetSort(Context ctx, Sort ty)
     {
         super(ctx, Native.mkSetSort(ctx.nCtx(), ty.getNativeObject()));
     }

src/api/java/Solver.java

@@ -27,7 +27,7 @@ public class Solver extends Z3Object
     /**
      * A string that describes all available solver parameters.
      **/
-    public String getHelp() throws Z3Exception
+    public String getHelp()
     {
         return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
     }
@@ -37,7 +37,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void setParameters(Params value) throws Z3Exception
+    public void setParameters(Params value)
     {
         getContext().checkContextMatch(value);
         Native.solverSetParams(getContext().nCtx(), getNativeObject(),
@@ -49,7 +49,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ParamDescrs getParameterDescriptions() throws Z3Exception
+    public ParamDescrs getParameterDescriptions()
     {
         return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
                 getContext().nCtx(), getNativeObject()));
@@ -60,7 +60,7 @@ public class Solver extends Z3Object
      * @see pop 
      * @see push
      **/
-    public int getNumScopes() throws Z3Exception
+    public int getNumScopes()
     {
         return Native
                 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
@@ -70,7 +70,7 @@ public class Solver extends Z3Object
      * Creates a backtracking point. 
      * @see pop
      **/
-    public void push() throws Z3Exception
+    public void push()
     {
         Native.solverPush(getContext().nCtx(), getNativeObject());
     }
@@ -79,7 +79,7 @@ public class Solver extends Z3Object
      * Backtracks one backtracking point.
      * Remarks: .
      **/
-    public void pop() throws Z3Exception
+    public void pop()
     {
         pop(1);
     }
@@ -91,7 +91,7 @@ public class Solver extends Z3Object
      * {@code NumScopes} 
      * @see push
      **/
-    public void pop(int n) throws Z3Exception
+    public void pop(int n)
     {
         Native.solverPop(getContext().nCtx(), getNativeObject(), n);
     }
@@ -101,7 +101,7 @@ public class Solver extends Z3Object
      * Remarks: This removes all assertions from the
      * solver.
      **/
-    public void reset() throws Z3Exception
+    public void reset()
     {
         Native.solverReset(getContext().nCtx(), getNativeObject());
     }
@@ -111,7 +111,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public void add(BoolExpr... constraints) throws Z3Exception
+    public void add(BoolExpr... constraints)
     {
         getContext().checkContextMatch(constraints);
         for (BoolExpr a : constraints)
@@ -135,7 +135,7 @@ public class Solver extends Z3Object
      * and the Boolean literals
      * provided using <see cref="Check"/> with assumptions.
      **/
-    public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
+    public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
     {
         getContext().checkContextMatch(constraints);
         getContext().checkContextMatch(ps);
@@ -160,7 +160,7 @@ public class Solver extends Z3Object
      * and the Boolean literals
      * provided using <see cref="Check"/> with assumptions.
      */ 
-    public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception
+    public void assertAndTrack(BoolExpr constraint, BoolExpr p)
     {
         getContext().checkContextMatch(constraint);
         getContext().checkContextMatch(p);
@@ -174,7 +174,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public int getNumAssertions() throws Z3Exception
+    public int getNumAssertions()
     {
         ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
@@ -186,7 +186,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public BoolExpr[] getAssertions() throws Z3Exception
+    public BoolExpr[] getAssertions()
     {
         ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
@@ -204,7 +204,7 @@ public class Solver extends Z3Object
      * @see getUnsatCore
      * @see getProof 
      **/
-    public Status check(Expr... assumptions) throws Z3Exception
+    public Status check(Expr... assumptions)
     {
         Z3_lbool r;
         if (assumptions == null)
@@ -232,7 +232,7 @@ public class Solver extends Z3Object
      * @see getUnsatCore
      * @see getProof 
      **/
-    public Status check() throws Z3Exception
+    public Status check()
     {
         return check((Expr[]) null);
     }
@@ -246,7 +246,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Model getModel() throws Z3Exception
+    public Model getModel()
     {
         long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
         if (x == 0)
@@ -264,7 +264,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr getProof() throws Z3Exception
+    public Expr getProof()
     {
         long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
         if (x == 0)
@@ -282,7 +282,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getUnsatCore() throws Z3Exception
+    public Expr[] getUnsatCore()
     {
 
         ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
@@ -298,7 +298,7 @@ public class Solver extends Z3Object
      * A brief justification of why the last call to {@code Check} returned
      * {@code UNKNOWN}.
      **/
-    public String getReasonUnknown() throws Z3Exception
+    public String getReasonUnknown()
     {
         return Native.solverGetReasonUnknown(getContext().nCtx(),
                 getNativeObject());
@@ -309,7 +309,7 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Statistics getStatistics() throws Z3Exception
+    public Statistics getStatistics()
     {
         return new Statistics(getContext(), Native.solverGetStatistics(
                 getContext().nCtx(), getNativeObject()));
@@ -330,18 +330,18 @@ public class Solver extends Z3Object
         }
     }
 
-    Solver(Context ctx, long obj) throws Z3Exception
+    Solver(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getSolverDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getSolverDRQ().add(o);
         super.decRef(o);

src/api/java/Sort.java

@@ -58,7 +58,7 @@ public class Sort extends AST
     /**
      * Returns a unique identifier for the sort.
      **/
-    public int getId() throws Z3Exception
+    public int getId()
     {
         return Native.getSortId(getContext().nCtx(), getNativeObject());
     }
@@ -66,7 +66,7 @@ public class Sort extends AST
     /**
      * The kind of the sort.
      **/
-    public Z3_sort_kind getSortKind() throws Z3Exception
+    public Z3_sort_kind getSortKind()
     {
         return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
                 getNativeObject()));
@@ -75,7 +75,7 @@ public class Sort extends AST
     /**
      * The name of the sort
      **/
-    public Symbol getName() throws Z3Exception
+    public Symbol getName()
     {
         return Symbol.create(getContext(),
                 Native.getSortName(getContext().nCtx(), getNativeObject()));
@@ -98,12 +98,12 @@ public class Sort extends AST
     /**
      * Sort constructor
      **/
-    Sort(Context ctx, long obj) throws Z3Exception
+    Sort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
                 .toInt())
@@ -111,7 +111,7 @@ public class Sort extends AST
         super.checkNativeObject(obj);
     }
 
-    static Sort create(Context ctx, long obj) throws Z3Exception
+    static Sort create(Context ctx, long obj)
     {
         Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
         switch (sk)

src/api/java/Statistics.java

@@ -70,7 +70,7 @@ public class Statistics extends Z3Object
          * 
          * @throws Z3Exception
          **/
-        public String getValueString() throws Z3Exception
+        public String getValueString()
         {
             if (isUInt())
                 return Integer.toString(m_int);
@@ -131,7 +131,7 @@ public class Statistics extends Z3Object
     /**
      * The number of statistical data.
      **/
-    public int size() throws Z3Exception
+    public int size()
     {
         return Native.statsSize(getContext().nCtx(), getNativeObject());
     }
@@ -141,7 +141,7 @@ public class Statistics extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Entry[] getEntries() throws Z3Exception
+    public Entry[] getEntries()
     {
 
         int n = size();
@@ -166,7 +166,7 @@ public class Statistics extends Z3Object
     /**
      * The statistical counters.
      **/
-    public String[] getKeys() throws Z3Exception
+    public String[] getKeys()
     {
         int n = size();
         String[] res = new String[n];
@@ -182,7 +182,7 @@ public class Statistics extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Entry get(String key) throws Z3Exception
+    public Entry get(String key)
     {
         int n = size();
         Entry[] es = getEntries();
@@ -192,18 +192,18 @@ public class Statistics extends Z3Object
         return null;
     }
 
-    Statistics(Context ctx, long obj) throws Z3Exception
+    Statistics(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getStatisticsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getStatisticsDRQ().add(o);
         super.decRef(o);

src/api/java/StringSymbol.java

@@ -29,22 +29,22 @@ public class StringSymbol extends Symbol
      * Remarks: Throws an exception if the
      * symbol is not of string kind.
      **/
-    public String getString() throws Z3Exception
+    public String getString()
     {
         return Native.getSymbolString(getContext().nCtx(), getNativeObject());
     }
 
-    StringSymbol(Context ctx, long obj) throws Z3Exception
+    StringSymbol(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    StringSymbol(Context ctx, String s) throws Z3Exception
+    StringSymbol(Context ctx, String s)
     {
         super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
         if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
                 .toInt())

src/api/java/Symbol.java

@@ -27,7 +27,7 @@ public class Symbol extends Z3Object
     /**
      * The kind of the symbol (int or string)
      **/
-    protected Z3_symbol_kind getKind() throws Z3Exception
+    protected Z3_symbol_kind getKind()
     {
         return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
                 getNativeObject()));
@@ -36,7 +36,7 @@ public class Symbol extends Z3Object
     /**
      * Indicates whether the symbol is of Int kind
      **/
-    public boolean isIntSymbol() throws Z3Exception
+    public boolean isIntSymbol()
     {
         return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL;
     }
@@ -44,7 +44,7 @@ public class Symbol extends Z3Object
     /**
      * Indicates whether the symbol is of string kind.
      **/
-    public boolean isStringSymbol() throws Z3Exception
+    public boolean isStringSymbol()
     {
         return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
     }
@@ -72,12 +72,12 @@ public class Symbol extends Z3Object
     /**
      * Symbol constructor
      **/
-    protected Symbol(Context ctx, long obj) throws Z3Exception
+    protected Symbol(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    static Symbol create(Context ctx, long obj) throws Z3Exception
+    static Symbol create(Context ctx, long obj)
     {
         switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
         {

src/api/java/Tactic.java

@@ -29,7 +29,7 @@ public class Tactic extends Z3Object
     /**
      * A string containing a description of parameters accepted by the tactic.
      **/
-    public String getHelp() throws Z3Exception
+    public String getHelp()
     {
         return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
     }
@@ -38,7 +38,7 @@ public class Tactic extends Z3Object
      * Retrieves parameter descriptions for Tactics.
      * @throws Z3Exception 
      **/
-    public ParamDescrs getParameterDescriptions() throws Z3Exception
+    public ParamDescrs getParameterDescriptions()
     {
         return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
                 .nCtx(), getNativeObject()));
@@ -48,7 +48,7 @@ public class Tactic extends Z3Object
      * Execute the tactic over the goal.
      * @throws Z3Exception 
      **/
-    public ApplyResult apply(Goal g) throws Z3Exception
+    public ApplyResult apply(Goal g)
     {    
         return apply(g, null);
     }
@@ -57,7 +57,7 @@ public class Tactic extends Z3Object
      * Execute the tactic over the goal.
      * @throws Z3Exception 
      **/
-    public ApplyResult apply(Goal g, Params p) throws Z3Exception
+    public ApplyResult apply(Goal g, Params p)
     {
         getContext().checkContextMatch(g);
         if (p == null)
@@ -77,28 +77,28 @@ public class Tactic extends Z3Object
      * @see Context#mkSolver(Tactic)
      * @throws Z3Exception 
      **/
-    public Solver getSolver() throws Z3Exception
+    public Solver getSolver()
     {
         return getContext().mkSolver(this);
     }
 
-    Tactic(Context ctx, long obj) throws Z3Exception
+    Tactic(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    Tactic(Context ctx, String name) throws Z3Exception
+    Tactic(Context ctx, String name)
     {
         super(ctx, Native.mkTactic(ctx.nCtx(), name));
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
         getContext().getTacticDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
         getContext().getTacticDRQ().add(o);
         super.decRef(o);

src/api/java/TupleSort.java

@@ -26,7 +26,7 @@ public class TupleSort extends Sort
      * The constructor function of the tuple.
      * @throws Z3Exception 
      **/
-    public FuncDecl mkDecl() throws Z3Exception
+    public FuncDecl mkDecl()
     {
 
         return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext()
@@ -36,7 +36,7 @@ public class TupleSort extends Sort
     /**
      * The number of fields in the tuple.
      **/
-    public int getNumFields() throws Z3Exception
+    public int getNumFields()
     {
         return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
     }
@@ -45,7 +45,7 @@ public class TupleSort extends Sort
      * The field declarations.
      * @throws Z3Exception 
      **/
-    public FuncDecl[] getFieldDecls() throws Z3Exception
+    public FuncDecl[] getFieldDecls()
     {
 
         int n = getNumFields();
@@ -57,7 +57,7 @@ public class TupleSort extends Sort
     }
 
     TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames,
-            Sort[] fieldSorts) throws Z3Exception
+            Sort[] fieldSorts)
     {
         super(ctx, 0);
 

src/api/java/UninterpretedSort.java

@@ -22,12 +22,12 @@ package com.microsoft.z3;
  **/
 public class UninterpretedSort extends Sort
 {
-    UninterpretedSort(Context ctx, long obj) throws Z3Exception
+    UninterpretedSort(Context ctx, long obj)
     {
         super(ctx, obj);
     }
 
-    UninterpretedSort(Context ctx, Symbol s) throws Z3Exception
+    UninterpretedSort(Context ctx, Symbol s)
     {
         super(ctx, Native.mkUninterpretedSort(ctx.nCtx(), s.getNativeObject()));
     }

src/api/java/Z3Exception.java

@@ -22,7 +22,7 @@ package com.microsoft.z3;
  * The exception base class for error reporting from Z3
  **/
 @SuppressWarnings("serial")
-public class Z3Exception extends Exception
+public class Z3Exception extends RuntimeException
 {
     /**
      * Constructor.

src/api/java/Z3Object.java

@@ -26,7 +26,7 @@ public class Z3Object extends IDisposable
     /**
      * Finalizer.
      **/
-    protected void finalize() throws Z3Exception
+    protected void finalize()
     {
         dispose();
     }
@@ -34,7 +34,7 @@ public class Z3Object extends IDisposable
     /**
      * Disposes of the underlying native Z3 object.
      **/
-    public void dispose() throws Z3Exception
+    public void dispose()
     {
         if (m_n_obj != 0)
         {
@@ -58,7 +58,7 @@ public class Z3Object extends IDisposable
         m_ctx = ctx;
     }
 
-    Z3Object(Context ctx, long obj) throws Z3Exception
+    Z3Object(Context ctx, long obj)
     {
         ctx.m_refCount++;
         m_ctx = ctx;
@@ -66,15 +66,15 @@ public class Z3Object extends IDisposable
         m_n_obj = obj;
     }
 
-    void incRef(long o) throws Z3Exception
+    void incRef(long o)
     {
     }
 
-    void decRef(long o) throws Z3Exception
+    void decRef(long o)
     {
     }
 
-    void checkNativeObject(long obj) throws Z3Exception
+    void checkNativeObject(long obj)
     {
     }
 
@@ -83,7 +83,7 @@ public class Z3Object extends IDisposable
         return m_n_obj;
     }
 
-    void setNativeObject(long value) throws Z3Exception
+    void setNativeObject(long value)
     {
         if (value != 0)
         {

src/ast/fpa/fpa2bv_converter.cpp

@@ -1881,8 +1881,8 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     else if (num == 2 &&
              m_bv_util.is_bv(args[0]) &&
              m_bv_util.get_bv_size(args[0]) == 3 &&
-             m_arith_util.is_int(args[1]) || 
+             (m_arith_util.is_int(args[1]) || 
-             m_arith_util.is_real(args[1])) {
+              m_arith_util.is_real(args[1]))) {
         // rm + real -> float
         mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
     }

src/ast/used_vars.cpp

@@ -107,7 +107,7 @@ unsigned used_vars::get_num_vars() const {
     unsigned num = m_found_vars.size();
     for (unsigned i = 0; i < num; i++) {
         if (m_found_vars[i])
-            return r++;
+            r++;
     }
     return r;
 }

src/interp/iz3mgr.h

@@ -23,6 +23,8 @@ Revision History:
 
 #include <assert.h>
 #include <vector>
+#include <functional>
+
 #include "iz3hash.h"
 
 #include"well_sorted.h"

src/smt/asserted_formulas.cpp

@@ -603,11 +603,11 @@ void asserted_formulas::propagate_values() {
     proof_ref_vector new_prs1(m_manager);
     expr_ref_vector  new_exprs2(m_manager);
     proof_ref_vector new_prs2(m_manager);
-    unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
-    for (; i < sz; i++) {
+    for (unsigned i = 0; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
+        TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
         if (m_manager.is_eq(n)) {
             expr * lhs = to_app(n)->get_arg(0);
             expr * rhs = to_app(n)->get_arg(1);
@@ -615,9 +615,11 @@ void asserted_formulas::propagate_values() {
                 if (m_manager.is_value(lhs))
                     std::swap(lhs, rhs);
                 if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
+                    if (i >= m_asserted_qhead) {
                         new_exprs1.push_back(n);
                         if (m_manager.proofs_enabled())
                             new_prs1.push_back(pr);
+                    }
                     TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";);
                     m_simplifier.cache_result(lhs, rhs, pr);
                     found = true;
@@ -625,10 +627,12 @@ void asserted_formulas::propagate_values() {
                 }
             }
         }
+        if (i >= m_asserted_qhead) {
             new_exprs2.push_back(n);
             if (m_manager.proofs_enabled())
                 new_prs2.push_back(pr);
         }
+    }
     TRACE("propagate_values", tout << "found: " << found << "\n";);
     // If C is not empty, then reduce R using the updated simplifier cache with entries
     // x -> n for each constraint 'x = n' in C.