(Java) Added test cases for sosy-lab/java-smt#310

test/unit/api/java/CMakeLists.txt

@@ -37,6 +37,9 @@ set(java_test_src_files
   ${CMAKE_CURRENT_SOURCE_DIR}/TermTest.java
   ${CMAKE_CURRENT_SOURCE_DIR}/ProofTest.java
   ${CMAKE_CURRENT_SOURCE_DIR}/JavaSmtBug437.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/JavaSmtParallelBug1.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/JavaSmtParallelBug2.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/JavaSmtParallelBug3.java
 )
 
 # build junit tests
@@ -59,6 +62,7 @@ macro(cvc5_add_java_api_test name)
   add_test (NAME unit/api/java/${name}
     COMMAND
       ${Java_JAVA_EXECUTABLE}
+      -ea
       -Djava.library.path=${CVC5_JNI_PATH}
       -jar ${JUnit_JAR}
       -cp ${JUnit_JAR}:${CVC5_JAR_PATH}:.
@@ -84,5 +88,8 @@ cvc5_add_java_api_test(SynthResultTest)
 cvc5_add_java_api_test(TermTest)
 cvc5_add_java_api_test(ProofTest)
 cvc5_add_java_api_test(JavaSmtBug437)
+cvc5_add_java_api_test(JavaSmtParallelBug1)
+cvc5_add_java_api_test(JavaSmtParallelBug2)
+cvc5_add_java_api_test(JavaSmtParallelBug3)
 
 cvc5_add_unit_test_white(UncoveredTest api/java)

test/unit/api/java/JavaSmtParallelBug1.java

@@ -0,0 +1,52 @@
+/******************************************************************************
+ * Test for JavaSMT bug #310
+ * https://github.com/sosy-lab/java-smt/issues/310
+ */
+
+package tests;
+
+import io.github.cvc5.*;
+
+import java.util.concurrent.ExecutionException;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.Future;
+
+import org.junit.jupiter.api.Test;
+
+class JavaSmtParallelBug1 {
+  @Test
+  public void javaSmtParallelBug1Broken() throws InterruptedException, ExecutionException {
+    Solver solver = new Solver();
+
+    ExecutorService exec = Executors.newSingleThreadExecutor();
+    Future<?> result =
+        exec.submit(
+            () -> {
+              // FIXME: SEGFAULT (without -ea)
+              //  Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
+              //  C  [libcvc5.so.1+0x5e44c2]  cvc5::Solver::getBooleanSort() const+0x12
+              //  Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
+              //  j  io.github.cvc5.Solver.getBooleanSort(J)J+0
+              //  j  io.github.cvc5.Solver.getBooleanSort()Lio/github/cvc5/Sort;+5
+              //  j  tests.JavaSmtParallelBug1.lambda$bug1$0(Lio/github/cvc5/Solver;)Ljava/lang/Object;+1
+
+              // FIXME: ABORT (with -ea)
+              //  Fatal failure within
+              //  static cvc5::internal::TypeNode
+              //     cvc5::internal::expr::TypeChecker::computeType(
+              //       cvc5::internal::NodeManager*,
+              //       cvc5::internal::TNode,
+              //       bool,
+              //       std::ostream*
+              //       )
+              //  at /home/daniel/workspace/cvc5/build/src/expr/type_checker.cpp:2828
+              //  Unhandled case encountered  VARIABLE
+              Sort sortBool = solver.getBooleanSort();
+              return null;
+            });
+
+    assert result.get() == null;
+    solver.deletePointer();
+  }
+}

test/unit/api/java/JavaSmtParallelBug2.java

@@ -0,0 +1,45 @@
+/******************************************************************************
+ * Test for JavaSMT bug #310
+ * https://github.com/sosy-lab/java-smt/issues/310
+ */
+
+package tests;
+
+import io.github.cvc5.*;
+
+import java.util.concurrent.ExecutionException;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.Future;
+
+import org.junit.jupiter.api.Test;
+
+class JavaSmtParallelBug2 {  
+  @Test
+  public void javaSmtParallelBug2Broken() throws InterruptedException, ExecutionException {
+    Solver solver = new Solver();
+    Term formula = solver.mkFalse();
+
+    ExecutorService executor = Executors.newSingleThreadExecutor();
+    Future<?> result =
+        executor.submit(
+            () -> {
+              Solver prover = new Solver();
+
+              // FIXME: Exception (only with -ea)
+              //  io.github.cvc5.CVC5ApiException:
+              //   Given term is not associated with the node manager of this solver
+              //  at io.github.cvc5.Solver.assertFormula(Native Method)
+              //  at io.github.cvc5.Solver.assertFormula(Solver.java:1511)
+              //  at org.sosy_lab.java_smt.solvers.cvc5.CVC5NativeAPITest
+              //  at ..here
+              prover.assertFormula(formula);
+
+              prover.deletePointer();
+              return null;
+            });
+
+    assert result.get() == null;
+    solver.deletePointer();
+  }
+}

test/unit/api/java/JavaSmtParallelBug3.java

@@ -0,0 +1,55 @@
+/******************************************************************************
+ * Test for JavaSMT bug #310
+ * https://github.com/sosy-lab/java-smt/issues/350
+ */
+
+package tests;
+
+import io.github.cvc5.*;
+
+import java.util.concurrent.ExecutionException;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.Future;
+
+import org.junit.jupiter.api.Test;
+
+class JavaSmtParallelBug3 {
+  @Test
+  public void javaSmtParallelBug3Broken() throws InterruptedException, ExecutionException {
+    Solver solver = new Solver();
+    Term varA = solver.mkConst(solver.getBooleanSort(), "a");
+
+    solver.assertFormula(varA);
+
+    ExecutorService exec = Executors.newSingleThreadExecutor();
+    Future<?> task1 =
+        exec.submit(
+            () -> {
+              // FIXME: SEGFAULT (without -ea)
+              //  Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
+              //  C  [libcvc5.so.1+0x5fb5e6]  cvc5::Solver::push(unsigned int) const+0x36
+              //  Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
+              //  j  io.github.cvc5.Solver.push(JI)V+0
+              //  j  io.github.cvc5.Solver.push(I)V+13
+              //  j  io.github.cvc5.Solver.push()V+2
+
+              // FIXME: SIGABRT (with -ea)
+              //  Fatal failure within
+              //  static cvc5::internal::TypeNode
+              //     cvc5::internal::expr::TypeChecker::computeType(
+              //       cvc5::internal::NodeManager*,
+              //       cvc5::internal::TNode,
+              //       bool,
+              //       std::ostream*
+              //       )
+              //  at /home/daniel/workspace/cvc5/build/src/expr/type_checker.cpp:2828
+              //  Unhandled case encountered  VARIABLE
+              solver.push();
+              return null;
+            });
+
+    assert task1.get() == null;
+    solver.deletePointer();
+  }
+}