diff options
Diffstat (limited to 'Source/Dafny/Triggers')
| -rw-r--r-- | Source/Dafny/Triggers/TriggersCollector.cs | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index cc3b1978..c25f65b9 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -191,8 +191,13 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e));
TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort
- if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MultiSelectExpr || expr is MemberSelectExpr ||
- expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression ||
+ if (expr is FunctionCallExpr ||
+ expr is SeqSelectExpr ||
+ expr is MultiSelectExpr ||
+ expr is MemberSelectExpr ||
+ expr is OldExpr ||
+ expr is ApplyExpr ||
+ expr is DisplayExpression ||
(expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
(expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
annotation = AnnotatePotentialCandidate(expr);
|