diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index c42fd975170..db03b94672f 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -177,8 +177,7 @@ bool ansi_c_entry_point(
     return false; // give up
   }
 
-  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
-    return true;
+  static_lifetime_init(symbol_table, symbol.location, message_handler);
 
   return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
 }
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index c79e861fc46..0bd3254fbae 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -22,17 +22,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_functions.h>
 
-bool static_lifetime_init(
+void static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
   message_handlert &message_handler)
 {
-  namespacet ns(symbol_table);
+  PRECONDITION(symbol_table.has_symbol(INITIALIZE_FUNCTION));
 
-  const auto maybe_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION);
-  if(!maybe_symbol)
-    return false;
-  symbolt &init_symbol=*maybe_symbol;
+  const namespacet ns(symbol_table);
+
+  symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
 
   init_symbol.value=code_blockt();
   init_symbol.value.add_source_location()=source_location;
@@ -117,16 +116,10 @@ bool static_lifetime_init(
 
     if(symbol.value.is_nil())
     {
-      try
-      {
-        namespacet ns(symbol_table);
-        rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
-        assert(rhs.is_not_nil());
-      }
-      catch(...)
-      {
-        return true;
-      }
+      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");
     }
     else
       rhs=symbol.value;
@@ -156,6 +149,4 @@ bool static_lifetime_init(
       dest.move_to_operands(function_call);
     }
   }
-
-  return false;
 }
diff --git a/src/linking/static_lifetime_init.h b/src/linking/static_lifetime_init.h
index 829e2e16a05..b591727a903 100644
--- a/src/linking/static_lifetime_init.h
+++ b/src/linking/static_lifetime_init.h
@@ -16,7 +16,7 @@ class message_handlert;
 class source_locationt;
 class symbol_tablet;
 
-bool static_lifetime_init(
+void static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
   message_handlert &message_handler);
diff --git a/src/util/array_name.cpp b/src/util/array_name.cpp
index 450b95b3713..731a41a84d9 100644
--- a/src/util/array_name.cpp
+++ b/src/util/array_name.cpp
@@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "array_name.h"
 
 #include "expr.h"
+#include "invariant.h"
 #include "namespace.h"
-#include "symbol.h"
 #include "ssa_expr.h"
+#include "symbol.h"
 
 std::string array_name(
   const namespacet &ns,
@@ -22,10 +23,7 @@ std::string array_name(
 {
   if(expr.id()==ID_index)
   {
-    if(expr.operands().size()!=2)
-      throw "index takes two operands";
-
-    return array_name(ns, expr.op0())+"[]";
+    return array_name(ns, to_index_expr(expr).array()) + "[]";
   }
   else if(is_ssa_expr(expr))
   {
@@ -44,9 +42,10 @@ std::string array_name(
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    return array_name(ns, expr.op0())+"."+
-           expr.get_string(ID_component_name);
+    const member_exprt &member_expr = to_member_expr(expr);
+
+    return array_name(ns, member_expr.compound()) + "." +
+           id2string(member_expr.get_component_name());
   }
 
   return "array";
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
index b1b902ef2ae..107b9f1e434 100644
--- a/src/util/bv_arithmetic.cpp
+++ b/src/util/bv_arithmetic.cpp
@@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_arithmetic.h"
 
-#include <cassert>
 #include <ostream>
 
 #include "string2int.h"
@@ -90,7 +89,7 @@ exprt bv_arithmetict::to_expr() const
 
 bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
 {
-  assert(other.spec==spec);
+  PRECONDITION(other.spec == spec);
 
   if(other.value==0)
     value=0;
@@ -102,7 +101,7 @@ bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
 
 bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
 {
-  assert(other.spec==spec);
+  PRECONDITION(other.spec == spec);
 
   value*=other.value;
   adjust();
@@ -112,7 +111,7 @@ bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
 
 bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
 {
-  assert(other.spec==spec);
+  PRECONDITION(other.spec == spec);
 
   value+=other.value;
   adjust();
@@ -122,7 +121,7 @@ bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
 
 bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
 {
-  assert(other.spec==spec);
+  PRECONDITION(other.spec == spec);
 
   value-=other.value;
   adjust();
@@ -132,7 +131,7 @@ bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
 
 bv_arithmetict &bv_arithmetict::operator%=(const bv_arithmetict &other)
 {
-  assert(other.spec==spec);
+  PRECONDITION(other.spec == spec);
 
   value%=other.value;
   adjust();
@@ -183,7 +182,7 @@ void bv_arithmetict::change_spec(const bv_spect &dest_spec)
 
 void bv_arithmetict::from_expr(const exprt &expr)
 {
-  assert(expr.is_constant());
+  PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
   value=binary2integer(expr.get_string(ID_value), spec.is_signed);
 }
diff --git a/src/util/byte_operators.cpp b/src/util/byte_operators.cpp
index 74aa67e53d7..ea5a2c6febe 100644
--- a/src/util/byte_operators.cpp
+++ b/src/util/byte_operators.cpp
@@ -8,9 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "byte_operators.h"
 
-#include <cassert>
-
-#include "invariant.h"
 #include "config.h"
 
 irep_idt byte_extract_id()
diff --git a/src/util/byte_operators.h b/src/util/byte_operators.h
index ec855836b51..f999be2bd1c 100644
--- a/src/util/byte_operators.h
+++ b/src/util/byte_operators.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
+#include "invariant.h"
 #include "std_expr.h"
 
 /*! \brief TO_BE_DOCUMENTED
@@ -51,13 +52,13 @@ class byte_extract_exprt:public binary_exprt
 
 inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size() == 2);
   return static_cast<const byte_extract_exprt &>(expr);
 }
 
 inline byte_extract_exprt &to_byte_extract_expr(exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size() == 2);
   return static_cast<byte_extract_exprt &>(expr);
 }
 
@@ -78,14 +79,20 @@ class byte_extract_little_endian_exprt:public byte_extract_exprt
 inline const byte_extract_little_endian_exprt
   &to_byte_extract_little_endian_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_byte_extract_little_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "byte extract expressions have two operands");
+
   return static_cast<const byte_extract_little_endian_exprt &>(expr);
 }
 
 inline byte_extract_little_endian_exprt
   &to_byte_extract_little_endian_expr(exprt &expr)
 {
-  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_byte_extract_little_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "byte extract expressions have two operands");
+
   return static_cast<byte_extract_little_endian_exprt &>(expr);
 }
 
@@ -109,14 +116,20 @@ class byte_extract_big_endian_exprt:public byte_extract_exprt
 inline const byte_extract_big_endian_exprt
   &to_byte_extract_big_endian_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_byte_extract_big_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "byte extract expressions have two operands");
+
   return static_cast<const byte_extract_big_endian_exprt &>(expr);
 }
 
 inline byte_extract_big_endian_exprt
   &to_byte_extract_big_endian_expr(exprt &expr)
 {
-  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_byte_extract_big_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "byte extract expressions have two operands");
+
   return static_cast<byte_extract_big_endian_exprt &>(expr);
 }
 
@@ -154,13 +167,13 @@ class byte_update_exprt : public ternary_exprt
 
 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==3);
+  PRECONDITION(expr.operands().size() == 3);
   return static_cast<const byte_update_exprt &>(expr);
 }
 
 inline byte_update_exprt &to_byte_update_expr(exprt &expr)
 {
-  assert(expr.operands().size()==3);
+  PRECONDITION(expr.operands().size() == 3);
   return static_cast<byte_update_exprt &>(expr);
 }
 
@@ -184,14 +197,20 @@ class byte_update_little_endian_exprt:public byte_update_exprt
 inline const byte_update_little_endian_exprt
   &to_byte_update_little_endian_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
+  PRECONDITION(expr.id() == ID_byte_update_little_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "byte update expressions have three operands");
+
   return static_cast<const byte_update_little_endian_exprt &>(expr);
 }
 
 inline byte_update_little_endian_exprt
   &to_byte_update_little_endian_expr(exprt &expr)
 {
-  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
+  PRECONDITION(expr.id() == ID_byte_update_little_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "byte update expressions have three operands");
+
   return static_cast<byte_update_little_endian_exprt &>(expr);
 }
 
@@ -215,14 +234,20 @@ class byte_update_big_endian_exprt:public byte_update_exprt
 inline const byte_update_big_endian_exprt
   &to_byte_update_big_endian_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
+  PRECONDITION(expr.id() == ID_byte_update_big_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "byte update expressions have three operands");
+
   return static_cast<const byte_update_big_endian_exprt &>(expr);
 }
 
 inline byte_update_big_endian_exprt
   &to_byte_update_big_endian_expr(exprt &expr)
 {
-  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
+  PRECONDITION(expr.id() == ID_byte_update_big_endian);
+  DATA_INVARIANT(
+    expr.operands().size() == 3, "byte update expressions have three operands");
+
   return static_cast<byte_update_big_endian_exprt &>(expr);
 }
 
diff --git a/src/util/config.cpp b/src/util/config.cpp
index abf10afae0e..4ab30d8198a 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -10,15 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cstdlib>
 
-#include "namespace.h"
-#include "symbol_table.h"
 #include "arith_tools.h"
 #include "cmdline.h"
+#include "cprover_prefix.h"
+#include "exception_utils.h"
+#include "namespace.h"
 #include "simplify_expr.h"
 #include "std_expr.h"
-#include "cprover_prefix.h"
 #include "string2int.h"
 #include "string_utils.h"
+#include "symbol_table.h"
 
 configt config;
 
@@ -945,20 +946,42 @@ bool configt::set(const cmdlinet &cmdline)
   // the same architecture and OS that we are verifying for.
   if(arch==this_arch && os==this_os)
   {
-    assert(ansi_c.int_width==sizeof(int)*8);
-    assert(ansi_c.long_int_width==sizeof(long)*8);
-    assert(ansi_c.bool_width==sizeof(bool)*8);
-    assert(ansi_c.char_width==sizeof(char)*8);
-    assert(ansi_c.short_int_width==sizeof(short)*8);
-    assert(ansi_c.long_long_int_width==sizeof(long long)*8);
-    assert(ansi_c.pointer_width==sizeof(void *)*8);
-    assert(ansi_c.single_width==sizeof(float)*8);
-    assert(ansi_c.double_width==sizeof(double)*8);
-    assert(ansi_c.char_is_unsigned==(static_cast<char>(255)==255));
+    INVARIANT(
+      ansi_c.int_width == sizeof(int) * 8,
+      "int width shall be equal to the system int width");
+    INVARIANT(
+      ansi_c.long_int_width == sizeof(long) * 8,
+      "long int width shall be equal to the system long int width");
+    INVARIANT(
+      ansi_c.bool_width == sizeof(bool) * 8,
+      "bool width shall be equal to the system bool width");
+    INVARIANT(
+      ansi_c.char_width == sizeof(char) * 8,
+      "char width shall be equal to the system char width");
+    INVARIANT(
+      ansi_c.short_int_width == sizeof(short) * 8,
+      "short int width shall be equal to the system short int width");
+    INVARIANT(
+      ansi_c.long_long_int_width == sizeof(long long) * 8,
+      "long long int width shall be equal to the system long long int width");
+    INVARIANT(
+      ansi_c.pointer_width == sizeof(void *) * 8,
+      "pointer width shall be equal to the system pointer width");
+    INVARIANT(
+      ansi_c.single_width == sizeof(float) * 8,
+      "float width shall be equal to the system float width");
+    INVARIANT(
+      ansi_c.double_width == sizeof(double) * 8,
+      "double width shall be equal to the system double width");
+    INVARIANT(
+      ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
+      "char_is_unsigned flag shall indicate system char unsignedness");
 
     #ifndef _WIN32
     // On Windows, long double width varies by compiler
-    assert(ansi_c.long_double_width==sizeof(long double)*8);
+    INVARIANT(
+      ansi_c.long_double_width == sizeof(long double) * 8,
+      "long double width shall be equal to the system long double width");
     #endif
   }
 
@@ -1026,14 +1049,17 @@ bool configt::set(const cmdlinet &cmdline)
   {
     bv_encoding.object_bits=
       unsafe_string2unsigned(cmdline.get_value("object-bits"));
-    bv_encoding.is_object_bits_default=false;
 
     if(!(0<bv_encoding.object_bits &&
          bv_encoding.object_bits<ansi_c.pointer_width))
     {
-      throw "object-bits must be positive and less than the pointer width ("+
-        std::to_string(ansi_c.pointer_width)+") ";
+      throw invalid_user_input_exceptiont(
+        "object-bits must be positive and less than the pointer width (" +
+          std::to_string(ansi_c.pointer_width) + ") ",
+        "--object_bits");
     }
+
+    bv_encoding.is_object_bits_default = false;
   }
 
   return false;
@@ -1069,21 +1095,17 @@ static irep_idt string_from_ns(
   const irep_idt id=CPROVER_PREFIX "architecture_"+what;
   const symbolt *symbol;
 
-  if(ns.lookup(id, symbol))
-    throw "failed to find "+id2string(id);
+  const bool not_found = ns.lookup(id, symbol);
+  INVARIANT(!not_found, id2string(id) + " must be in namespace");
 
   const exprt &tmp=symbol->value;
 
-  if(tmp.id()!=ID_address_of ||
-     tmp.operands().size()!=1 ||
-     tmp.op0().id()!=ID_index ||
-     tmp.op0().operands().size()!=2 ||
-     tmp.op0().op0().id()!=ID_string_constant)
-  {
-    throw
-      "symbol table configuration entry `"+id2string(id)+
-      "' is not a string constant";
-  }
+  INVARIANT(
+    tmp.id() == ID_address_of && tmp.operands().size() == 1 &&
+      tmp.op0().id() == ID_index && tmp.op0().operands().size() == 2 &&
+      tmp.op0().op0().id() == ID_string_constant,
+    "symbol table configuration entry `" + id2string(id) +
+      "' must be a string constant");
 
   return tmp.op0().op0().get(ID_value);
 }
@@ -1095,21 +1117,24 @@ static unsigned unsigned_from_ns(
   const irep_idt id=CPROVER_PREFIX "architecture_"+what;
   const symbolt *symbol;
 
-  if(ns.lookup(id, symbol))
-    throw "failed to find "+id2string(id);
+  const bool not_found = ns.lookup(id, symbol);
+  INVARIANT(!not_found, id2string(id) + " must be in namespace");
 
   exprt tmp=symbol->value;
   simplify(tmp, ns);
 
-  if(tmp.id()!=ID_constant)
-    throw
-      "symbol table configuration entry `"+id2string(id)+"' is not a constant";
+  INVARIANT(
+    tmp.id() == ID_constant,
+    "symbol table configuration entry `" + id2string(id) +
+      "' must be a constant");
 
   mp_integer int_value;
 
-  if(to_integer(to_constant_expr(tmp), int_value))
-    throw
-      "failed to convert symbol table configuration entry `"+id2string(id)+"'";
+  const bool error = to_integer(to_constant_expr(tmp), int_value);
+  INVARIANT(
+    !error,
+    "symbol table configuration entry `" + id2string(id) +
+      "' must be convertible to mp_integer");
 
   return integer2unsigned(int_value);
 }
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index d526d3c4c74..12d9a3f488b 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ostream>
 
-#include "invariant.h"
 #include "std_types.h"
 #include "pointer_offset_size.h"
 #include "arith_tools.h"
diff --git a/src/util/endianness_map.h b/src/util/endianness_map.h
index 2de432a9c88..801fa0d65ba 100644
--- a/src/util/endianness_map.h
+++ b/src/util/endianness_map.h
@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 #include <vector>
 
+#include "invariant.h"
+
 class namespacet;
 class typet;
 
@@ -45,9 +47,9 @@ class endianness_mapt
 
   size_t map_bit(size_t bit) const
   {
-    assert(bit<map.size());
+    PRECONDITION(bit < map.size());
     size_t result=map[bit];
-    assert(result<map.size());
+    DATA_INVARIANT(result < map.size(), "bit index must be within bounds");
     return result;
   }
 
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index b089db327c0..75f8b89b053 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -56,6 +56,10 @@ 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 ||
@@ -119,12 +123,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     result.add_source_location()=source_location;
     return result;
   }
-  else if(type_id==ID_code)
-  {
-    error().source_location=source_location;
-    error() << "cannot initialize code-type" << eom;
-    throw 0;
-  }
   else if(type_id==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
@@ -160,10 +158,15 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
 
-        error().source_location=source_location;
-        error() << "failed to zero-initialize array of non-fixed size `"
-                << format(array_type.size()) << "'" << eom;
-        throw 0;
+        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() + "'");
       }
 
       DATA_INVARIANT(
@@ -188,10 +191,14 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       if(nondet)
         return side_effect_expr_nondett(type, source_location);
 
-      error().source_location=source_location;
-      error() << "failed to zero-initialize vector of non-fixed size `"
-              << format(vector_type.size()) << "'" << eom;
-      throw 0;
+      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() + "'");
     }
 
     DATA_INVARIANT(
@@ -322,9 +329,12 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   }
   else
   {
-    error().source_location=source_location;
-    error() << "failed to initialize `" << format(type) << "'" << eom;
-    throw 0;
+    std::ostringstream oss;
+    oss << format(type);
+
+    PRECONDITION_WITH_DIAGNOSTICS(
+      false,
+      source_location.as_string() + ": cannot initialize " + oss.str() + "'");
   }
 }
 
@@ -353,18 +363,9 @@ exprt zero_initializer(
   const source_locationt &source_location,
   const namespacet &ns)
 {
-  std::ostringstream oss;
-  stream_message_handlert mh(oss);
-
-  try
-  {
-    expr_initializert<false> z_i(ns, mh);
-    return z_i(type, source_location);
-  }
-  catch(int)
-  {
-    throw oss.str();
-  }
+  null_message_handlert null_message_handler;
+  expr_initializert<false> z_i(ns, null_message_handler);
+  return z_i(type, source_location);
 }
 
 exprt nondet_initializer(
@@ -372,16 +373,7 @@ exprt nondet_initializer(
   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)
-  {
-    throw oss.str();
-  }
+  null_message_handlert null_message_handler;
+  expr_initializert<true> z_i(ns, null_message_handler);
+  return z_i(type, source_location);
 }
diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp
index cafbc30f12e..f38aa64e86c 100644
--- a/src/util/file_util.cpp
+++ b/src/util/file_util.cpp
@@ -13,7 +13,7 @@ Date: January 2012
 
 #include "file_util.h"
 
-#include "invariant.h"
+#include "exception_utils.h"
 
 #include <cerrno>
 #include <cstring>
@@ -53,16 +53,18 @@ std::string get_current_working_directory()
   #ifndef _WIN32
   errno=0;
   char *wd=realpath(".", nullptr);
-  INVARIANT(
-    wd!=nullptr && errno==0,
-    std::string("realpath failed: ")+strerror(errno));
+
+  if(wd == nullptr || errno != 0)
+    throw system_exceptiont(
+      std::string("realpath failed: ") + std::strerror(errno));
 
   std::string working_directory=wd;
   free(wd);
   #else
   char buffer[4096];
   DWORD retval=GetCurrentDirectory(4096, buffer);
-  CHECK_RETURN(retval>0);
+  if(retval == 0)
+    throw system_exceptiont("failed to get current directory of process");
   std::string working_directory(buffer);
   #endif
 
@@ -118,7 +120,8 @@ void delete_directory(const std::string &path)
       struct stat stbuf;
       int result=stat(sub_path.c_str(), &stbuf);
       if(result!=0)
-        throw std::string("Stat failed: ")+std::strerror(errno);
+        throw system_exceptiont(
+          std::string("Stat failed: ") + std::strerror(errno));
 
       if(S_ISDIR(stbuf.st_mode))
         delete_directory(sub_path);
@@ -126,7 +129,8 @@ void delete_directory(const std::string &path)
       {
         result=remove(sub_path.c_str());
         if(result!=0)
-          throw std::string("Remove failed: ")+std::strerror(errno);
+          throw system_exceptiont(
+            std::string("Remove failed: ") + std::strerror(errno));
       }
     }
     closedir(dir);
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index d5af3609d90..02b441badb4 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -45,7 +45,7 @@ constant_exprt fixedbvt::to_expr() const
   fixedbv_typet type;
   type.set_width(spec.width);
   type.set_integer_bits(spec.integer_bits);
-  assert(spec.width!=0);
+  PRECONDITION(spec.width != 0);
   return constant_exprt(integer2binary(v, spec.width), type);
 }
 
diff --git a/src/util/format_number_range.cpp b/src/util/format_number_range.cpp
index 2c4c54d1da3..15173fa6fbf 100644
--- a/src/util/format_number_range.cpp
+++ b/src/util/format_number_range.cpp
@@ -66,6 +66,6 @@ std::string format_number_range(const std::vector<unsigned> &input_numbers)
       start_number = *next;
   }
 
-  CHECK_RETURN(!number_range.str().empty());
+  POSTCONDITION(!number_range.str().empty());
   return number_range.str();
 }
diff --git a/src/util/graph.h b/src/util/graph.h
index c18622a054a..600f805c96d 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -360,8 +360,8 @@ class grapht
 template<class N>
 void grapht<N>::add_undirected_edge(node_indext a, node_indext b)
 {
-  assert(a<nodes.size());
-  assert(b<nodes.size());
+  PRECONDITION(a < nodes.size());
+  PRECONDITION(b < nodes.size());
   nodet &na=nodes[a];
   nodet &nb=nodes[b];
   na.add_out(b);
@@ -497,7 +497,8 @@ void grapht<N>::shortest_path(
     path.push_front(dest);
     if(distance[dest]==0 ||
        previous[dest]==src) break; // we are there
-    assert(dest!=previous[dest]);
+    INVARIANT(
+      dest != previous[dest], "loops cannot be part of the shortest path");
     dest=previous[dest];
   }
 }
@@ -536,12 +537,20 @@ void grapht<N>::disconnect_unreachable(const std::vector<node_indext> &src)
   std::size_t reachable_idx = 0;
   for(std::size_t i = 0; i < nodes.size(); i++)
   {
+    // Holds since `reachable` contains node indices (i.e., all elements are
+    // smaller than `nodes.size()`), `reachable` is sorted, indices from `0` to
+    // `nodes.size()-1` are iterated over by variable i in order, and
+    // `reachable_idx` is only incremented when `i == reachable[reachable_idx]`
+    // holds.
+    INVARIANT(
+      reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
+      "node index i is smaller or equal to the node index at "
+      "reachable[reachable_idx], when reachable_idx is within bounds");
+
     if(reachable_idx >= reachable.size())
       remove_edges(i);
     else if(i == reachable[reachable_idx])
       reachable_idx++;
-    else if(i > reachable[reachable_idx])
-      throw "error disconnecting unreachable nodes";
     else
       remove_edges(i);
   }
@@ -787,7 +796,9 @@ void grapht<N>::tarjan(tarjant &t, node_indext v) const
   {
     while(true)
     {
-      assert(!t.scc_stack.empty());
+      INVARIANT(
+        !t.scc_stack.empty(),
+        "stack of strongly connected components should have another component");
       node_indext vp=t.scc_stack.top();
       t.scc_stack.pop();
       t.in_scc[vp]=false;
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 693b48602c9..37aceca87cc 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -13,8 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ostream>
 
-#include "std_expr.h"
+#include "invariant.h"
 #include "simplify_utils.h"
+#include "std_expr.h"
 
 void guardt::guard_expr(exprt &dest) const
 {
@@ -52,8 +53,7 @@ exprt guardt::as_expr(guard_listt::const_iterator it) const
   dest.reserve_operands(guard_list.size());
   for(; it!=guard_list.end(); it++)
   {
-    if(!it->is_boolean())
-      throw "guard is expected to be Boolean";
+    PRECONDITION(it->is_boolean());
     dest.copy_to_operands(*it);
   }
 
@@ -63,7 +63,7 @@ exprt guardt::as_expr(guard_listt::const_iterator it) const
 
 void guardt::add(const exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
+  PRECONDITION(expr.type().id() == ID_bool);
 
   if(is_false() || expr.is_true())
     return;