C nondet symbol factory: arrays may have zero size

There is nothing fundamentally wrong in an array having size 0.

Fixes: #5093

Author: tautschnig

regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --function testFunc
---
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^EXIT=134$
 --
-Github issue #5093: Pointer to struct with flexible array member as parameter to entry point causes invariant violation
+Github issue #5093: Pointer to struct with flexible array member as parameter to
+entry point causes invariant violation

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -173,7 +173,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(