diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index e84dc8c81..f43aa85d2 100644
--- a/src/api/java/AST.java
+++ b/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());
     }
 
     /**
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index 7bc485bf5..a6201d8a0 100644
--- a/src/api/java/ASTMap.java
+++ b/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)
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index ab99e2aee..da1ab0f12 100644
--- a/src/api/java/ASTVector.java
+++ b/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)
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index 84c63e966..f598c9504 100644
--- a/src/api/java/ApplyResult.java
+++ b/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)
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index 5a62f8087..d6c176855 100644
--- a/src/api/java/BitVecNum.java
+++ b/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)
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
index 69a44c559..9aeb41759 100644
--- a/src/api/java/FPNum.java
+++ b/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());
     }
 
 }
diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java
index e53ed22b2..68467e408 100644
--- a/src/api/java/FiniteDomainNum.java
+++ b/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());
     }
 }
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 14fb3a44a..2ff10a1f3 100644
--- a/src/api/java/Fixedpoint.java
+++ b/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();
-        }
     }
 
     /**
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 301978c44..273e853c0 100644
--- a/src/api/java/FuncDecl.java
+++ b/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());
     }
 
     /**
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index 46b04f6bf..e60971179 100644
--- a/src/api/java/Goal.java
+++ b/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());
     }
     
     /** 
diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java
index 71d878311..d3a5b456f 100644
--- a/src/api/java/IntNum.java
+++ b/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());
     }
 }
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 0695d7cf1..1bf77d246 100644
--- a/src/api/java/Model.java
+++ b/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)
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 8f8c6df0b..f265fb19e 100644
--- a/src/api/java/ParamDescrs.java
+++ b/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)
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index 25d009b12..4be36c23d 100644
--- a/src/api/java/Params.java
+++ b/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)
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index eb12b6448..852ffcd0f 100644
--- a/src/api/java/Pattern.java
+++ b/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)
diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java
index f44823a2b..2bf1b28dd 100644
--- a/src/api/java/RatNum.java
+++ b/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)
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index ea76637c8..431811b8d 100644
--- a/src/api/java/Solver.java
+++ b/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)
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index e30e0b8b3..30a43e7dd 100644
--- a/src/api/java/Sort.java
+++ b/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());
     }
 
     /**
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 5af0cf863..1e842a892 100644
--- a/src/api/java/Statistics.java
+++ b/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());
     }
 
     /**