diff options
Diffstat (limited to 'Test/dafny0/ListContents.dfy')
| -rw-r--r-- | Test/dafny0/ListContents.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy index 07dc2f7e..62636ce5 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny0/ListContents.dfy @@ -75,7 +75,7 @@ class Node<T> { (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
invariant
(forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
- decreases current, |current.list|;
+ decreases if current != null then |current.list| else -1;
{
var nx := current.next;
assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
|