Merge pull request #6194 from TGWDB/issue6130-auto-array

Enable and use the automatic limit for array-as-uninterpreted-function (duplicated, fixes 6130)

Author: TGWDB

src/solvers/flattening/boolbv.cpp

@@ -544,14 +544,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>
@@ -138,7 +137,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
       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
@@ -155,8 +153,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     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);
+    if(total < 0)
+      entry.total_width = 0;
+    else
+      entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
   }
   else if(type_id==ID_complex)
   {