From 8718c8de05f07ffbb3ccbceee550a9c88a599947 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 6 Nov 2009 23:54:22 +0000
Subject: Added a sequence update expression in Dafny.

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

(limited to 'Test/VSI-Benchmarks/b4.dfy')

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index e3a99884..3fa80b4c 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -52,10 +52,8 @@ class Map<Key,Value> {
     if (j == -1) {
       keys := keys + [key];
       values := values + [val];
-      assert values[|keys|-1] == val;  // lemma
     } else {
-      values := values[..j] + [val] + values[j+1..];
-      assert values[j] == val; //lemma
+      values := values[j := val];
     }
   }
 
-- 
cgit v1.2.3