From 983fe528f1f05c686e7bc246e84a443f5ea6bbd0 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Thu, 28 Dec 2023 21:48:00 +0100
Subject: [PATCH] Added Java test case for JavaSMT bug
 https://github.com/sosy-lab/java-smt/issues/347

---
 test/unit/api/java/CMakeLists.txt     |  2 +
 test/unit/api/java/JavaSmtBug437.java | 58 +++++++++++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 test/unit/api/java/JavaSmtBug437.java

diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
index ebe7fa7e6c9..fcb499a0567 100644
--- a/test/unit/api/java/CMakeLists.txt
+++ b/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)
diff --git a/test/unit/api/java/JavaSmtBug437.java b/test/unit/api/java/JavaSmtBug437.java
new file mode 100644
index 00000000000..246802f2b5c
--- /dev/null
+++ b/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();
+    }
+  }
+}