Enable and use the 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.

Furthermore the limit should apply across all dimensions of an array, not just
the top-level size.

Fixes: #2018

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -631,14 +631,12 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   if(unbounded_array==unbounded_arrayt::U_ALL)
     return true;
 
-  const exprt &size=to_array_type(type).size();
-
-  const auto s = numeric_cast<mp_integer>(size);
-  if(!s.has_value())
+  const std::size_t size = boolbv_width(type);
+  if(size == 0)
     return true;
 
   if(unbounded_array==unbounded_arrayt::U_AUTO)
-    if(*s > MAX_FLATTENED_ARRAY_SIZE)
+    if(size > MAX_FLATTENED_ARRAY_SIZE)
       return true;
 
   return false;

src/solvers/flattening/boolbv.h

@@ -39,7 +39,7 @@ class boolbvt:public arrayst
     propt &_prop,
     message_handlert &message_handler)
     : arrayst(_ns, _prop, message_handler),
-      unbounded_array(unbounded_arrayt::U_NONE),
+      unbounded_array(unbounded_arrayt::U_AUTO),
       boolbv_width(_ns),
       bv_utils(_prop),
       functions(*this),

src/solvers/flattening/boolbv_width.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/std_types.h>
 
@@ -138,9 +137,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     else
     {
       mp_integer total = *array_size * sub_width;
-      if(total>(1<<30)) // realistic limit
-        throw analysis_exceptiont("array too large for flattening");
-
       entry.total_width = numeric_cast_v<std::size_t>(total);
     }
   }
@@ -152,9 +148,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
 
     mp_integer total = vector_size * sub_width;
-    if(total > (1 << 30)) // realistic limit
-      throw analysis_exceptiont("vector too large for flattening");
-
     entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
   }
   else if(type_id==ID_complex)