Re-enable array theory as default for array size above threshold

Previously, the command line permitted setting uninterpreted functions
to "never" or "always", where "never" actually was the default. The
"automatic" mode could not be enabled in any way.

We previously attempted to do this in in #6194 (inspired by #2108, but
not picking up all its changes), but then reverted the gist of the
change in #6232 as `array-bug-6230/main.c` demonstrated lingering
issues. This PR now addresses the flaw in the array theory back-end.

We may still run into performance regressions as the threshold of 1000
bits of total size of the array object is possibly lower than where the
cost of bit-blasting exceeds the cost of constraints produced by our
current array theory implementation. Two of our existing regression
tests already demonstrate this problem, hence those now use
`--arrays-uf-never`.

regression/cbmc/array-bug-6230/main.c

@@ -3,7 +3,9 @@
 
 struct inner
 {
-  uint32_t exts[32]; // 32 is the minimum to crash
+  // 32 is the minimum to crash as it will produce an array wider than 1000 bits
+  // (the default value of MAX_FLATTENED_ARRAY_SIZE)
+  uint32_t exts[32];
 };
 
 struct outer

regression/cbmc/bounds_check1/test.desc

@@ -1,6 +1,6 @@
 CORE thorough-smt-backend no-new-smt
 main.c
---no-malloc-may-fail
+--no-malloc-may-fail --arrays-uf-never
 ^EXIT=10$
 ^SIGNAL=0$
 \[\(.*\)i2\]: FAILURE

regression/cbmc/union/union_large_array.desc

@@ -1,6 +1,6 @@
 CORE thorough-smt-backend no-new-smt
 union_large_array.c
-
+--arrays-uf-never
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ should fail: FAILURE$

src/solvers/flattening/arrays.cpp

@@ -196,12 +196,24 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
-    const auto &struct_op = to_member_expr(a).struct_op();
+    const exprt *struct_op_ptr = &to_member_expr(a).struct_op();
+    while(struct_op_ptr->id() == ID_member)
+      struct_op_ptr = &to_member_expr(*struct_op_ptr).struct_op();
 
-    DATA_INVARIANT(
-      struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
-      "unexpected array expression: member with '" + struct_op.id_string() +
-        "'");
+    if(struct_op_ptr->id() == ID_index)
+    {
+      const auto &array_op = to_index_expr(*struct_op_ptr).array();
+      arrays.make_union(a, array_op);
+      collect_arrays(array_op);
+    }
+    else
+    {
+      DATA_INVARIANT(
+        struct_op_ptr->id() == ID_struct || struct_op_ptr->id() == ID_symbol ||
+          struct_op_ptr->id() == ID_nondet_symbol,
+        "unexpected array expression: member with '" +
+          struct_op_ptr->id_string() + "'");
+    }
   }
   else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant)
   {
@@ -497,10 +509,7 @@ void arrayst::add_array_constraints(
     expr.id() == ID_string_constant)
   {
   }
-  else if(
-    expr.id() == ID_member &&
-    (to_member_expr(expr).struct_op().id() == ID_symbol ||
-     to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
+  else if(expr.id() == ID_member)
   {
   }
   else if(expr.id()==ID_byte_update_little_endian ||

src/solvers/flattening/boolbv.h

@@ -51,7 +51,7 @@ class boolbvt:public arrayst
     message_handlert &message_handler,
     bool get_array_constraints = false)
     : arrayst(_ns, _prop, message_handler, get_array_constraints),
-      unbounded_array(unbounded_arrayt::U_NONE),
+      unbounded_array(unbounded_arrayt::U_AUTO),
       bv_width(_ns),
       bv_utils(_prop),
       functions(*this),