Skip to content

Commit a9589ec

Browse files
committed
enable disabled test for interpolation in BV theory with CVC5.
1 parent cdcc7f9 commit a9589ec

File tree

1 file changed

+0
-5
lines changed

1 file changed

+0
-5
lines changed

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -421,11 +421,6 @@ public <T> void sequentialInterpolationWithFewPartitions()
421421
public <T> void sequentialBVInterpolation() throws SolverException, InterruptedException {
422422
requireBitvectors();
423423

424-
assume()
425-
.withMessage("Solver %s runs into timeout on this test", solverToUse())
426-
.that(solverToUse())
427-
.isNotEqualTo(Solvers.CVC5);
428-
429424
InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
430425

431426
int i = index.getFreshId();

0 commit comments

Comments
 (0)