diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-07 19:01:09 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-07 19:01:09 -0700 |
commit | 3850de76b8d17cc3ce88d910323ce7ee916b1fcc (patch) | |
tree | 7a59e164acbf4e8d20b1339d703b6632a936bb7b /Test | |
parent | 967acc643c247cd649d665f9b879e67e9773b44e (diff) | |
parent | 85a65323bda16d372a9e163dc4225e5d5535d14c (diff) |
Merge
Diffstat (limited to 'Test')
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 7 |
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..];
}
}
|