summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2012-09-07 17:38:30 +0200
committerGravatar wuestholz <unknown>2012-09-07 17:38:30 +0200
commit112fdef9cfa83ee669494f14230b75eacaf699af (patch)
treebd8dafa063cfed8959df51e69028be4ea0f4f61c /Test
parent4a522f9458decdf7865be79596788c50e9145faf (diff)
Dafny: Fixed a test that would fail with Z3 4.1.
Diffstat (limited to 'Test')
-rw-r--r--Test/VSI-Benchmarks/b4.dfy7
1 files changed, 3 insertions, 4 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 76e1ffa7..d5a56df4 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -1,6 +1,5 @@
/*
- This test fails with Z3 2.4 (on Win7 x64) and works
- with Z3 2.9 (on Win7 x64). Other versions ... who knows.
+ This test works with Z3 3.2 and Z3 4.1 (on Win7 x64). Other versions ... who knows.
*/
// Note: We are using the built-in equality to compare keys.
@@ -111,8 +110,6 @@ class Map<Key(==),Value> {
if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
Values := Values[..n] + Values[n+1..];
- assert Keys[n..] == old(Keys)[n+1..];
- assert Values[n..] == old(Values)[n+1..];
nodes := nodes[..n] + nodes[n+1..];
if (prev == null) {
@@ -120,6 +117,8 @@ class Map<Key(==),Value> {
} else {
prev.next := p.next;
}
+ assert Keys[n..] == old(Keys)[n+1..];
+ assert Values[n..] == old(Values)[n+1..];
}
}