From ccd88a63a5decf3cd35e90401435a7547ea44382 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Wed, 6 Jan 2016 11:12:33 +0100
Subject: [PATCH] No need to call "new String()"

---
 src/api/java/FuncInterp.java | 6 +++---
 src/api/java/Statistics.java | 2 +-
 src/api/java/Symbol.java     | 5 ++---
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index fb549b3f2..72f6bb25d 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -83,7 +83,7 @@ public class FuncInterp extends Z3Object
                 return res + getValue() + "]";
             } catch (Z3Exception e)
             {
-                return new String("Z3Exception: " + e.getMessage());
+                return "Z3Exception: " + e.getMessage();
             }
         }
 
@@ -105,7 +105,7 @@ public class FuncInterp extends Z3Object
             getContext().getFuncEntryDRQ().add(o);
             super.decRef(o);
         }
-    };
+    }
 
     /**
      * The number of entries in the function interpretation.
@@ -186,7 +186,7 @@ public class FuncInterp extends Z3Object
             return res;
         } catch (Z3Exception e)
         {
-            return new String("Z3Exception: " + e.getMessage());
+            return "Z3Exception: " + e.getMessage();
         }
     }
 
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index de5a52ebb..051912468 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -90,7 +90,7 @@ public class Statistics extends Z3Object
                 return Key + ": " + getValueString();
             } catch (Z3Exception e)
             {
-                return new String("Z3Exception: " + e.getMessage());
+                return "Z3Exception: " + e.getMessage();
             }
         }
 
diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java
index b90f8d915..60b60dbdf 100644
--- a/src/api/java/Symbol.java
+++ b/src/api/java/Symbol.java
@@ -72,11 +72,10 @@ public class Symbol extends Z3Object
             else if (isStringSymbol())
                 return ((StringSymbol) this).getString();
             else
-                return new String(
-                        "Z3Exception: Unknown symbol kind encountered.");
+                return "Z3Exception: Unknown symbol kind encountered.";
         } catch (Z3Exception ex)
         {
-            return new String("Z3Exception: " + ex.getMessage());
+            return "Z3Exception: " + ex.getMessage();
         }
     }