From 2d3c12716ac66caffd7144ea4fdcad87830a6d8b Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 14 Oct 2015 21:19:59 +0100
Subject: [PATCH] Bugfix for Java memory leaks.

Relates to #205 #245
---
 src/api/java/Context.java  | 35 ++++++++++++++++-------------------
 src/api/java/Z3Object.java |  3 ++-
 2 files changed, 18 insertions(+), 20 deletions(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 89adaad5d..b733df2fa 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -370,16 +370,15 @@ public class Context extends IDisposable
      * Update a datatype field at expression t with value v.
      * The function performs a record update at t. The field
      * that is passed in as argument is updated with value v,
-     * the remainig fields of t are unchanged.	
+     * the remainig fields of t are unchanged.    
      **/
     public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
-            throws Z3Exception
+        throws Z3Exception
     {
-	return Expr.create
-	    (this, 
-	     Native.datatypeUpdateField
-	     (nCtx(), field.getNativeObject(),
-	      t.getNativeObject(), v.getNativeObject()));		
+        return Expr.create (this, 
+                            Native.datatypeUpdateField
+                            (nCtx(), field.getNativeObject(),
+                             t.getNativeObject(), v.getNativeObject()));        
     }
 
 
@@ -3777,18 +3776,6 @@ public class Context extends IDisposable
     {
         try {            
             dispose();
-    
-            if (m_refCount.get() == 0)
-            {
-                try
-                {
-                    Native.delContext(m_ctx);
-                } catch (Z3Exception e)
-                {
-                    // OK.
-                }
-                m_ctx = 0;
-            } 
         }
         catch (Throwable t) {
             throw t;
@@ -3821,5 +3808,15 @@ public class Context extends IDisposable
         m_boolSort = null;
         m_intSort = null;
         m_realSort = null;
+
+        if (m_refCount.get() == 0) {
+            try {
+                Native.delContext(m_ctx);
+            } catch (Z3Exception e) {
+                // OK?
+                System.out.println("Context deletion failed; memory leak possible.");
+            }
+            m_ctx = 0;
+        }
     }
 }
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 473cb5403..574a2820c 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -53,7 +53,8 @@ public class Z3Object extends IDisposable
 
         if (m_ctx != null)
         {            
-            m_ctx.m_refCount.decrementAndGet();
+            if (m_ctx.m_refCount.decrementAndGet() == 0)
+                m_ctx.dispose();
             m_ctx = null;
         }
     }