Fix massive memory leak

Author: GUIpsp

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -20,13 +20,16 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c)
 
         try {
             Expression exp = toVerify.getExpression();
-            TranslatorToZ3 tz3 = new TranslatorToZ3(c);
-            // com.microsoft.z3.Expr
-            Expr<?> e = exp.eval(tz3);
-            Status s = tz3.verifyExpression(e);
-            if (s.equals(Status.SATISFIABLE)) {
-                // System.out.println("result of SMT: Not Ok!");
-                throw new TypeCheckError(subRef + " not a subtype of " + supRef);
+            Status s;
+            try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) {
+                // com.microsoft.z3.Expr
+                Expr<?> e = exp.eval(tz3);
+                s = tz3.verifyExpression(e);
+
+                if (s.equals(Status.SATISFIABLE)) {
+                    // System.out.println("result of SMT: Not Ok!");
+                    throw new TypeCheckError(subRef + " not a subtype of " + supRef);
+                }
             }
             // System.out.println("result of SMT: Ok!");
 

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -21,7 +21,7 @@
 
 import liquidjava.processor.context.AliasWrapper;
 
-public class TranslatorToZ3 {
+public class TranslatorToZ3 implements AutoCloseable {
 
     private com.microsoft.z3.Context z3 = new com.microsoft.z3.Context();
     private Map<String, Expr<?>> varTranslation = new HashMap<>();
@@ -37,7 +37,6 @@ public TranslatorToZ3(liquidjava.processor.context.Context c) {
         TranslatorContextToZ3.addGhostStates(z3, c.getGhostState(), funcTranslation);
     }
 
-    @SuppressWarnings("unchecked")
     public Status verifyExpression(Expr<?> e) throws Exception {
         Solver s = z3.mkSolver();
         // s.add((BoolExpr) e.eval(this));
@@ -266,4 +265,9 @@ public Expr<?> makeIte(Expr<?> c, Expr<?> t, Expr<?> e) {
             return z3.mkITE((BoolExpr) c, t, e);
         throw new RuntimeException("Condition is not a boolean expression");
     }
+
+    @Override
+    public void close() throws Exception {
+        z3.close();
+    }
 }