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 291ac8dd6a..a5f4118f69 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -537,7 +537,6 @@ public void enumTypeTest() throws SolverException, InterruptedException { private final ExecutorService executor = Executors.newSingleThreadExecutor(); - @SuppressWarnings("unused") private long createSharedEnv(long sibling) { long cfg = msat_create_config(); @@ -569,13 +568,15 @@ public void bug339Test() throws ExecutionException, InterruptedException { long prover = createSharedEnv(this.env); msat_assert_formula(prover, formula); - Future task1 = executor.submit(() -> { - try { - assertThat(msat_check_sat(prover)).isFalse(); - } catch (InterruptedException | SolverException pE) { - throw new RuntimeException(pE); - } - }); + Future task1 = + executor.submit( + () -> { + try { + assertThat(msat_check_sat(prover)).isFalse(); + } catch (InterruptedException | SolverException pE) { + throw new RuntimeException(pE); + } + }); assert task1.get() == null; } diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java index 87f9506580..3c6f65c1f5 100644 --- a/src/org/sosy_lab/java_smt/test/Bug339Test.java +++ b/src/org/sosy_lab/java_smt/test/Bug339Test.java @@ -71,6 +71,6 @@ public void fixedTest() throws InterruptedException, ExecutionException { } }); - assert task1.get() == null; + assert task1.get() == null; } } diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 75977f01d9..9f6606dbce 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -218,36 +218,37 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation()) { T id1 = prover.push(f1); - Future task1 = executor.submit( - () -> { - try { - // FIXME: Exception for CVC5 - // java.lang.IllegalStateException: - // You tried to use push() on an CVC5 assertion stack illegally. - // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl - // (CVC5AbstractProver.java:89) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push - // (AbstractProver.java:88) - // at .. - prover.push(f2); - - // FIXME: Exception for MathSAT (bug #339) - // java.lang.StackOverflowError - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve - // (Native Method) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat - // (Mathsat5NativeApi.java:156) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat - // (Mathsat5AbstractProver.java:106) - // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable - // (ProverEnvironmentSubject.java:67) - // at .. - assertThat(prover).isUnsatisfiable(); - - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); + Future task1 = + executor.submit( + () -> { + try { + // FIXME: Exception for CVC5 + // java.lang.IllegalStateException: + // You tried to use push() on an CVC5 assertion stack illegally. + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl + // (CVC5AbstractProver.java:89) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push + // (AbstractProver.java:88) + // at .. + prover.push(f2); + + // FIXME: Exception for MathSAT (bug #339) + // java.lang.StackOverflowError + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve + // (Native Method) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat + // (Mathsat5NativeApi.java:156) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat + // (Mathsat5AbstractProver.java:106) + // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable + // (ProverEnvironmentSubject.java:67) + // at .. + assertThat(prover).isUnsatisfiable(); + + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); assert task1.get() == null; @@ -271,19 +272,20 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi executor.awaitTermination(100, TimeUnit.MILLISECONDS); prover.pop(); - Future task3 = executor.submit( - () -> { - try { - prover.pop(); + Future task3 = + executor.submit( + () -> { + try { + prover.pop(); - prover.push(itp.get()); - prover.push(f2); + prover.push(itp.get()); + prover.push(f2); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException | ExecutionException pE) { - throw new RuntimeException(pE); - } - }); + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException | ExecutionException pE) { + throw new RuntimeException(pE); + } + }); assert task3.get() == null; }