diff --git a/regression/cbmc/Array_UF22/main.c b/regression/cbmc/Array_UF22/main.c
new file mode 100644
index 00000000000..20ece5e5fe7
--- /dev/null
+++ b/regression/cbmc/Array_UF22/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  int a[2] = {0};
+  int b[2] = {0};
+  __CPROVER_assert(__CPROVER_array_equal(a, b), "equal");
+}
diff --git a/regression/cbmc/Array_UF22/test.desc b/regression/cbmc/Array_UF22/test.desc
new file mode 100644
index 00000000000..67011369611
--- /dev/null
+++ b/regression/cbmc/Array_UF22/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG broken-smt-backend
+main.c
+--arrays-uf-always --no-propagation
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test demonstrates the need for implementing the extensionality rule.