summaryrefslogtreecommitdiff
path: root/Source/Dafny/Resolver.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Resolver.cs')
-rw-r--r--Source/Dafny/Resolver.cs3
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 098dbad2..5e2bc911 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3715,6 +3715,9 @@ namespace Microsoft.Dafny {
return UsesSpecFeatures(e.Seq) ||
(e.E0 != null && UsesSpecFeatures(e.E0)) ||
(e.E1 != null && UsesSpecFeatures(e.E1));
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee));
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
return UsesSpecFeatures(e.Seq) ||