Merge pull request #522 from sosy-lab/519-cvc5-fails-while-calculating-an-interpolant-sequence

fix invalid interpolation query for CVC5.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java

@@ -105,7 +105,7 @@ public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<String>
       Collection<Term> formulasA =
           FluentIterable.from(partitions.get(i - 1))
               .transform(assertedTerms.peek()::get)
-              .append(previousItp)
+              .append(new Term[] {previousItp}) // class Term is Iterable<Term>, be careful here
               .toSet();
       Collection<Term> formulasB =
           FluentIterable.concat(partitions.subList(i, n))

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

@@ -262,11 +262,6 @@ public <T> void sequentialInterpolation() throws SolverException, InterruptedExc
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
     requireIntegers();
 
-    assume()
-        .withMessage("Solver %s runs into timeout on this test", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     int i = index.getFreshId();
 
     IntegerFormula zero = imgr.makeNumber(0);
@@ -426,11 +421,6 @@ public <T> void sequentialInterpolationWithFewPartitions()
   public <T> void sequentialBVInterpolation() throws SolverException, InterruptedException {
     requireBitvectors();
 
-    assume()
-        .withMessage("Solver %s runs into timeout on this test", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC5);
-
     InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
 
     int i = index.getFreshId();