diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index dce9c55f267..cb0c52ec8b4 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/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;
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index fc3b1484b96..3bda86f2cfa 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/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),
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 39e5439cf08..90b9eda01b2 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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)
   {