Removed native API test for bug339 as it has been fixed.

sosy-lab · Dec 19, 2023 · 36919ed · 36919ed
1 parent 80ede24
commit 36919ed
Showing 1 changed file with 0 additions and 76 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java
@@ -534,80 +534,4 @@ public void enumTypeTest() throws SolverException, InterruptedException {
     assertThat(msat_check_sat(env)).isFalse();
     msat_pop_backtrack_point(env);
   }
-
-  private final ExecutorService executor = Executors.newSingleThreadExecutor();
-
-  private long createSharedEnv(long sibling) {
-    long cfg = msat_create_config();
-    msat_set_option_checked(cfg, "dpll.ghost_filtering", "true");
-    msat_set_option_checked(cfg, "theory.la.split_rat_eq", "false");
-
-    long prover = msat_create_shared_env(cfg, sibling);
-    msat_destroy_config(cfg);
-
-    return prover;
-  }
-
-  private long makeLt(long e, long t1, long t2) {
-    return msat_make_not(e, msat_make_leq(e, t2, t1));
-  }
-
-  @SuppressWarnings("unused")
-  @Test(expected = StackOverflowError.class)
-  public void bug339BrokenTest() throws ExecutionException, InterruptedException {
-    long integerType = msat_get_integer_type(env);
-
-    long varA = msat_make_variable(env, "A", integerType);
-    long varB = msat_make_variable(env, "B", integerType);
-
-    long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA));
-    long prover = createSharedEnv(this.env);
-
-    // FIXME: Bug #339 is caused by this line. Removing it will fix the test.
-    long hook = msat_set_termination_callback(prover, () -> false);
-
-    msat_assert_formula(prover, formula);
-
-    Future<?> task1 =
-        executor.submit(
-            () -> {
-              try {
-                assertThat(msat_check_sat(prover)).isFalse();
-              } catch (InterruptedException | SolverException pE) {
-                throw new RuntimeException(pE);
-              }
-            });
-
-    assert task1.get() == null;
-  }
-
-  @SuppressWarnings("unused")
-  @Test
-  public void bug339FixedTest() throws ExecutionException, InterruptedException {
-    long integerType = msat_get_integer_type(env);
-
-    long varA = msat_make_variable(env, "A", integerType);
-    long varB = msat_make_variable(env, "B", integerType);
-
-    long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA));
-    long prover = createSharedEnv(this.env);
-
-    msat_assert_formula(prover, formula);
-
-    Future<?> task1 =
-        executor.submit(
-            () -> {
-              try {
-                // FIXME: Bug #339 is not triggered if we add the callback on the thread that
-                //  will do the calculation
-                long hook = msat_set_termination_callback(prover, () -> false);
-
-                assertThat(msat_check_sat(prover)).isFalse();
-              } catch (InterruptedException | SolverException pE) {
-                throw new RuntimeException(pE);
-              }
-            });
-
-    assert task1.get() == null;
-  }
 }