Merge pull request #6824 from tautschnig/feature/extensionality

Failing test to demonstrate need for extensionality rule

Author: kroening

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

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.