Skip to content

Commit

Permalink
Remove comment about bug #339 from SolverThreadLocalityTest as the is…
Browse files Browse the repository at this point in the history
…sues has been solved.
  • Loading branch information
daniel-raffler authored and baierd committed Jan 3, 2024
1 parent 220e08a commit db0ef27
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -150,18 +150,6 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException
// (AbstractProver.java:108)
// at ..
prover.push(formula);

// 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);
Expand Down

0 comments on commit db0ef27

Please sign in to comment.