Test case for issue 861

tests/issues/issue861.cry

@@ -0,0 +1,6 @@
+atXis0:
+    {n, a, w}
+    (fin n, Eq a, Zero a, Cmp w, Integral w, Literal n w) =>
+    [n]a -> w -> Bit
+property atXis0 seq i =
+    zero == seq ==> i < `n ==> seq @ i == zero

tests/issues/issue861.icry

@@ -0,0 +1,31 @@
+:l issue861.cry
+
+:set tests=1000
+
+:check atXis0`{4, Char, Integer}
+
+let xs = [0,1,2] : [3]Integer
+
+xs@0
+xs@1
+xs@2
+xs@3
+xs@(-1)
+
+xs!0
+xs!1
+xs!2
+xs!3
+xs!(-1)
+
+update xs 0 5
+update xs 1 5
+update xs 2 5
+update xs 3 5
+update xs (-1) 5
+
+updateEnd xs 0 5
+updateEnd xs 1 5
+updateEnd xs 2 5
+updateEnd xs 3 5
+updateEnd xs (-1) 5

tests/issues/issue861.icry.stdout

@@ -0,0 +1,33 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Using random testing.
+Testing... Passed 1000 tests.
+0
+1
+2
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+2
+1
+0
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+[5, 1, 2]
+[0, 5, 2]
+[0, 1, 5]
+
+invalid sequence index: 3
+
+invalid sequence index: -1
+[0, 1, 5]
+[0, 5, 2]
+[5, 1, 2]
+
+invalid sequence index: 3
+
+invalid sequence index: -1