1 files changed, 1 insertions, 3 deletions
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];
     }
   }