fix test for Yices, the test was added during the last merge.
@@ -105,6 +105,14 @@ public class SolverContextTest extends SolverBasedTest0 {
.that(solverToUse())
.isNotEqualTo(Solvers.Z3);
+ // Yices2 allows simple checks (comparison against constants like TRUE/FALSE), lets abort here.
+ assume()
+ .withMessage(
+ "Solver %s does not support to access formulae after closing the context",
+ solverToUse())
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.YICES2);
+
// try to access some data about formulae and managers
assertThat(term.toString()).isEqualTo("variable");
assertThat(term.hashCode()).isEqualTo(hash);
