Allow display expressions as trigger terms

1 files changed, 2 insertions, 3 deletions

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 30f7b9e8..167a6a1b 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -169,7 +169,7 @@ 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 MemberSelectExpr || expr is OldExpr || expr is ApplyExpr ||

+      if (expr is FunctionCallExpr || expr is SeqSelectExpr || 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);

@@ -186,8 +186,7 @@ namespace Microsoft.Dafny.Triggers {
                  expr is OldExpr ||

                  expr is ThisExpr ||

                  expr is BoxingCastExpr ||

-                 expr is DatatypeValue ||

-                 expr is SeqDisplayExpr) { //FIXME what abvout other display expressions?

+                 expr is DatatypeValue) {

         annotation = AnnotateOther(expr, false);

       } else {

         annotation = AnnotateOther(expr, true);