diff options
Diffstat (limited to 'Test/dafny1/ListReverse.dfy')
| -rw-r--r-- | Test/dafny1/ListReverse.dfy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy index 0837dd91..8d5a71e8 100644 --- a/Test/dafny1/ListReverse.dfy +++ b/Test/dafny1/ListReverse.dfy @@ -11,6 +11,7 @@ class Node { modifies r;
ensures reverse == null || reverse in r;
ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
+ decreases *;
{
var current := x;
reverse := null;
|