9 files changed, 78 insertions, 3 deletions

diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index 1e1f391c..d0a14586 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -52,7 +52,7 @@ val slice_slice : forall 'n 'm 'o 'p, 0 <= 'p <= 'm <= 'o & 'o - 'p < 'n.
 function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
 
 /* We can update a bitvector from another bitvector or a slice */
-val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
+val _set_slice : forall 'n 'm 'o, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), bits('o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice (v, stop, start, update) = {
@@ -61,7 +61,7 @@ function _set_slice (v, stop, start, update) = {
   (*v) = v2;
 }
 
-val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o <= 'n.
+val _set_slice2 : forall 'n 'm 'o 'p, 0 <= 'm <= 'o < 'n.
   (register(bits('n)), atom('o), atom('m), slice('p, 'o - ('m - 1))) -> unit effect {wreg, rreg}
 
 function _set_slice2 (v, stop, start, MkSlice(_, update)) = _set_slice(v, stop, start, update)
diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
index 078e266b..21911b15 100644
--- a/test/typecheck/pass/vec_length.sail
+++ b/test/typecheck/pass/vec_length.sail
@@ -4,5 +4,6 @@ $include <vector_dec.sail>
 function main () : unit -> unit = {
   let x : bits(8) = 0xff;
   let y = x[3];
+  let z = [x with 5 = y];
   ()
-}
\ No newline at end of file
+}
diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect
new file mode 100644
index 00000000..7ce8fd99
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1_inc.sail b/test/typecheck/pass/vec_length/v1_inc.sail
new file mode 100644
index 00000000..b72738d1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1_inc.sail
@@ -0,0 +1,8 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect
new file mode 100644
index 00000000..d123cabd
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2.sail b/test/typecheck/pass/vec_length/v2.sail
new file mode 100644
index 00000000..4df62e81
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect
new file mode 100644
index 00000000..e7d2b52f
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25
+
+  let z = [x with 10 = y];
+
+No overloadings for vector_update, tried:
+  bitvector_update:
+    Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_update:
+    Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v2_inc.sail b/test/typecheck/pass/vec_length/v2_inc.sail
new file mode 100644
index 00000000..3f75fee1
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v2_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 10 = y];
+  ()
+}
diff --git a/test/typecheck/pass/vec_length_inc.sail b/test/typecheck/pass/vec_length_inc.sail
new file mode 100644
index 00000000..a8dd707f
--- /dev/null
+++ b/test/typecheck/pass/vec_length_inc.sail
@@ -0,0 +1,9 @@
+default Order inc
+$include <vector_inc.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  let z = [x with 5 = y];
+  ()
+}