diff options
Diffstat (limited to 'Test/dafny1/ExtensibleArray.dfy')
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index adf97863..57ac69c7 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -83,7 +83,7 @@ class ExtensibleArray<T> { modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + [t];
- decreases Contents;
+ decreases |Contents|;
{
if (length == 0 || length % 256 != 0) {
// there is room in "elements"
|