diff options
Diffstat (limited to 'Test/vacid0/LazyInitArray.dfy')
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index 6ae00e24..c5a032fe 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -89,7 +89,7 @@ class LazyInitArray<T> { {
if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
} else {
- assert n <= e[i];
+ assert n <= e[i]; // lemma
b[i] := n;
c[n] := i;
ghost var t := d[n];
|