Added Java test case for JavaSMT bug sosy-lab/java-smt#347

test/unit/api/java/CMakeLists.txt

@@ -36,6 +36,7 @@ set(java_test_src_files
   ${CMAKE_CURRENT_SOURCE_DIR}/SynthResultTest.java
   ${CMAKE_CURRENT_SOURCE_DIR}/TermTest.java
   ${CMAKE_CURRENT_SOURCE_DIR}/ProofTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/JavaSmtBug437.java
 )
 
 # build junit tests
@@ -82,5 +83,6 @@ cvc5_add_java_api_test(SymbolManagerTest)
 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_unit_test_white(UncoveredTest api/java)

test/unit/api/java/JavaSmtBug437.java

@@ -0,0 +1,58 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for JavaSMT bug #347
+ * https://github.com/sosy-lab/java-smt/issues/347
+ */
+
+package tests;
+
+import io.github.cvc5.*;
+import org.junit.jupiter.api.Test;
+
+class JavaSmtBug437 {
+  private class Task extends Thread {
+    @Override
+    public void run() {
+      try {
+        Solver solver = new Solver();
+        Term formula = solver.mkBoolean(false);
+
+        solver.push();
+        solver.assertFormula(formula);
+
+        assert !solver.checkSat().isSat();
+
+        solver.deletePointer(); // Remove this line to fix
+
+      } catch (CVC5ApiException pE) {
+        throw new RuntimeException(pE);
+      }
+    }
+  }
+
+  @Test
+  public void bug347BrokenTest() throws InterruptedException {
+    for (int k = 0; k < 100; k++) {
+      System.out.println(k);
+
+      Task t1 = new Task();
+      t1.start();
+
+      Task t2 = new Task();
+      t2.start();
+
+      t1.join();
+      t2.join();
+    }
+  }
+}