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

@@ -638,14 +638,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

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