1 files changed, 19 insertions, 0 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a2cfc741..01c9f1ea 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -23,4 +23,23 @@ class Node {
     tmp := new Node;
     assert tmp != this;  // was once a bug in the Dafny checker
   }
+
+  method SequenceUpdateOutOfBounds(s: seq<set<int>>, j: int) returns (t: seq<set<int>>)
+  {
+    t := s[j := {}];  // error: j is possibly out of bounds
+  }
+
+  method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)
+    requires 10 <= |s|;
+    requires 8 <= j && j < |s|;
+    ensures |t| == |s|;
+    ensures t[8] == s[8] || t[9] == s[9];
+    ensures t[j] == b;
+  {
+    if (c) {
+      t := s[j := b];
+    } else {
+      t := s[..j] + [b] + s[j+1..];
+    }
+  }
 }