Skip Ackermann constraints for derived arrays (weak equivalence)

regression/CMakeLists.txt

@@ -8,6 +8,7 @@ macro(add_test_pl_profile name cmdline flag profile)
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
         LABELS "${profile};CBMC"
+        TIMEOUT 1200
     )
 endmacro(add_test_pl_profile)
 

regression/cbmc/Array_UF23/main.c

@@ -0,0 +1,21 @@
+/// \file
+/// Test that Ackermann constraints are reduced by the weak equivalence
+/// optimisation: derived arrays (with, if, etc.) do not need Ackermann
+/// constraints because they are implied by the with/if constraints plus
+/// Ackermann on base arrays.
+#include <stdlib.h>
+int main()
+{
+  size_t array_size;
+  int a[array_size];
+  int i0, i1, i2, i3, i4;
+
+  a[i0] = 0;
+  a[i1] = 1;
+  a[i2] = 2;
+  a[i3] = 3;
+  a[i4] = 4;
+
+  __CPROVER_assert(a[i0] >= 0, "a[i0] >= 0");
+  return 0;
+}

regression/cbmc/Array_UF23/test.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend no-new-smt
+main.c
+--arrays-uf-always --unwind 1 --show-array-constraints --json-ui
+"arrayAckermann": 60
+^EXIT=10$
+^SIGNAL=0$
+--
+"arrayAckermann": 110
+--
+Checks that the weak equivalence optimisation reduces Ackermann constraints.
+With 5 stores to the same unbounded array, the old code produced 110 Ackermann
+constraints (one per pair of indices per array term). The optimised code skips
+derived arrays (with, if, etc.) and produces only 60.

regression/libcprover-cpp/CMakeLists.txt

@@ -20,6 +20,7 @@ macro(add_test_pl_profile name cmdline flag profile)
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
         LABELS "${profile};CBMC"
+        TIMEOUT 1200
     )
 endmacro(add_test_pl_profile)
 

src/solvers/flattening/arrays.cpp

@@ -335,6 +335,25 @@ void arrayst::add_array_Ackermann_constraints()
   // iterate over arrays
   for(std::size_t i=0; i<arrays.size(); i++)
   {
+    // Skip arrays that are derived from other arrays via with, if, etc.
+    // Their Ackermann constraints are implied by the combination of:
+    // (1) the with/if/array_of/etc. constraints already generated, and
+    // (2) the Ackermann constraints on the underlying base arrays.
+    // This is the "weak equivalence" optimisation: arrays connected by
+    // store chains are weakly equivalent, and read-over-weakeq follows
+    // from the read-over-write constraints plus Ackermann on base arrays.
+    const exprt &arr = arrays[i];
+    if(
+      arr.id() == ID_with || arr.id() == ID_update || arr.id() == ID_if ||
+      arr.id() == ID_array_of || arr.id() == ID_array ||
+      arr.id() == ID_array_comprehension || arr.id() == ID_typecast ||
+      arr.id() == ID_string_constant || arr.is_constant())
+    {
+      continue;
+    }
+    if(expr_try_dynamic_cast<let_exprt>(arr))
+      continue;
+
     const index_sett &index_set=index_map[arrays.find_number(i)];
 
 #ifdef DEBUG