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