diff options
| author |  Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
| commit | 1005adb004baf133b265eda5bfdc53022437e6ef (patch) | |
| tree | b2fd13051b5f484a79a9b2303404aafc2da5858f /Test/dafny1 | |
| parent | 967bd4d7a4223d710f8f10659cdced173b249eac (diff) | |
Fixed bug in translation of method termination checks, and also fixed a (previously undetected) specification bug in the test suite.
Diffstat (limited to 'Test/dafny1')
| -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 405f3e15..a16cf603 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 Repr;
+ decreases Contents;
{
if (length == 0 || length % 256 != 0) {
// there is room in "elements"
|