diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index b743f74fcf..46c515b731 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -555,6 +555,12 @@ public Void visitAtom(BooleanFormula pAtom, FunctionDeclaration @Test public void testBoolVariableDump() { + // FIXME: Broken on yices2 + // Yices does not quote symbols when dumping a formula, f.ex for the variable "(" we get + // (declare-fun |(| () Bool) + // (assert () + // which is not a valid SMTLIB script. + assume().that(solverToUse()).isNotEqualTo(Solvers.YICES2); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) { @@ -566,6 +572,7 @@ public void testBoolVariableDump() { @Test public void testEqBoolVariableDump() { + // FIXME: Rewrite test? Most solvers will simplify the formula to `true`. for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) {