Enable and use the automatic limit for array-as-uninterpreted-function

This is a duplicate of PR diffblue#2108. This is here for alternative author
management.

Fixes diffblue#6130

Author: TGWDB

src/solvers/flattening/boolbv.cpp

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

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

src/solvers/flattening/boolbv_width.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/std_types.h>
@@ -136,13 +135,7 @@ 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");
-
-      if(total < 0)
-        entry.total_width = 0;
-      else
-        entry.total_width = numeric_cast_v<std::size_t>(total);
+      entry.total_width = numeric_cast_v<std::size_t>(total);
     }
   }
   else if(type_id==ID_vector)
@@ -153,9 +146,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)