Tiny cleanup in TriggersCollector

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);