From 1a0ef1ae83a88966a2d68e5eba5a70a215f28f3e Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:08:25 -0700 Subject: Allow MultiSelectExpr as quantifier heads --- Source/Dafny/Triggers/TriggersCollector.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Source/Dafny/Triggers') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 11860404..69c47d90 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -185,7 +185,8 @@ 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 || 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); -- cgit v1.2.3