diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 1a0ab2c3487..df1186b8462 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -172,9 +172,9 @@ void symbol_factoryt::gen_nondet_array_init(
   auto const &array_type = to_array_type(expr.type());
   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)
+  auto const array_size = numeric_cast_v<mp_integer>(to_constant_expr(size));
+  DATA_INVARIANT(array_size >= 0, "Arrays must have non-negative size");
+  for(mp_integer index = 0; index < array_size; ++index)
   {
     gen_nondet_init(
       assignments,