diff options
author | wuestholz <unknown> | 2013-05-21 14:19:06 -0700 |
---|---|---|
committer | wuestholz <unknown> | 2013-05-21 14:19:06 -0700 |
commit | d993cffd4d57286408ab6a9c92cc360bc7708562 (patch) | |
tree | d8d308081cc07f46a3c6ab751da52f2269c5c991 /Test/VSI-Benchmarks | |
parent | 45638021e2d82e5cd16621ce5a0909ba9804eeaf (diff) |
Updated a test to verify with Z3 4.3.0.
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index 6830fd87..f06b712c 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -1,5 +1,5 @@ /*
- This test works with Z3 3.2 and Z3 4.1 (on Win7 x64). Other versions ... who knows.
+ This test works with Z3 4.3 (on Win8 x64). Other versions ... who knows.
*/
// Note: We are using the built-in equality to compare keys.
@@ -117,6 +117,8 @@ 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..];
}
|