diff options
Diffstat (limited to 'Test/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 1 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 2 |
2 files changed, 0 insertions, 3 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 19f54d94..bb88b265 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -94,7 +94,6 @@ class Benchmark3 { call r.Enqueue(m);
pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];
}
- assert (forall i :: 0 <= i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index fdb23379..80d6b8d6 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -105,9 +105,7 @@ class Map<Key,Value> { call p, n, prev := FindIndex(key);
if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
- assert Keys[..n] == old(Keys)[..n] && Keys[n..] == old(Keys)[n+1..];
Values := Values[..n] + Values[n+1..];
- assert Values[..n] == old(Values)[..n] && Values[n..] == old(Values)[n+1..];
nodes := nodes[..n] + nodes[n+1..];
if (prev == null) {
head := head.next;
|