1 files changed, 23 insertions, 0 deletions
diff --git a/Test/dafny0/SeqSlice.dfy b/Test/dafny0/SeqSlice.dfy
index 381bb131..2f9c4bbd 100644
--- a/Test/dafny0/SeqSlice.dfy
+++ b/Test/dafny0/SeqSlice.dfy
@@ -25,3 +25,26 @@ method test(x:seq<int>)
     assert forall i :: 0 <= i < |e| ==> e[i] == x[i+1];
     assert forall i :: 0 <= i < |f| ==> f[i] == x[i+6];
 }
+
+newtype MyNumeric = n | 0 <= n < 100
+
+method NumericSlice<T>(x: seq<T>, two: MyNumeric) returns (y: seq<T>)
+  requires 10 <= |x| && two == 2;
+  ensures |y| == 3;
+{
+  var slices;
+  if * {
+    slices := x[0:two:3:0:];
+  } else {
+    slices := x[1 : 1 : 1 : 3 : two : two : 0];
+    assert |slices[5]| == 2;
+  }
+  assert |slices| == 5 || |slices| == 7;
+  return middle(slices);
+}
+
+function method middle<G>(s: seq<G>): G
+  requires |s| % 2 == 1;
+{
+  s[|s| / 2]
+}