Bugfix for Java memory leaks.

Relates to #205 #245

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
+        return Expr.create (this, 
-	    (this, 
+                            Native.datatypeUpdateField
-	     Native.datatypeUpdateField
+                            (nCtx(), field.getNativeObject(),
-	     (nCtx(), field.getNativeObject(),
+                             t.getNativeObject(), v.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;
+        }
     }
 }

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;
         }
     }