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

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 @@
   }
   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 @@
     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),