summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks
diff options
context:
space:
mode:
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r--Test/VSI-Benchmarks/b4.dfy4
1 files changed, 0 insertions, 4 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index f06b712c..ae5b0511 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -117,10 +117,6 @@ class Map<Key(==),Value> {
} else {
prev.next := p.next;
}
- assert Keys[..n] == old(Keys)[..n];
- assert Values[..n] == old(Values)[..n];
- assert Keys[n..] == old(Keys)[n+1..];
- assert Values[n..] == old(Values)[n+1..];
}
}