Enable automatic limit for array-as-uninterpreted-function

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.

This reverts #6232, but now includes additional changes to the array
theory to handle nested struct members no different from members of a
top-level struct.

Fixes: #2018

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -195,12 +195,6 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
-    const auto &struct_op = to_member_expr(a).struct_op();
-
-    DATA_INVARIANT(
-      struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
-      "unexpected array expression: member with '" + struct_op.id_string() +
-        "'");
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -494,10 +488,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

@@ -49,7 +49,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),