diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 48a9b58654c..07dd5a77b81 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -708,12 +708,14 @@ void java_bytecode_convert_classt::convert(
       new_symbol.type.set(ID_C_access, ID_default);
 
     const namespacet ns(symbol_table);
-    new_symbol.value=
-      zero_initializer(
-        field_type,
-        class_symbol.location,
-        ns,
-        get_message_handler());
+    const auto value = zero_initializer(field_type, class_symbol.location, ns);
+    if(!value.has_value())
+    {
+      error().source_location = class_symbol.location;
+      error() << "failed to zero-initialize " << f.name << eom;
+      throw 0;
+    }
+    new_symbol.value = *value;
 
     // Load annotations
     if(!f.annotations.empty())
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index a8b84381b12..981dc61ca0d 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2951,8 +2951,15 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   if(return_type.id() == ID_empty)
     return {};
 
-  return zero_initializer(
-    return_type, location, namespacet(symbol_table), get_message_handler());
+  const auto value =
+    zero_initializer(return_type, location, namespacet(symbol_table));
+  if(!value.has_value())
+  {
+    error().source_location = location;
+    error() << "failed to zero-initialize return type" << eom;
+    throw 0;
+  }
+  return value;
 }
 
 void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index cdabf2adb42..bc163e076a1 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -193,13 +193,18 @@ static void java_static_lifetime_init(
         // First initialize the object as prior to a constructor:
         namespacet ns(symbol_table);
 
-        exprt zero_object =
-          zero_initializer(
-            sym.type, source_locationt(), ns, message_handler);
+        auto zero_object = zero_initializer(sym.type, source_locationt(), ns);
+        if(!zero_object.has_value())
+        {
+          messaget message(message_handler);
+          message.error() << "failed to zero-initialize " << sym.name
+                          << messaget::eom;
+          throw 0;
+        }
         set_class_identifier(
-          to_struct_expr(zero_object), ns, to_symbol_type(sym.type));
+          to_struct_expr(*zero_object), ns, to_symbol_type(sym.type));
 
-        code_block.add(code_assignt(sym.symbol_expr(), zero_object));
+        code_block.add(code_assignt(sym.symbol_expr(), *zero_object));
 
         // Then call the init function:
         code_block.move(initializer_call);
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 2850ac3b1a4..3afc19cbe04 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1044,19 +1044,17 @@ void java_object_factoryt::gen_nondet_struct_init(
     // passes can easily recognise leaves no uninitialised state behind.
 
     // This code mirrors the `remove_java_new` pass:
-    null_message_handlert nullout;
-    exprt initial_object =
-      zero_initializer(
-        struct_type, source_locationt(), ns, nullout);
+    auto initial_object = zero_initializer(struct_type, source_locationt(), ns);
+    CHECK_RETURN(initial_object.has_value());
     irep_idt qualified_clsid = "java::" + id2string(class_identifier);
     set_class_identifier(
-      to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid));
+      to_struct_expr(*initial_object), ns, symbol_typet(qualified_clsid));
 
     // If the initialised type is a special-cased String type (one with length
     // and data fields introduced by string-library preprocessing), initialise
     // those fields with nondet values:
     skip_special_string_fields = initialize_nondet_string_fields(
-      to_struct_expr(initial_object),
+      to_struct_expr(*initial_object),
       assignments,
       object_factory_parameters.min_nondet_string_length,
       object_factory_parameters.max_nondet_string_length,
@@ -1065,7 +1063,7 @@ void java_object_factoryt::gen_nondet_struct_init(
       symbol_table,
       object_factory_parameters.string_printable);
 
-    assignments.add(code_assignt(expr, initial_object));
+    assignments.add(code_assignt(expr, *initial_object));
   }
 
   for(const auto &component : components)
diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp
index 8463139d7b8..71723840dd3 100644
--- a/jbmc/src/java_bytecode/java_string_literals.cpp
+++ b/jbmc/src/java_bytecode/java_string_literals.cpp
@@ -192,8 +192,10 @@ symbol_exprt get_or_create_string_literal_symbol(
       // Other members of JDK's java.lang.String we don't understand
       // without string-refinement. Just zero-init them; consider using
       // test-gen-like nondet object trees instead.
-      literal_init.copy_to_operands(
-        zero_initializer(comp.type(), string_expr.source_location(), ns));
+      const auto init =
+        zero_initializer(comp.type(), string_expr.source_location(), ns);
+      CHECK_RETURN(init.has_value());
+      literal_init.copy_to_operands(*init);
     }
     new_symbol.value = literal_init;
   }
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
index 35ba1e8996b..34673a85181 100644
--- a/jbmc/src/java_bytecode/remove_java_new.cpp
+++ b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -93,12 +93,12 @@ goto_programt::targett remove_java_newt::lower_java_new(
 
   // zero-initialize the object
   dereference_exprt deref(lhs, object_type);
-  exprt zero_object =
-    zero_initializer(object_type, location, ns, get_message_handler());
+  auto zero_object = zero_initializer(object_type, location, ns);
+  CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
+    to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
   goto_programt::targett t_i = dest.insert_after(target);
-  t_i->make_assignment(code_assignt(deref, zero_object));
+  t_i->make_assignment(code_assignt(deref, *zero_object));
   t_i->source_location = location;
 
   return t_i;
@@ -153,12 +153,12 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
   // Init base class:
   dereference_exprt deref(lhs, object_type);
-  exprt zero_object =
-    zero_initializer(object_type, location, ns, get_message_handler());
+  auto zero_object = zero_initializer(object_type, location, ns);
+  CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
+    to_struct_expr(*zero_object), ns, to_symbol_type(object_type));
   goto_programt::targett t_i = dest.insert_before(next);
-  t_i->make_assignment(code_assignt(deref, zero_object));
+  t_i->make_assignment(code_assignt(deref, *zero_object));
   t_i->source_location = location;
 
   // if it's an array, we need to set the length field
@@ -232,10 +232,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // zero-initialize the data
   if(!rhs.get_bool(ID_skip_initialize))
   {
-    exprt zero_element = zero_initializer(
-      data.type().subtype(), location, ns, get_message_handler());
+    const auto zero_element =
+      zero_initializer(data.type().subtype(), location, ns);
+    CHECK_RETURN(zero_element.has_value());
     codet array_set(ID_array_set);
-    array_set.copy_to_operands(new_array_data_symbol, zero_element);
+    array_set.copy_to_operands(new_array_data_symbol, *zero_element);
     goto_programt::targett t_d = dest.insert_before(next);
     t_d->make_other(array_set);
     t_d->source_location = location;
diff --git a/regression/ansi-c/array_initialization4/main.c b/regression/ansi-c/array_initialization4/main.c
new file mode 100644
index 00000000000..1113857429d
--- /dev/null
+++ b/regression/ansi-c/array_initialization4/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int foo(unsigned n)
+{
+  assert(n > 0);
+  int A[n] = {1};
+  return A[0];
+}
+
+int main()
+{
+  assert(foo(1) == 1);
+}
diff --git a/regression/ansi-c/array_initialization4/test.desc b/regression/ansi-c/array_initialization4/test.desc
new file mode 100644
index 00000000000..1320fac0435
--- /dev/null
+++ b/regression/ansi-c/array_initialization4/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 485ab675f57..cf20ab85dd8 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -114,13 +114,16 @@ exprt c_typecheck_baset::do_initializer_rec(
       {
         // fill up
         tmp.type()=type;
-        exprt zero=
-          zero_initializer(
-            full_type.subtype(),
-            value.source_location(),
-            *this,
-            get_message_handler());
-        tmp.operands().resize(integer2size_t(array_size), zero);
+        const auto zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize array with subtype `"
+                  << to_string(full_type.subtype()) << "'" << eom;
+          throw 0;
+        }
+        tmp.operands().resize(integer2size_t(array_size), *zero);
       }
     }
 
@@ -171,13 +174,16 @@ exprt c_typecheck_baset::do_initializer_rec(
       {
         // fill up
         tmp2.type()=type;
-        exprt zero=
-          zero_initializer(
-            full_type.subtype(),
-            value.source_location(),
-            *this,
-            get_message_handler());
-        tmp2.operands().resize(integer2size_t(array_size), zero);
+        const auto zero =
+          zero_initializer(full_type.subtype(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize array with subtype `"
+                  << to_string(full_type.subtype()) << "'" << eom;
+          throw 0;
+        }
+        tmp2.operands().resize(integer2size_t(array_size), *zero);
       }
     }
 
@@ -395,13 +401,16 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
             to_array_type(full_type).size().is_nil()))
         {
           // we are willing to grow an incomplete or zero-sized array
-          exprt zero=
-            zero_initializer(
-              full_type.subtype(),
-              value.source_location(),
-              *this,
-              get_message_handler());
-          dest->operands().resize(integer2size_t(index)+1, zero);
+          const auto zero = zero_initializer(
+            full_type.subtype(), value.source_location(), *this);
+          if(!zero.has_value())
+          {
+            err_location(value);
+            error() << "cannot zero-initialize array with subtype `"
+                    << to_string(full_type.subtype()) << "'" << eom;
+            throw 0;
+          }
+          dest->operands().resize(integer2size_t(index) + 1, *zero);
 
           // todo: adjust type!
         }
@@ -461,15 +470,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       {
         // Note that gcc issues a warning if the union component is switched.
         // Build a union expression from given component.
-        union_exprt union_expr(type);
-        union_expr.op()=
-          zero_initializer(
-            component.type(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        const auto zero =
+          zero_initializer(component.type(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize union component of type `"
+                  << to_string(component.type()) << "'" << eom;
+          throw 0;
+        }
+        union_exprt union_expr(component.get_name(), *zero, type);
         union_expr.add_source_location()=value.source_location();
-        union_expr.set_component_name(component.get_name());
         *dest=union_expr;
       }
 
@@ -524,15 +535,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         const union_typet::componentt &component=
           union_type.components().front();
 
-        union_exprt union_expr(type);
-        union_expr.op()=
-          zero_initializer(
-            component.type(),
-            value.source_location(),
-            *this,
-            get_message_handler());
+        const auto zero =
+          zero_initializer(component.type(), value.source_location(), *this);
+        if(!zero.has_value())
+        {
+          err_location(value);
+          error() << "cannot zero-initialize union component of type `"
+                  << to_string(component.type()) << "'" << eom;
+          throw 0;
+        }
+        union_exprt union_expr(component.get_name(), *zero, type);
         union_expr.add_source_location()=value.source_location();
-        union_expr.set_component_name(component.get_name());
         *dest=union_expr;
       }
     }
@@ -830,9 +843,15 @@ exprt c_typecheck_baset::do_initializer_list(
      full_type.id()==ID_vector)
   {
     // start with zero everywhere
-    result=
-      zero_initializer(
-        type, value.source_location(), *this, get_message_handler());
+    const auto zero = zero_initializer(type, value.source_location(), *this);
+    if(!zero.has_value())
+    {
+      err_location(value.source_location());
+      error() << "cannot zero-initialize `" << to_string(full_type) << "'"
+              << eom;
+      throw 0;
+    }
+    result = *zero;
   }
   else if(full_type.id()==ID_array)
   {
@@ -845,9 +864,15 @@ exprt c_typecheck_baset::do_initializer_list(
     else
     {
       // start with zero everywhere
-      result=
-        zero_initializer(
-          type, value.source_location(), *this, get_message_handler());
+      const auto zero = zero_initializer(type, value.source_location(), *this);
+      if(!zero.has_value())
+      {
+        err_location(value.source_location());
+        error() << "cannot zero-initialize `" << to_string(full_type) << "'"
+                << eom;
+        throw 0;
+      }
+      result = *zero;
     }
 
     // 6.7.9, 14: An array of character type may be initialized by a character
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index ae40e1a3ce7..87356b9112c 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -870,15 +870,18 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr)
   {
     // Default value, e.g., int()
     typecheck_type(expr.type());
-    exprt new_expr=
-      ::zero_initializer(
-        expr.type(),
-        expr.find_source_location(),
-        *this,
-        get_message_handler());
-
-    new_expr.add_source_location()=expr.source_location();
-    expr=new_expr;
+    auto new_expr =
+      ::zero_initializer(expr.type(), expr.find_source_location(), *this);
+    if(!new_expr.has_value())
+    {
+      err_location(expr.find_source_location());
+      error() << "cannot zero-initialize `" << to_string(expr.type()) << "'"
+              << eom;
+      throw 0;
+    }
+
+    new_expr->add_source_location() = expr.source_location();
+    expr = *new_expr;
   }
   else if(expr.operands().size()==1)
   {
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index df540ae02dc..a43d16630d8 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -306,13 +306,16 @@ void cpp_typecheckt::zero_initializer(
   }
   else
   {
-    exprt value=
-      ::zero_initializer(
-        final_type, source_location, *this, get_message_handler());
+    const auto value = ::zero_initializer(final_type, source_location, *this);
+    if(!value.has_value())
+    {
+      err_location(source_location);
+      error() << "cannot zero-initialize `" << to_string(final_type) << "'"
+              << eom;
+      throw 0;
+    }
 
-    code_assignt assign;
-    assign.lhs()=object;
-    assign.rhs()=value;
+    code_assignt assign(object, *value);
     assign.add_source_location()=source_location;
 
     typecheck_expr(assign.op0());
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index 216667de32c..5138d9799f1 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -522,8 +522,9 @@ int linker_script_merget::ls_data2instructions(
     // Push the array initialization to the front now, so that it happens before
     // the initialization of the symbols that point to it.
     namespacet ns(symbol_table);
-    exprt zi=zero_initializer(array_type, array_loc, ns, *message_handler);
-    code_assignt array_assign(array_expr, zi);
+    const auto zi = zero_initializer(array_type, array_loc, ns);
+    CHECK_RETURN(zi.has_value());
+    code_assignt array_assign(array_expr, *zi);
     array_assign.add_source_location()=array_loc;
     goto_programt::instructiont array_assign_i;
     array_assign_i.make_assignment(array_assign);
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index e295f1aafa5..a141246e2e3 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1192,13 +1192,10 @@ void goto_convertt::do_function_call_symbol(
     {
       goto_programt::targett t=dest.add_instruction(ASSIGN);
       t->source_location=function.source_location();
-      exprt zero=
-        zero_initializer(
-          dest_expr.type(),
-          function.source_location(),
-          ns,
-          get_message_handler());
-      t->code=code_assignt(dest_expr, zero);
+      const auto zero =
+        zero_initializer(dest_expr.type(), function.source_location(), ns);
+      CHECK_RETURN(zero.has_value());
+      t->code = code_assignt(dest_expr, *zero);
     }
   }
   else if(identifier=="__sync_fetch_and_add" ||
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 9e918fec7fd..8e442d796e4 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -169,16 +169,10 @@ void goto_symext::symex_allocate(
 
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
-    null_message_handlert null_message;
-    exprt zero_value=
-      zero_initializer(
-        object_type,
-        code.source_location(),
-        ns,
-        null_message);
-
-    CHECK_RETURN(zero_value.is_not_nil());
-    code_assignt assignment(value_symbol.symbol_expr(), zero_value);
+    const auto zero_value =
+      zero_initializer(object_type, code.source_location(), ns);
+    CHECK_RETURN(zero_value.has_value());
+    code_assignt assignment(value_symbol.symbol_expr(), *zero_value);
     symex_assign(state, assignment);
   }
   else
@@ -242,7 +236,9 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   do_simplify(tmp);
   irep_idt id=get_symbol(tmp);
 
-  exprt rhs=zero_initializer(lhs.type(), code.source_location(), ns);
+  const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
+  CHECK_RETURN(zero.has_value());
+  exprt rhs(*zero);
 
   if(!id.empty())
   {
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index acd8791a871..c446b472bf8 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -115,7 +115,11 @@ void goto_symext::symex_start_thread(statet &state)
 
     exprt rhs=symbol.value;
     if(rhs.is_nil())
-      rhs=zero_initializer(symbol.type, symbol.location, ns);
+    {
+      const auto zero = zero_initializer(symbol.type, symbol.location, ns);
+      CHECK_RETURN(zero.has_value());
+      rhs = *zero;
+    }
 
     guardt guard;
     symex_assign_symbol(
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index ab9102b37f2..2ea40a00682 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -117,9 +117,9 @@ void static_lifetime_init(
     if(symbol.value.is_nil())
     {
       const namespacet ns(symbol_table);
-      rhs = zero_initializer(symbol.type, symbol.location, ns, message_handler);
-      INVARIANT(
-        rhs.is_not_nil(), "result of zero-initialization must be non-nil");
+      const auto zero = zero_initializer(symbol.type, symbol.location, ns);
+      CHECK_RETURN(zero.has_value());
+      rhs = *zero;
     }
     else
       rhs=symbol.value;
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 035488a6690..7bc07aa4d03 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -13,24 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "c_types.h"
-#include "format_expr.h"
-#include "format_type.h"
-#include "invariant.h"
-#include "message.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "std_code.h"
 #include "std_expr.h"
 
 template <bool nondet>
-class expr_initializert : public messaget
+class expr_initializert
 {
 public:
-  expr_initializert(
-    const namespacet &_ns,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    ns(_ns)
+  explicit expr_initializert(const namespacet &_ns) : ns(_ns)
   {
   }
 
@@ -56,10 +48,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
 {
   const irep_idt &type_id=type.id();
 
-  PRECONDITION_WITH_DIAGNOSTICS(
-    type_id != ID_code,
-    source_location.as_string() + ": cannot initialize code type");
-
   if(type_id==ID_unsignedbv ||
      type_id==ID_signedbv ||
      type_id==ID_pointer ||
@@ -118,6 +106,9 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     {
       exprt sub_zero =
         expr_initializer_rec(to_complex_type(type).subtype(), source_location);
+      if(sub_zero.is_nil())
+        return nil_exprt();
+
       result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
     }
 
@@ -142,6 +133,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     {
       exprt tmpval =
         expr_initializer_rec(array_type.subtype(), source_location);
+      if(tmpval.is_nil())
+        return nil_exprt();
 
       mp_integer array_size;
 
@@ -158,20 +151,12 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       {
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
-
-        std::ostringstream oss;
-        oss << format(array_type.size());
-
-        INVARIANT_WITH_DIAGNOSTICS(
-          false,
-          "non-infinite array size expression must be convertible to an "
-          "integer",
-          source_location.as_string() +
-            ": failed to zero-initialize array of size `" + oss.str() + "'");
+        else
+          return nil_exprt();
       }
 
-      DATA_INVARIANT(
-        array_size >= 0, "array should not have negative size");
+      if(array_size < 0)
+        return nil_exprt();
 
       array_exprt value(array_type);
       value.operands().resize(integer2size_t(array_size), tmpval);
@@ -184,6 +169,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     const vector_typet &vector_type=to_vector_type(type);
 
     exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
+    if(tmpval.is_nil())
+      return nil_exprt();
 
     mp_integer vector_size;
 
@@ -191,19 +178,12 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     {
       if(nondet)
         return side_effect_expr_nondett(type, source_location);
-
-      std::ostringstream oss;
-      oss << format(vector_type.size());
-
-      INVARIANT_WITH_DIAGNOSTICS(
-        false,
-        "vector size must be convertible to an integer",
-        source_location.as_string() +
-          ": failed to zero-initialize vector of size `" + oss.str() + "'");
+      else
+        return nil_exprt();
     }
 
-    DATA_INVARIANT(
-      vector_size >= 0, "vector should not have negative size");
+    if(vector_size < 0)
+      return nil_exprt();
 
     vector_exprt value(vector_type);
     value.operands().resize(integer2size_t(vector_size), tmpval);
@@ -229,7 +209,13 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         value.copy_to_operands(code_value);
       }
       else
-        value.copy_to_operands(expr_initializer_rec(c.type(), source_location));
+      {
+        const exprt member = expr_initializer_rec(c.type(), source_location);
+        if(member.is_nil())
+          return nil_exprt();
+
+        value.copy_to_operands(member);
+      }
     }
 
     value.add_source_location()=source_location;
@@ -277,6 +263,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       value.set_component_name(component.get_name());
       value.op()=
         expr_initializer_rec(component.type(), source_location);
+      if(value.op().is_nil())
+        return nil_exprt();
     }
 
     return value;
@@ -329,52 +317,44 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     return result;
   }
   else
-  {
-    std::ostringstream oss;
-    oss << format(type);
-
-    PRECONDITION_WITH_DIAGNOSTICS(
-      false,
-      source_location.as_string() + ": cannot initialize " + oss.str() + "'");
-  }
+    return nil_exprt();
 }
 
-exprt zero_initializer(
-  const typet &type,
-  const source_locationt &source_location,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  expr_initializert<false> z_i(ns, message_handler);
-  return z_i(type, source_location);
-}
-
-exprt nondet_initializer(
-  const typet &type,
-  const source_locationt &source_location,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  expr_initializert<true> z_i(ns, message_handler);
-  return z_i(type, source_location);
-}
-
-exprt zero_initializer(
+/// Create the equivalent of zero for type `type`.
+/// \param type: Type of the target expression.
+/// \param source_location: Location to record in all created sub-expressions.
+/// \param ns: Namespace to perform type symbol/tag lookups.
+/// \return An expression if a constant expression of the input type can be
+/// built.
+optionalt<exprt> zero_initializer(
   const typet &type,
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  null_message_handlert null_message_handler;
-  expr_initializert<false> z_i(ns, null_message_handler);
-  return z_i(type, source_location);
+  expr_initializert<false> z_i(ns);
+  const exprt result = z_i(type, source_location);
+  if(result.is_nil())
+    return {};
+  else
+    return result;
 }
 
-exprt nondet_initializer(
+/// Create a non-deterministic value for type `type`, with all subtypes
+/// independently expanded as non-deterministic values.
+/// \param type: Type of the target expression.
+/// \param source_location: Location to record in all created sub-expressions.
+/// \param ns: Namespace to perform type symbol/tag lookups.
+/// \return An expression if a non-deterministic expression of the input type
+/// can be built.
+optionalt<exprt> nondet_initializer(
   const typet &type,
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  null_message_handlert null_message_handler;
-  expr_initializert<true> z_i(ns, null_message_handler);
-  return z_i(type, source_location);
+  expr_initializert<true> z_i(ns);
+  const exprt result = z_i(type, source_location);
+  if(result.is_nil())
+    return {};
+  else
+    return result;
 }
diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h
index 696c0d9c3fe..bc61ed1ceb0 100644
--- a/src/util/expr_initializer.h
+++ b/src/util/expr_initializer.h
@@ -13,30 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_EXPR_INITIALIZER_H
 
 #include "expr.h"
+#include "optional.h"
 
 class message_handlert;
 class namespacet;
 class source_locationt;
 
-exprt zero_initializer(
-  const typet &,
-  const source_locationt &,
-  const namespacet &,
-  message_handlert &);
-
-exprt nondet_initializer(
-  const typet &,
-  const source_locationt &,
-  const namespacet &,
-  message_handlert &);
-
-// throws a char* in case of failure
-exprt zero_initializer(
-  const typet &,
-  const source_locationt &,
-  const namespacet &);
-
-exprt nondet_initializer(
+optionalt<exprt>
+zero_initializer(const typet &, const source_locationt &, const namespacet &);
+
+optionalt<exprt> nondet_initializer(
   const typet &type,
   const source_locationt &source_location,
   const namespacet &ns);