diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2 b/regression/QF_AX/arrays_extensionality_no_selects.smt2
new file mode 100644
index 000000000..ec3d001b4
--- /dev/null
+++ b/regression/QF_AX/arrays_extensionality_no_selects.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_AX)
+(set-info :status sat)
+(set-info :smt-lib-version 2.6)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun S () (Array I E))
+(declare-fun SS () (Array I E))
+(assert (= S SS))
+(check-sat)
diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.err b/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.out b/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.out
new file mode 100644
index 000000000..6b8a2c3d2
--- /dev/null
+++ b/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2 b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2
new file mode 100644
index 000000000..e6df8d1c0
--- /dev/null
+++ b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AX)
+(set-info :status unsat)
+(set-info :smt-lib-version 2.6)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun S () (Array I E))
+(declare-fun SS () (Array I E))
+(declare-fun SSS () (Array I E))
+(assert (= S SS))
+(assert (= SS SSS))
+(assert (not (= S SSS)))
+(check-sat)
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.err b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.err
new file mode 100644
index 000000000..e69de29bb
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.out b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.out
new file mode 100644
index 000000000..3f65111b0
--- /dev/null
+++ b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.out
@@ -0,0 +1 @@
+unsat