Array speedup

performance/array_read1.c

@@ -0,0 +1,10 @@
+int main()
+{
+  unsigned size;
+  char array[size];
+
+  for(unsigned i = 0; i < N; i++)
+    __CPROVER_assume(array[i] == 123);
+
+  __CPROVER_assert(0, "");
+}

performance/array_write1.c

@@ -0,0 +1,10 @@
+int main()
+{
+  unsigned size;
+  char array[size];
+
+  for(unsigned i = 0; i < N; i++)
+    array[i] = 123;
+
+  __CPROVER_assert(0, "");
+}

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 @@
+CORE 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.

regression/cbmc/trace-values/unbounded_array.c

@@ -9,5 +9,8 @@ int main(int argc, char *argv[])
   array[size - 1] = 42;
   int fixed_array[] = {1, 2};
   __CPROVER_array_replace(array, fixed_array);
+  assert(array[0] == 1);
+  assert(array[1] == 2);
+  assert(array[size - 1] == 42);
   assert(array[0] == 0);
 }