bv_cbmct::unbounded_arrayt::U_AUTO is never enabled

[tautschnig]

While seemingly meant to be the default (only never/always can be set via the command line), the default is actually U_NONE. Enabling it is trivial, but will break lots of examples until #1086 is complete and merged. Furthermore it seems current code only looks at the top-level size, not the nested values. Below is a patch that may be a useful starting point:

diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index ab69f9b..caf40be 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -110,6 +110,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
   else if(options.get_option("arrays-uf")=="always")
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
+  else
+    bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_AUTO;

   solver->set_prop_conv(std::move(bv_cbmc));

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 4cf43a0..503be96 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -689,17 +689,20 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   if(unbounded_array==unbounded_arrayt::U_ALL)
     return true;

+#if 0
   const exprt &size=to_array_type(type).size();

   mp_integer s;
   if(to_integer(size, s))
     return true;
+#endif

+  bool retval=false;
   if(unbounded_array==unbounded_arrayt::U_AUTO)
-    if(s>MAX_FLATTENED_ARRAY_SIZE)
-      return true;
+    if(boolbv_width(type)>MAX_FLATTENED_ARRAY_SIZE)
+      retval=true;

-  return false;
+  return retval;
 }

 void boolbvt::print_assignment(std::ostream &out) const