diff options
Diffstat (limited to 'Test/vacid0')
| -rw-r--r-- | Test/vacid0/Composite.dfy | 1 | ||||
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 2 | ||||
| -rw-r--r-- | Test/vacid0/SparseArray.dfy | 2 |
3 files changed, 2 insertions, 3 deletions
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index ca5f206b..87e63e2c 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -91,7 +91,6 @@ class Composite { var p := parent;
parent := null;
if (p != null) {
- assert (p.left == this) != (p.right == this);
if (p.left == this) {
p.left := null;
} else {
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];
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];
|