diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index c77a805de1..3997f0d108 100644 --- 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; - } }