Skip to content

Commit 1638bd4

Browse files
committed
fix invalid interpolation query for CVC5.
Since class Term implements Iterable of Terms, the append-method was iterating over the terms children, and for TRUE/FALSE, there are none. Actually a tricky, quite simple bug.
1 parent 0dbe836 commit 1638bd4

File tree

2 files changed

+1
-6
lines changed

2 files changed

+1
-6
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<String>
105105
Collection<Term> formulasA =
106106
FluentIterable.from(partitions.get(i - 1))
107107
.transform(assertedTerms.peek()::get)
108-
.append(previousItp)
108+
.append(new Term[]{previousItp}) // class Term is Iterable<Term>, be careful here
109109
.toSet();
110110
Collection<Term> formulasB =
111111
FluentIterable.concat(partitions.subList(i, n))

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -262,11 +262,6 @@ public <T> void sequentialInterpolation() throws SolverException, InterruptedExc
262262
InterpolatingProverEnvironment<T> stack = newEnvironmentForTest();
263263
requireIntegers();
264264

265-
assume()
266-
.withMessage("Solver %s runs into timeout on this test", solverToUse())
267-
.that(solverToUse())
268-
.isNotEqualTo(Solvers.CVC5);
269-
270265
int i = index.getFreshId();
271266

272267
IntegerFormula zero = imgr.makeNumber(0);

0 commit comments

Comments
 (0)