8 files changed, 76 insertions, 1 deletions

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];
+  ()
+}