diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go
index c8bde74..d905cfa 100644
--- a/pkg/corset/resolver.go
+++ b/pkg/corset/resolver.go
@@ -558,14 +558,18 @@ func (r *resolver) finaliseArrayAccessInModule(scope LocalScope, expr *ArrayAcce
 	//
 	if !expr.IsResolved() && !scope.Bind(expr) {
 		return nil, r.srcmap.SyntaxErrors(expr, "unknown array column")
-	} else if binding, ok := expr.Binding().(*ColumnBinding); ok {
-		// Found column, now check it is an array.
-		if arr_t, ok := binding.dataType.(*ArrayType); ok {
-			return arr_t.element, nil
-		}
+	} else if binding, ok := expr.Binding().(*ColumnBinding); !ok {
+		return nil, r.srcmap.SyntaxErrors(expr, "unknown array column")
+	} else if arr_t, ok := binding.dataType.(*ArrayType); !ok {
+		return nil, r.srcmap.SyntaxErrors(expr, "expected array column")
+	} else if c := expr.arg.AsConstant(); c == nil {
+		return nil, r.srcmap.SyntaxErrors(expr, "expected constant array index")
+	} else if i := uint(c.Uint64()); i == 0 || i > arr_t.Width() {
+		return nil, r.srcmap.SyntaxErrors(expr, "array access out-of-bounds")
+	} else {
+		// All good
+		return arr_t.element, nil
 	}
-	// Default
-	return nil, r.srcmap.SyntaxErrors(expr, "not an array column")
 }
 
 // Resolve an if condition contained within some expression which, in turn, is
diff --git a/pkg/corset/translator.go b/pkg/corset/translator.go
index 35fd1c3..3aa231b 100644
--- a/pkg/corset/translator.go
+++ b/pkg/corset/translator.go
@@ -446,6 +446,9 @@ func (t *translator) translateArrayAccessInModule(expr *ArrayAccess, shift int)
 	// Did we find it?
 	if !ok {
 		errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "invalid array index encountered during translation"))
+	}
+	// Error check
+	if len(errors) > 0 {
 		return nil, errors
 	}
 	// Lookup underlying column info
diff --git a/pkg/test/invalid_corset_test.go b/pkg/test/invalid_corset_test.go
index 3b10b91..e73d649 100644
--- a/pkg/test/invalid_corset_test.go
+++ b/pkg/test/invalid_corset_test.go
@@ -494,6 +494,29 @@ func Test_Invalid_For_03(t *testing.T) {
 	CheckInvalid(t, "for_invalid_03")
 }
 
+// ===================================================================
+// Arrays
+// ===================================================================
+func Test_Invalid_Array_01(t *testing.T) {
+	CheckInvalid(t, "array_invalid_01")
+}
+
+func Test_Invalid_Array_02(t *testing.T) {
+	CheckInvalid(t, "array_invalid_02")
+}
+
+func Test_Invalid_Array_03(t *testing.T) {
+	CheckInvalid(t, "array_invalid_03")
+}
+
+func Test_Invalid_Array_04(t *testing.T) {
+	CheckInvalid(t, "array_invalid_04")
+}
+
+func Test_Invalid_Array_05(t *testing.T) {
+	CheckInvalid(t, "array_invalid_05")
+}
+
 // ===================================================================
 // Test Helpers
 // ===================================================================
diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go
index 9993429..72f5991 100644
--- a/pkg/test/valid_corset_test.go
+++ b/pkg/test/valid_corset_test.go
@@ -648,6 +648,15 @@ func Test_Array_01(t *testing.T) {
 	Check(t, false, "array_01")
 }
 
+/* func Test_Array_02(t *testing.T) {
+	Check(t, false, "array_02")
+}
+*/
+
+func Test_Array_03(t *testing.T) {
+	Check(t, false, "array_03")
+}
+
 // ===================================================================
 // Complex Tests
 // ===================================================================
diff --git a/testdata/array_02.accepts b/testdata/array_02.accepts
new file mode 100644
index 0000000..3df73f5
--- /dev/null
+++ b/testdata/array_02.accepts
@@ -0,0 +1,18 @@
+{ "ARG": [], "BIT_4": [], "BIT_3": [], "BIT_2": [], "BIT_1": [] }
+;;
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
diff --git a/testdata/array_02.lisp b/testdata/array_02.lisp
new file mode 100644
index 0000000..d319048
--- /dev/null
+++ b/testdata/array_02.lisp
@@ -0,0 +1,8 @@
+(defcolumns
+    (BIT :binary@prove :array [4])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (reduce +
+      (for i [0:3] (* (^ 2 i) [BIT (+ 1 i)])))))
diff --git a/testdata/array_02.rejects b/testdata/array_02.rejects
new file mode 100644
index 0000000..ff824cd
--- /dev/null
+++ b/testdata/array_02.rejects
@@ -0,0 +1,256 @@
+;; x=0
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=1
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=2
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=3
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=4
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=5
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=6
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=7
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=8
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=9
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=10
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=11
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=12
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=13
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=14
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+;; x=15
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] }
+{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] }
diff --git a/testdata/array_03.accepts b/testdata/array_03.accepts
new file mode 100644
index 0000000..801a8c1
--- /dev/null
+++ b/testdata/array_03.accepts
@@ -0,0 +1,7 @@
+{"ARR_1": [], "ARR_2": []}
+{"ARR_1": [-1], "ARR_2": [1]}
+{"ARR_1": [0], "ARR_2": [0]}
+{"ARR_1": [1], "ARR_2": [-1]}
+{"ARR_1": [0,-1], "ARR_2": [0,1]}
+{"ARR_1": [0,0], "ARR_2": [0,0]}
+{"ARR_1": [0,1], "ARR_2": [0,-1]}
diff --git a/testdata/array_03.lisp b/testdata/array_03.lisp
new file mode 100644
index 0000000..d62ede2
--- /dev/null
+++ b/testdata/array_03.lisp
@@ -0,0 +1,3 @@
+(defcolumns (ARR :@loob :array [2]))
+(defconstraint c1 () (+ [ARR 1] [ARR 2]))
+(defconstraint c2 () (+ [ARR 2] [ARR 2]))
diff --git a/testdata/array_03.rejects b/testdata/array_03.rejects
new file mode 100644
index 0000000..0acce1a
--- /dev/null
+++ b/testdata/array_03.rejects
@@ -0,0 +1,6 @@
+{"ARR_1": [1], "ARR_2": [0]}
+{"ARR_1": [-1], "ARR_2": [0]}
+{"ARR_1": [0], "ARR_2": [1]}
+{"ARR_1": [0], "ARR_2": [-1]}
+{"ARR_1": [2], "ARR_2": [-1]}
+{"ARR_1": [-2], "ARR_2": [1]}
diff --git a/testdata/array_invalid_01.lisp b/testdata/array_invalid_01.lisp
new file mode 100644
index 0000000..50456c3
--- /dev/null
+++ b/testdata/array_invalid_01.lisp
@@ -0,0 +1,4 @@
+;;error:4:24-30:not an array column
+(defcolumns (BIT :@loob))
+
+(defconstraint bits () [BIT 1])
diff --git a/testdata/array_invalid_02.lisp b/testdata/array_invalid_02.lisp
new file mode 100644
index 0000000..58137e9
--- /dev/null
+++ b/testdata/array_invalid_02.lisp
@@ -0,0 +1,4 @@
+;;error:4:24-25:expected loobean constraint (found (𝔽@loob)[4])
+(defcolumns (BIT :@loob :array [4]))
+
+(defconstraint bits () BIT)
diff --git a/testdata/array_invalid_03.lisp b/testdata/array_invalid_03.lisp
new file mode 100644
index 0000000..0c04221
--- /dev/null
+++ b/testdata/array_invalid_03.lisp
@@ -0,0 +1,4 @@
+;;error:4:24-30:expected constant array index
+(defcolumns X (BIT :@loob :array [4]))
+
+(defconstraint bits () [BIT X])
diff --git a/testdata/array_invalid_04.lisp b/testdata/array_invalid_04.lisp
new file mode 100644
index 0000000..b2169e5
--- /dev/null
+++ b/testdata/array_invalid_04.lisp
@@ -0,0 +1,12 @@
+;;error:12:12-18:out-of-bounds array access
+(defcolumns
+    (BIT :binary@prove :array [3])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (+
+      (* 1 [BIT 1])
+      (* 2 [BIT 2])
+      (* 4 [BIT 3])
+      (* 8 [BIT 4]))))
diff --git a/testdata/array_invalid_05.lisp b/testdata/array_invalid_05.lisp
new file mode 100644
index 0000000..4518bbc
--- /dev/null
+++ b/testdata/array_invalid_05.lisp
@@ -0,0 +1,12 @@
+;;error:12:12-18:out-of-bounds array access
+(defcolumns
+    (BIT :binary@prove :array [4])
+    (ARG :i16@loob))
+
+(defconstraint bits ()
+  (- ARG
+     (+
+      (* 1 [BIT 0])
+      (* 2 [BIT 1])
+      (* 4 [BIT 2])
+      (* 8 [BIT 3]))))