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 | |
parent | 45638021e2d82e5cd16621ce5a0909ba9804eeaf (diff) |
Updated a test to verify with Z3 4.3.0.
Diffstat (limited to 'Test')
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 4 | ||||
-rw-r--r-- | Test/dafny0/Answer | 14 |
2 files changed, 10 insertions, 8 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..];
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 48b242ac..fd4efae5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -180,10 +180,10 @@ Execution trace: Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
Definedness.dfy(87,10): Error: possible violation of function precondition
@@ -752,19 +752,19 @@ Execution trace: Dafny program verifier finished with 34 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+ (0,0): anon8_Else
+ (0,0): anon9_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
+ (0,0): anon8_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
|