diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6688a0a4..9f3f474b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4205,6 +4205,9 @@ namespace Microsoft.Dafny { } else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
return e.Elements.Exists(ee => UsesSpecFeatures(ee));
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B));
} else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
return cce.NonNull(e.Field).IsGhost || UsesSpecFeatures(e.Obj);
|