From d993cffd4d57286408ab6a9c92cc360bc7708562 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 21 May 2013 14:19:06 -0700
Subject: Updated a test to verify with Z3 4.3.0.

---
 Test/VSI-Benchmarks/b4.dfy |  4 +++-
 Test/dafny0/Answer         | 14 +++++++-------
 2 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'Test')

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
-- 
cgit v1.2.3