diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 69758351b3f..52f79249fad 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -21,12 +21,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_language.h"
 #include "java_utils.h"
 
-#include <util/c_types.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
-
-#include <linking/zero_initializer.h>
 #include <util/suffix.h>
 
 class java_bytecode_convert_classt:public messaget
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 6669e0e05a2..a6f2996a215 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
@@ -32,8 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
-#include <linking/zero_initializer.h>
-
 #include <goto-programs/cfg.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
index 6fa16827fe9..83dcaa6dd9b 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -12,10 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_typecheck.h"
 
 #include <util/arith_tools.h>
+#include <util/expr_initializer.h>
 #include <util/unicode.h>
 
-#include <linking/zero_initializer.h>
-
 #include "java_pointer_casts.h"
 #include "java_types.h"
 #include "java_utils.h"
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index b8ed2371242..14329aaaba4 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_object_factory.h"
 
+#include <util/expr_initializer.h>
 #include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
 #include <util/pointer_offset_size.h>
@@ -15,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
-#include <linking/zero_initializer.h>
-
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
 
diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp
index ca6832b4f2c..b4de86b1cd4 100644
--- a/jbmc/src/java_bytecode/java_string_literals.cpp
+++ b/jbmc/src/java_bytecode/java_string_literals.cpp
@@ -11,9 +11,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "java_types.h"
 #include "java_utils.h"
 
-#include <linking/zero_initializer.h>
-
 #include <util/arith_tools.h>
+#include <util/expr_initializer.h>
 #include <util/namespace.h>
 #include <util/unicode.h>
 
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
index 1d88c7ddbcd..d6676d678dd 100644
--- a/jbmc/src/java_bytecode/remove_java_new.cpp
+++ b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -14,11 +14,10 @@ Author: Peter Schrammel
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
-#include <linking/zero_initializer.h>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_cast.h>
+#include <util/expr_initializer.h>
 #include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index c025aa1fb6b..31eda7a4c33 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_typecheck_base.h"
 
 #include <util/config.h>
+#include <util/expr_initializer.h>
 
 #include "ansi_c_declaration.h"
 
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 6fea7bc9c77..977ad82f43f 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -14,14 +14,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 #include <util/type_eq.h>
 
-#include <linking/zero_initializer.h>
-
 #include "anonymous_member.h"
 
 void c_typecheck_baset::do_initializer(
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index 549a5b6d77d..16d307e2324 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -14,10 +14,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/expr_initializer.h>
 #include <util/source_location.h>
 #include <util/symbol.h>
 
-#include <linking/zero_initializer.h>
 #include <ansi-c/c_typecast.h>
 
 #include "expr2cpp.h"
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 75aebd7f4b4..1476b0e2028 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -19,12 +19,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
 
 #include <ansi-c/c_qualifiers.h>
 
-#include <linking/zero_initializer.h>
-
 #include "cpp_exception_id.h"
 #include "cpp_type2name.h"
 #include "expr2cpp.h"
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index c4c85637878..adc598e855c 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -13,10 +13,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
 
-#include <linking/zero_initializer.h>
-
 /// Initialize an object with a value
 void cpp_typecheckt::convert_initializer(symbolt &symbol)
 {
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index e530536a892..6a132bf88bb 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -14,6 +14,7 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/magic.h>
 #include <util/run.h>
 #include <util/tempfile.h>
@@ -21,7 +22,6 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2017
 #include <json/json_parser.h>
 
 #include <linking/static_lifetime_init.h>
-#include <linking/zero_initializer.h>
 
 #include <goto-programs/read_goto_binary.h>
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 934b610e728..74bf5ede7a4 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -16,12 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.h>
 #include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
 
-#include <linking/zero_initializer.h>
-
 #include <langapi/language_util.h>
 
 #include "format_strings.h"
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 1fff82d17fa..0d6455dc142 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -13,13 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_initializer.h>
 #include <util/invariant_utils.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
 
-#include <linking/zero_initializer.h>
-
 inline static typet c_sizeof_type_rec(const exprt &expr)
 {
   const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 4b672574aab..9986812598e 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <linking/zero_initializer.h>
+#include <util/expr_initializer.h>
 
 void goto_symext::symex_start_thread(statet &state)
 {
diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt
index f33232fd156..4534ff02476 100644
--- a/src/linking/CMakeLists.txt
+++ b/src/linking/CMakeLists.txt
@@ -3,4 +3,4 @@ add_library(linking ${sources})
 
 generic_includes(linking)
 
-target_link_libraries(linking util ansi-c)
+target_link_libraries(linking util)
diff --git a/src/linking/Makefile b/src/linking/Makefile
index a2030500ec4..f1a52517dae 100644
--- a/src/linking/Makefile
+++ b/src/linking/Makefile
@@ -1,7 +1,6 @@
 SRC = linking.cpp \
       remove_internal_symbols.cpp \
       static_lifetime_init.cpp \
-      zero_initializer.cpp \
       # Empty last line
 
 INCLUDES= -I ..
diff --git a/src/linking/module_dependencies.txt b/src/linking/module_dependencies.txt
index e5b9de47bd8..c686b60d2d7 100644
--- a/src/linking/module_dependencies.txt
+++ b/src/linking/module_dependencies.txt
@@ -1,4 +1,3 @@
-ansi-c # should go away
 goto-programs
 langapi # should go away
 linking
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index 8178f839ea1..3da62aec260 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -11,19 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <cstdlib>
 
-#include <util/namespace.h>
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
-#include <util/std_code.h>
+#include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_initializer.h>
+#include <util/namespace.h>
 #include <util/prefix.h>
-
-#include <util/c_types.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <goto-programs/goto_functions.h>
 
-#include "zero_initializer.h"
-
 bool static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
diff --git a/src/util/Makefile b/src/util/Makefile
index 6afa460e650..10e7c6b3125 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -11,6 +11,7 @@ SRC = arith_tools.cpp \
       dstring.cpp \
       endianness_map.cpp \
       expr.cpp \
+      expr_initializer.cpp \
       expr_util.cpp \
       file_util.cpp \
       find_macros.cpp \
diff --git a/src/linking/zero_initializer.cpp b/src/util/expr_initializer.cpp
similarity index 60%
rename from src/linking/zero_initializer.cpp
rename to src/util/expr_initializer.cpp
index 675cdb7dd7f..e7504dd861d 100644
--- a/src/linking/zero_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -1,29 +1,32 @@
 /*******************************************************************\
 
-Module: Linking: Zero Initialization
+Module: Expression Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Linking: Zero Initialization
-
-#include "zero_initializer.h"
-
-#include <util/arith_tools.h>
-#include <util/c_types.h>
-#include <util/message.h>
-#include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/std_expr.h>
-
-#include <ansi-c/expr2c.h>
-
-class zero_initializert:public messaget
+/// Expression Initialization
+
+#include "expr_initializer.h"
+
+#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
 {
 public:
-  zero_initializert(
+  expr_initializert(
     const namespacet &_ns,
     message_handlert &_message_handler):
     messaget(_message_handler),
@@ -35,28 +38,19 @@ class zero_initializert:public messaget
     const typet &type,
     const source_locationt &source_location)
   {
-    return zero_initializer_rec(type, source_location);
+    return expr_initializer_rec(type, source_location);
   }
 
 protected:
   const namespacet &ns;
 
-  std::string to_string(const exprt &src)
-  {
-    return expr2c(src, ns);
-  }
-
-  std::string to_string(const typet &src)
-  {
-    return type2c(src, ns);
-  }
-
-  exprt zero_initializer_rec(
+  exprt expr_initializer_rec(
     const typet &type,
     const source_locationt &source_location);
 };
 
-exprt zero_initializert::zero_initializer_rec(
+template <bool nondet>
+exprt expr_initializert<nondet>::expr_initializer_rec(
   const typet &type,
   const source_locationt &source_location)
 {
@@ -73,38 +67,62 @@ exprt zero_initializert::zero_initializer_rec(
      type_id==ID_floatbv ||
      type_id==ID_fixedbv)
   {
-    exprt result=from_integer(0, type);
+    exprt result;
+    if(nondet)
+      result = side_effect_expr_nondett(type);
+    else
+      result = from_integer(0, type);
+
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_rational ||
           type_id==ID_real)
   {
-    constant_exprt result(ID_0, type);
+    exprt result;
+    if(nondet)
+      result = side_effect_expr_nondett(type);
+    else
+      result = constant_exprt(ID_0, type);
+
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_verilog_signedbv ||
           type_id==ID_verilog_unsignedbv)
   {
-    std::size_t width=to_bitvector_type(type).get_width();
-    std::string value(width, '0');
+    exprt result;
+    if(nondet)
+      result = side_effect_expr_nondett(type);
+    else
+    {
+      const std::size_t width = to_bitvector_type(type).get_width();
+      std::string value(width, '0');
+
+      result = constant_exprt(value, type);
+    }
 
-    constant_exprt result(value, type);
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_complex)
   {
-    exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
-    complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
+    exprt result;
+    if(nondet)
+      result = side_effect_expr_nondett(type);
+    else
+    {
+      exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
+      result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
+    }
+
     result.add_source_location()=source_location;
     return result;
   }
   else if(type_id==ID_code)
   {
     error().source_location=source_location;
-    error() << "cannot zero-initialize code-type" << eom;
+    error() << "cannot initialize code-type" << eom;
     throw 0;
   }
   else if(type_id==ID_array)
@@ -123,34 +141,44 @@ exprt zero_initializert::zero_initializer_rec(
     }
     else
     {
-      exprt tmpval=zero_initializer_rec(array_type.subtype(), source_location);
+      exprt tmpval =
+        expr_initializer_rec(array_type.subtype(), source_location);
 
       mp_integer array_size;
 
       if(array_type.size().id()==ID_infinity)
       {
+        if(nondet)
+        {
+          side_effect_expr_nondett result(type);
+          result.add_source_location() = source_location;
+          return result;
+        }
+
         array_of_exprt value(tmpval, array_type);
         value.add_source_location()=source_location;
         return value;
       }
       else if(to_integer(array_type.size(), array_size))
       {
+        if(nondet)
+        {
+          side_effect_expr_nondett result(type);
+          result.add_source_location() = source_location;
+          return result;
+        }
+
         error().source_location=source_location;
         error() << "failed to zero-initialize array of non-fixed size `"
-                << to_string(array_type.size()) << "'" << eom;
+                << format(array_type.size()) << "'" << eom;
         throw 0;
       }
 
-      if(array_size<0)
-      {
-        error().source_location=source_location;
-        error() << "failed to zero-initialize array of with negative size"
-                << eom;
-        throw 0;
-      }
+      DATA_INVARIANT(
+        array_size >= 0, "array should not have negative size");
 
       array_exprt value(array_type);
-      value.operands().resize(integer2unsigned(array_size), tmpval);
+      value.operands().resize(integer2size_t(array_size), tmpval);
       value.add_source_location()=source_location;
       return value;
     }
@@ -159,28 +187,30 @@ exprt zero_initializert::zero_initializer_rec(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    exprt tmpval=zero_initializer_rec(vector_type.subtype(), source_location);
+    exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
 
     mp_integer vector_size;
 
     if(to_integer(vector_type.size(), vector_size))
     {
+      if(nondet)
+      {
+        side_effect_expr_nondett result(type);
+        result.add_source_location() = source_location;
+        return result;
+      }
+
       error().source_location=source_location;
       error() << "failed to zero-initialize vector of non-fixed size `"
-              << to_string(vector_type.size()) << "'" << eom;
+              << format(vector_type.size()) << "'" << eom;
       throw 0;
     }
 
-    if(vector_size<0)
-    {
-      error().source_location=source_location;
-      error() << "failed to zero-initialize vector of with negative size"
-              << eom;
-      throw 0;
-    }
+    DATA_INVARIANT(
+      vector_size >= 0, "vector should not have negative size");
 
     vector_exprt value(vector_type);
-    value.operands().resize(integer2unsigned(vector_size), tmpval);
+    value.operands().resize(integer2size_t(vector_size), tmpval);
     value.add_source_location()=source_location;
 
     return value;
@@ -207,7 +237,7 @@ exprt zero_initializert::zero_initializer_rec(
       }
       else
         value.copy_to_operands(
-          zero_initializer_rec(it->type(), source_location));
+          expr_initializer_rec(it->type(), source_location));
     }
 
     value.add_source_location()=source_location;
@@ -257,14 +287,14 @@ exprt zero_initializert::zero_initializer_rec(
     {
       value.set_component_name(component.get_name());
       value.op()=
-        zero_initializer_rec(component.type(), source_location);
+        expr_initializer_rec(component.type(), source_location);
     }
 
     return value;
   }
   else if(type_id==ID_symbol)
   {
-    exprt result=zero_initializer_rec(ns.follow(type), source_location);
+    exprt result = expr_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
     if(ns.follow(type).id()!=ID_array)
       result.type()=type;
@@ -274,33 +304,39 @@ exprt zero_initializert::zero_initializer_rec(
   else if(type_id==ID_c_enum_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_c_enum_tag_type(type)),
         source_location);
   }
   else if(type_id==ID_struct_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_struct_tag_type(type)),
         source_location);
   }
   else if(type_id==ID_union_tag)
   {
     return
-      zero_initializer_rec(
+      expr_initializer_rec(
         ns.follow_tag(to_union_tag_type(type)),
         source_location);
   }
   else if(type_id==ID_string)
   {
-    return constant_exprt(irep_idt(), type);
+    exprt result;
+    if(nondet)
+      result = side_effect_expr_nondett(type);
+    else
+      result = constant_exprt(irep_idt(), type);
+
+    result.add_source_location()=source_location;
+    return result;
   }
   else
   {
     error().source_location=source_location;
-    error() << "failed to zero-initialize `" << to_string(type)
-            << "'" << eom;
+    error() << "failed to initialize `" << format(type) << "'" << eom;
     throw 0;
   }
 }
@@ -311,7 +347,17 @@ exprt zero_initializer(
   const namespacet &ns,
   message_handlert &message_handler)
 {
-  zero_initializert z_i(ns, 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);
 }
 
@@ -325,7 +371,26 @@ exprt zero_initializer(
 
   try
   {
-    zero_initializert z_i(ns, mh);
+    expr_initializert<false> z_i(ns, mh);
+    return z_i(type, source_location);
+  }
+  catch(int)
+  {
+    throw oss.str();
+  }
+}
+
+exprt nondet_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns)
+{
+  std::ostringstream oss;
+  stream_message_handlert mh(oss);
+
+  try
+  {
+    expr_initializert<true> z_i(ns, mh);
     return z_i(type, source_location);
   }
   catch(int)
diff --git a/src/linking/zero_initializer.h b/src/util/expr_initializer.h
similarity index 54%
rename from src/linking/zero_initializer.h
rename to src/util/expr_initializer.h
index 3bb440b8b74..696c0d9c3fe 100644
--- a/src/linking/zero_initializer.h
+++ b/src/util/expr_initializer.h
@@ -1,18 +1,18 @@
 /*******************************************************************\
 
-Module: Linking: Zero Initialization
+Module: Expression Initialization
 
 Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
 /// \file
-/// Linking: Zero Initialization
+/// Expression Initialization
 
-#ifndef CPROVER_LINKING_ZERO_INITIALIZER_H
-#define CPROVER_LINKING_ZERO_INITIALIZER_H
+#ifndef CPROVER_UTIL_EXPR_INITIALIZER_H
+#define CPROVER_UTIL_EXPR_INITIALIZER_H
 
-#include <util/expr.h>
+#include "expr.h"
 
 class message_handlert;
 class namespacet;
@@ -24,10 +24,21 @@ exprt zero_initializer(
   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 &);
 
-#endif // CPROVER_LINKING_ZERO_INITIALIZER_H
+exprt nondet_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns);
+
+#endif // CPROVER_UTIL_EXPR_INITIALIZER_H