CVC5: Removed CVC5 from the blacklist in concurrent tests.

Author: daniel-raffler

Diff for: src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java

@@ -281,11 +281,6 @@ public void testFormulaTranslationWithConcurrentContexts()
   public void testIntConcurrencyWithoutConcurrentContext() throws InvalidConfigurationException {
     requireIntegers();
 
-    assume()
-        .withMessage("Solver does not support concurrency without concurrent context.")
-        .that(solver)
-        .isNotEqualTo(Solvers.CVC5);
-
     ConcurrentLinkedQueue<SolverContext> contextList = new ConcurrentLinkedQueue<>();
     // Initialize contexts before using them in the threads
     for (int i = 0; i < NUMBER_OF_THREADS; i++) {
@@ -306,11 +301,6 @@ public void testIntConcurrencyWithoutConcurrentContext() throws InvalidConfigura
   public void testBvConcurrencyWithoutConcurrentContext() throws InvalidConfigurationException {
     requireBitvectors();
 
-    assume()
-        .withMessage("Solver does not support concurrency without concurrent context.")
-        .that(solver)
-        .isNotEqualTo(Solvers.CVC5);
-
     ConcurrentLinkedQueue<SolverContext> contextList = new ConcurrentLinkedQueue<>();
     // Initialize contexts before using them in the threads
     for (int i = 0; i < NUMBER_OF_THREADS; i++) {

Diff for: src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java

@@ -42,7 +42,7 @@ public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolv
   private static final int DEFAULT_PROBLEM_SIZE = 8;
 
   private static final Collection<Solvers> SOLVERS_NOT_SUPPORTING_FORMULA_THREAD_SHARING =
-      ImmutableList.of(Solvers.CVC5);
+      ImmutableList.of(); // TODO: Remove this
 
   @Before
   public void makeThreads() {
@@ -78,7 +78,6 @@ public void allLocalTest() throws InterruptedException, SolverException {
   public void nonLocalContextTest()
       throws ExecutionException, InterruptedException, SolverException {
     requireIntegers();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
 
     // generate a new context in another thread, i.e., non-locally
     Future<SolverContext> result = executor.submit(() -> factory.generateContext());
@@ -113,7 +112,6 @@ public void nonLocalContextTest()
   public void nonLocalFormulaTest()
       throws InterruptedException, SolverException, ExecutionException {
     requireIntegers();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
 
     // generate a new formula in another thread, i.e., non-locally
     Future<BooleanFormula> result =
@@ -142,8 +140,6 @@ public void nonLocalFormulaTest()
   @Test
   public void nonLocalProverTest() throws InterruptedException, ExecutionException {
     requireIntegers();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
-
     BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE);
 
     // generate a new prover in another thread, i.e., non-locally
@@ -263,7 +259,6 @@ public <T> void localInterpolationTest() throws InterruptedException, SolverExce
   public <T> void nonLocalInterpolationTest() throws InterruptedException, ExecutionException {
     requireIntegers();
     requireInterpolation();
-    assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5);
 
     BooleanFormula f1 = imgr.lessThan(imgr.makeVariable("A"), imgr.makeVariable("B"));
     BooleanFormula f2 = imgr.lessThan(imgr.makeVariable("B"), imgr.makeVariable("A"));