From a082485fb3d7fce983ff63b3cda5009edc935db0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 23 Feb 2026 12:14:58 +0000
Subject: [PATCH 1/2] Skip Ackermann constraints for derived arrays (weak
 equivalence)

Skip generating Ackermann constraints for arrays that are derived from
other arrays via with (store), if, array_of, array constants,
array_comprehension, typecast, or let expressions.

For a derived array such as x = y with [k := v], the Ackermann
constraint i1 = i2 => x[i1] = x[i2] is already implied by:
  (1) the with constraint: k != j => x[j] = y[j], and
  (2) the Ackermann constraint on the base array y.
This is the read-over-weakeq optimisation from the theory of weakly
equivalent arrays (Christ & Hoenicke, 2014).

The same reasoning applies to if, array_of, and other derived array
expressions, all of which already have constraints connecting them
element-wise to their constituent arrays.

With 5 stores to the same unbounded array the Ackermann constraint
count drops from 110 to 60; with 40 stores it drops from 63180 to
31980 (approximately 50% reduction in all cases).

Co-authored-by: Kiro
---
 regression/cbmc/Array_UF23/main.c    | 21 +++++++++++++++++++++
 regression/cbmc/Array_UF23/test.desc | 13 +++++++++++++
 src/solvers/flattening/arrays.cpp    | 19 +++++++++++++++++++
 3 files changed, 53 insertions(+)
 create mode 100644 regression/cbmc/Array_UF23/main.c
 create mode 100644 regression/cbmc/Array_UF23/test.desc

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/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

From 86a9c390a51ec7bfb1842c4dea57f31204a67dda Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 24 Feb 2026 10:32:14 +0000
Subject: [PATCH 2/2] Set 20-minute timeout for all CMake-based regression
 tests

Add TIMEOUT 1200 to the set_tests_properties call in both copies of the
add_test_pl_profile macro (regression/CMakeLists.txt and
regression/libcprover-cpp/CMakeLists.txt). This ensures CTest will kill
and report as failed any regression test that exceeds 20 minutes,
preventing CI jobs from hanging indefinitely on tests that time out.

Co-authored-by: Kiro (autonomous agent) <kiro-agent@users.noreply.github.com>
---
 regression/CMakeLists.txt                | 1 +
 regression/libcprover-cpp/CMakeLists.txt | 1 +
 2 files changed, 2 insertions(+)

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/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)