From 55f386136e7e383a9237e5bf2154cd583aa524d1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 24 Apr 2022 16:05:59 +0000
Subject: [PATCH] Failing test to demonstrate need for extensionality rule

All existing tests rely on indexed access to arrays, which is covered by
the read-over-write axiom.
---
 regression/cbmc/Array_UF22/main.c    |  6 ++++++
 regression/cbmc/Array_UF22/test.desc | 10 ++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 regression/cbmc/Array_UF22/main.c
 create mode 100644 regression/cbmc/Array_UF22/test.desc

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.