From 112fdef9cfa83ee669494f14230b75eacaf699af Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 7 Sep 2012 17:38:30 +0200
Subject: Dafny: Fixed a test that would fail with Z3 4.1.

---
 Test/VSI-Benchmarks/b4.dfy | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'Test')

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