From 6b120f130cb41f45151b9418a679850775a16ef7 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 26 Nov 2013 15:25:59 -0500
Subject: [PATCH] Fix Java destruction order issue; thanks to Zheng Manchun for
 reporting this bug.

---
 src/expr/expr_manager.i | 21 +++++++++++++++++++++
 src/smt/smt_engine.i    | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+)

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 8e601a396..6fb802497 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -2,6 +2,27 @@
 #include "expr/expr_manager.h"
 %}
 
+%typemap(javacode) CVC4::ExprManager %{
+  // a ref is kept here to keep Java GC from collecting the Options
+  // before the ExprManager
+  private Object options;
+%}
+%typemap(javaconstruct) ExprManager(Options options) {
+    this($imcall, true);
+    this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::ExprManager {
+    SmtEngine.dlRef(options);
+    options = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_SmtEngine(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+
 #ifdef SWIGOCAML
   /* OCaml bindings cannot deal with this degree of overloading */
   %ignore CVC4::ExprManager::mkExpr(Kind, const std::vector<Expr>&);
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index c326d95d3..5d59cae61 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -2,6 +2,46 @@
 #include "smt/smt_engine.h"
 %}
 
+%typemap(javacode) CVC4::SmtEngine %{
+  // a ref is kept here to keep Java GC from collecting the EM
+  // before the SmtEngine
+  private Object emRef;
+  static final native Object mkRef(Object obj);
+  static final native void dlRef(Object obj);
+%}
+%native (mkRef) jobject SmtEngine::mkRef(jobject);
+%native (dlRef) void SmtEngine::dlRef(jobject);
+%{
+extern "C" {
+SWIGEXPORT jobject JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) {
+  if(o == NULL) {
+    return NULL;
+  }
+  return jenv->NewGlobalRef(o);
+}
+SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) {
+  if(o != NULL) {
+    jenv->DeleteGlobalRef(o);
+  }
+}
+}
+%}
+%typemap(javaconstruct) SmtEngine(ExprManager em) {
+    this($imcall, true);
+    emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
+  }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine {
+    dlRef(emRef);
+    emRef = null;
+    if (swigCPtr != 0) {
+      if (swigCMemOwn) {
+        swigCMemOwn = false;
+        CVC4JNI.delete_SmtEngine(swigCPtr);
+      }
+      swigCPtr = 0;
+    }
+  }
+
 %ignore CVC4::SmtEngine::setLogic(const char*);
 %ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
-- 
2.30.2