Error handling for very large size arrays and vectors

This reinstates and improves the error handling for very large
arrays and vectors with the limit of 1 << 30 (from old code).
This prevents exceptions in the cast which can occur for extremely
large values.

Author: TGWDB

src/solvers/flattening/boolbv_width.cpp

@@ -135,7 +135,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     else
     {
       mp_integer total = *array_size * sub_width;
-      entry.total_width = numeric_cast_v<std::size_t>(total);
+      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);
     }
   }
   else if(type_id==ID_vector)
@@ -146,7 +151,12 @@ 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;
-    entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
+    if(total > (1 << 30)) // realistic limit
+      throw analysis_exceptiont("vector too large for flattening");
+    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)
   {