diff options
Diffstat (limited to 'Dafny/Resolver.ssc')
| -rw-r--r-- | Dafny/Resolver.ssc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 8bbc1d29..d53bf450 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -343,6 +343,10 @@ namespace Microsoft.Dafny { Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type);
}
}
+ foreach (Expression e in m.Decreases) {
+ ResolveExpression(e, false);
+ // any type is fine
+ }
// Add out-parameters to the scope, but don't care about any duplication errors, since they have already been reported
foreach (Formal p in m.Outs) {
|