diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 023f1805fe1..cb035f2a530 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -195,12 +195,6 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
-    const auto &struct_op = to_member_expr(a).struct_op();
-
-    DATA_INVARIANT(
-      struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
-      "unexpected array expression: member with '" + struct_op.id_string() +
-        "'");
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -494,10 +488,7 @@ void arrayst::add_array_constraints(
           expr.id()==ID_string_constant)
   {
   }
-  else if(
-    expr.id() == ID_member &&
-    (to_member_expr(expr).struct_op().id() == ID_symbol ||
-     to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
+  else if(expr.id() == ID_member)
   {
   }
   else if(expr.id()==ID_byte_update_little_endian ||
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 1636dd67ffa..6eaf6c48643 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -49,7 +49,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),