diff options
-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
|