diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index f2632fcf3b0..6d8a6fe0702 100644
--- a/regression/CMakeLists.txt
+++ b/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)
 
diff --git a/regression/cbmc/Array_UF23/main.c b/regression/cbmc/Array_UF23/main.c
new file mode 100644
index 00000000000..77b15f695f7
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/Array_UF23/test.desc b/regression/cbmc/Array_UF23/test.desc
new file mode 100644
index 00000000000..947c52b86d9
--- /dev/null
+++ b/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.
diff --git a/regression/libcprover-cpp/CMakeLists.txt b/regression/libcprover-cpp/CMakeLists.txt
index 0c57cb71d46..8efb91967b8 100644
--- a/regression/libcprover-cpp/CMakeLists.txt
+++ b/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)
 
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 96cb3c8045f..c706d998ccc 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/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