|
11 | 11 | import static com.google.common.base.Preconditions.checkArgument; |
12 | 12 | import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.EXISTS; |
13 | 13 | import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.FORALL; |
14 | | -import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq; |
15 | 14 | import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq; |
16 | 15 | import static scala.collection.JavaConverters.asJava; |
17 | 16 | import static scala.collection.JavaConverters.asJavaCollection; |
@@ -547,15 +546,19 @@ private <R> R visitQuantifier(FormulaVisitor<R> visitor, BooleanFormula f, IQuan |
547 | 546 |
|
548 | 547 | // substitute the bound variable with index 0 with a new variable, and un-shift the remaining |
549 | 548 | // de-Bruijn indices, such that the next nested bound variable has index 0. |
550 | | - IFormula substitutedBody = IFormula.subst(body, toITermSeq(substitutionVariable).toList(), -1); |
| 549 | + IFormula substitutedBody = IFormula.subst(body, asScalaList(substitutionVariable), -1); |
551 | 550 |
|
552 | 551 | return visitor.visitQuantifier( |
553 | 552 | f, |
554 | 553 | quantifier, |
555 | | - List.of(encapsulateWithTypeOf(substitutionVariable)), |
| 554 | + ImmutableList.of(encapsulateWithTypeOf(substitutionVariable)), |
556 | 555 | encapsulateBoolean(substitutedBody)); |
557 | 556 | } |
558 | 557 |
|
| 558 | + private static scala.collection.immutable.List<ITerm> asScalaList(ITerm substitutionVariable) { |
| 559 | + return scala.collection.immutable.List$.MODULE$.empty().$colon$colon(substitutionVariable); |
| 560 | + } |
| 561 | + |
559 | 562 | /** |
560 | 563 | * Get a fresh variable name for the given formula. We compute the same variable name for the same |
561 | 564 | * body, such that a user gets the same substituted body when visiting a quantified formulas |
|
0 commit comments