From 2efa59dea051803bc716d02070aa013397cfccc4 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/dafny0/Answer | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0/Answer')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 78982f01..e7f7c4d6 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -27,6 +27,7 @@ class MyClass<T, U> {
       var to: MyClass<T,U>;
       call to, u, v := M(true, lotsaObjects)
       call to, u, v := to.M(true, lotsaObjects)
+      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
     }
   }
 }
@@ -38,8 +39,11 @@ Dafny program verifier finished with 0 verified, 0 errors
 Boogie program verifier finished with 8 verified, 0 errors
 
 -------------------- SmallTests.dfy --------------------
+SmallTests.dfy(29,7): Error: RHS expression must be well defined
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 4 verified, 1 error
 
 -------------------- Queue.dfy --------------------
 
-- 
cgit v1.2.3