Skip to content

Commit e960257

Browse files
Yices: Add support for distinct in the visitor
1 parent fc3de1e commit e960257

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -490,6 +490,9 @@ private <R> R visitFunctionApplication(
490490
case YICES_EQ_TERM:
491491
functionKind = FunctionDeclarationKind.EQ; // Covers all equivalences
492492
break;
493+
case YICES_DISTINCT_TERM:
494+
functionKind = FunctionDeclarationKind.DISTINCT;
495+
break;
493496
case YICES_NOT_TERM:
494497
if (isNestedExists(pF)) {
495498
int existsTerm = Iterables.getOnlyElement(getArgs(pF));

0 commit comments

Comments
 (0)