diff --git a/regression/cbmc/Struct_Hack_Initialization/main.c b/regression/cbmc/Struct_Hack_Initialization/main.c
new file mode 100644
index 00000000000..f1a9c874834
--- /dev/null
+++ b/regression/cbmc/Struct_Hack_Initialization/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+typedef struct stritem
+{
+  unsigned nkey;
+  unsigned cas[];
+} item;
+
+int foo(item *it)
+{
+  assert(it->cas[0] == 0);
+  return 0;
+}
diff --git a/regression/cbmc/Struct_Hack_Initialization/test.desc b/regression/cbmc/Struct_Hack_Initialization/test.desc
new file mode 100644
index 00000000000..5ec6fe729da
--- /dev/null
+++ b/regression/cbmc/Struct_Hack_Initialization/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--function foo --bounds-check --pointer-check
+^\[foo.assertion.1\] line \d+ assertion it->cas\[0\] == 0: FAILURE$
+^\[foo.array_bounds.3\] line \d+ array.cas upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.array_bounds.2\] line \d+ array.cas dynamic object upper bound in it->cas\[\(.*\)0\]: FAILURE$
+^\[foo.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in it->cas: SUCCESS$
+^\[foo.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in it->cas: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 5e91a9a2a73..5047a756425 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -163,7 +163,6 @@ void symbol_factoryt::gen_nondet_array_init(
   const auto &size = array_type.size();
   PRECONDITION(size.id() == ID_constant);
   auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
-  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
   for(size_t index = 0; index < array_size; ++index)
   {
     gen_nondet_init(
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 1868627547a..184cc479bc6 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -2672,7 +2672,14 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
 
         // may need to flatten array-theory arrays in there
         if(op.type().id() == ID_array)
-          flatten_array(op);
+        {
+          const array_typet &array_type = to_array_type(op.type());
+          const auto &size_expr = array_type.size();
+          CHECK_RETURN(size_expr.id() == ID_constant);
+
+          if(numeric_cast_v<mp_integer>(to_constant_expr(size_expr)) != 0)
+            flatten_array(op);
+        }
         else
           convert_expr(op);
 
@@ -4526,7 +4533,11 @@ void smt2_convt::convert_type(const typet &type)
   {
     if(use_datatypes)
     {
-      out << datatype_map.at(type);
+      const typet &struct_type = type.id() == ID_struct_tag
+                                   ? ns.follow_tag(to_struct_tag_type(type))
+                                   : type;
+      CHECK_RETURN(datatype_map.count(struct_type) > 0);
+      out << datatype_map.at(struct_type);
     }
     else
     {