Do not needlessly catch exceptions in Java bindings

A lot of existing code in Java bindings catches exceptions just to
silence them later.

This is:
a) Unnecessary: it is OK for a function to throw a RuntimeException
without declaring it.
b) Highly unidiomatic and not recommended by Java experts (see Effective
Java and others)
c) Confusing as has the potential to hide the existing bugs and have
them resurface at the most inconvenient/unexpected moment.

src/api/java/AST.java

@@ -175,15 +175,8 @@ public class AST extends Z3Object implements Comparable<AST>
      * A string representation of the AST.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.astToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.astToString(getContext().nCtx(), getNativeObject());
     }
 
     /**

src/api/java/ASTMap.java

@@ -104,13 +104,7 @@ class ASTMap extends Z3Object
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.astMapToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.astMapToString(getContext().nCtx(), getNativeObject());
     }
 
     ASTMap(Context ctx, long obj)

src/api/java/ASTVector.java

@@ -88,15 +88,8 @@ public class ASTVector extends Z3Object
      * Retrieves a string representation of the vector.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.astVectorToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.astVectorToString(getContext().nCtx(), getNativeObject());
     }
 
     ASTVector(Context ctx, long obj)

src/api/java/ApplyResult.java

@@ -64,15 +64,8 @@ public class ApplyResult extends Z3Object
      * A string representation of the ApplyResult.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.applyResultToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.applyResultToString(getContext().nCtx(), getNativeObject());
     }
 
     ApplyResult(Context ctx, long obj)

src/api/java/BitVecNum.java

@@ -66,13 +66,7 @@ public class BitVecNum extends BitVecExpr
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 
     BitVecNum(Context ctx, long obj)

src/api/java/FPNum.java

@@ -87,13 +87,7 @@ public class FPNum extends FPExpr
      */           
     public String toString()
     {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 
 }

src/api/java/FiniteDomainNum.java

@@ -68,12 +68,6 @@ public class FiniteDomainNum extends FiniteDomainExpr
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 }

src/api/java/Fixedpoint.java

@@ -255,14 +255,8 @@ public class Fixedpoint extends Z3Object
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
+        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                     0, null);
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
     }
 
     /**

src/api/java/FuncDecl.java

@@ -47,13 +47,7 @@ public class FuncDecl extends AST
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
     }
 
     /**

src/api/java/Goal.java

@@ -211,15 +211,8 @@ public class Goal extends Z3Object
      * 
      * @return A string representation of the Goal.
      **/
-    public String toString()
-    {
-        try
-        {
-            return Native.goalToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.goalToString(getContext().nCtx(), getNativeObject());
     }
     
     /** 

src/api/java/IntNum.java

@@ -63,14 +63,7 @@ public class IntNum extends IntExpr
     /**
      * Returns a string representation of the numeral.
      **/
-    public String toString()
-    {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 }

src/api/java/Model.java

@@ -283,15 +283,8 @@ public class Model extends Z3Object
      * @return A string representation of the model.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.modelToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.modelToString(getContext().nCtx(), getNativeObject());
     }
 
     Model(Context ctx, long obj)

src/api/java/ParamDescrs.java

@@ -82,15 +82,8 @@ public class ParamDescrs extends Z3Object
      * Retrieves a string representation of the ParamDescrs.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
     }
 
     ParamDescrs(Context ctx, long obj)

src/api/java/Params.java

@@ -115,13 +115,7 @@ public class Params extends Z3Object
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.paramsToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.paramsToString(getContext().nCtx(), getNativeObject());
     }
 
     Params(Context ctx)

src/api/java/Pattern.java

@@ -53,13 +53,7 @@ public class Pattern extends AST
     @Override
     public String toString()
     {
-        try
-        {
-            return Native.patternToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.patternToString(getContext().nCtx(), getNativeObject());
     }
 
     Pattern(Context ctx, long obj)

src/api/java/RatNum.java

@@ -75,15 +75,8 @@ public class RatNum extends RealExpr
      * Returns a string representation of the numeral.
      **/
     @Override
-    public String toString()
-    {
-        try
-        {
-            return Native.getNumeralString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    public String toString() {
+        return Native.getNumeralString(getContext().nCtx(), getNativeObject());
     }
 
     RatNum(Context ctx, long obj)

src/api/java/Solver.java

@@ -323,14 +323,8 @@ public class Solver extends Z3Object
     @Override
     public String toString()
     {
-        try
-        {
-            return Native
-                    .solverToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native
+                .solverToString(getContext().nCtx(), getNativeObject());
     }
 
     Solver(Context ctx, long obj)

src/api/java/Sort.java

@@ -82,15 +82,9 @@ public class Sort extends AST
     /**
      * A string representation of the sort.
      **/
-    public String toString()
-    {
-        try
-        {
-            return Native.sortToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+    @Override
+    public String toString() {
+        return Native.sortToString(getContext().nCtx(), getNativeObject());
     }
 
     /**

src/api/java/Statistics.java

@@ -84,15 +84,9 @@ public class Statistics extends Z3Object
         /**
          * The string representation of the Entry.
          **/
-        public String toString()
-        {
-            try
-            {
-                return Key + ": " + getValueString();
-            } catch (Z3Exception e)
-            {
-                return "Z3Exception: " + e.getMessage();
-            }
+        @Override
+        public String toString() {
+            return Key + ": " + getValueString();
         }
 
         private boolean m_is_int = false;
@@ -118,15 +112,10 @@ public class Statistics extends Z3Object
     /**
      * A string representation of the statistical data.
      **/
+    @Override
     public String toString()
     {
-        try
-        {
-            return Native.statsToString(getContext().nCtx(), getNativeObject());
-        } catch (Z3Exception e)
-        {
-            return "Z3Exception: " + e.getMessage();
-        }
+        return Native.statsToString(getContext().nCtx(), getNativeObject());
     }
 
     /**