Quickfix for sosy-lab/java-smt#347

src/api/java/jni/api_utilities.h

@@ -19,6 +19,7 @@
 #include <cvc5/cvc5_parser.h>
 #include <jni.h>
 
+#include <mutex>
 #include <string>
 #include <vector>
 
@@ -149,8 +150,15 @@ jobject getBooleanObject(JNIEnv* env, bool value);
  * a map from solver pointers to global references that need to be freed when
  * the java Solver.deletePointer method is called
  */
+
 inline std::map<jlong, std::vector<jobject> > globalReferences;
 
+/**
+ * a lock to protect globalReferences
+ */
+
+inline std::mutex globalLock;
+
 /**
  * @param env jni environment
  * @param solverRef a global reference to java Solver object

src/api/java/jni/solver.cpp

@@ -41,6 +41,7 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_deletePointer(JNIEnv* env,
                                                                 jobject,
                                                                 jlong pointer)
 {
+  std::lock_guard<std::mutex> guard(globalLock);
   const std::vector<jobject>& refs = globalReferences[pointer];
   for (jobject ref : refs)
   {
@@ -2437,6 +2438,7 @@ Java_io_github_cvc5_Solver_declareOracleFun(JNIEnv* env,
                                             jobject oracle)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  std::lock_guard<std::mutex> guard(globalLock);
   jobject oracleReference = env->NewGlobalRef(oracle);
   globalReferences[pointer].push_back(oracleReference);
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2446,6 +2448,13 @@ Java_io_github_cvc5_Solver_declareOracleFun(JNIEnv* env,
   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
   std::function<Term(std::vector<Term>)> fn =
       [env, oracleReference](std::vector<Term> input) {
+        // FIXME:
+        // This is likely still broken if multiple threads are
+        // used as the captured JEnv ("env") is only valid on the
+        // current thread. However, the callback might come from
+        // any thread that encouters a term for the oracle.
+        //
+        // See https://github.com/sosy-lab/java-smt/pull/345
         Term term = applyOracle(env, oracleReference, input);
         return term;
       };