Skip to content

Commit

Permalink
Disable yices2 in VariableNamesTest.testBoolVariable as it does not q…
Browse files Browse the repository at this point in the history
…uote symbols correctly and returns invalid SMTLIB strings when dumping formulas.
  • Loading branch information
daniel-raffler committed Oct 9, 2024
1 parent 2aecfa0 commit fed0e55
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions src/org/sosy_lab/java_smt/test/VariableNamesTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -555,6 +555,12 @@ public Void visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula>

@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) {
Expand All @@ -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) {
Expand Down

0 comments on commit fed0e55

Please sign in to comment.