diff --git a/CODING_STANDARD b/CODING_STANDARD
index ebc2b31f594..0a86fd71b22 100644
--- a/CODING_STANDARD
+++ b/CODING_STANDARD
@@ -158,6 +158,9 @@ C++ features:
 - Use the auto keyword if and only if one of the following
   - The type is explictly repeated on the RHS (e.g. a constructor call)
   - Adding the type will increase confusion (e.g. iterators, function pointers)
+- Avoid assert, if the condition is an actual invariant, use INVARIANT,
+  PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT.
+  If there are possible reasons why it might fail, throw an exception.
 
 Architecture-specific code:
 - Avoid if possible.
diff --git a/regression/cbmc/invariant-failure/main.c b/regression/cbmc/invariant-failure/main.c
new file mode 100644
index 00000000000..f8b643afbf2
--- /dev/null
+++ b/regression/cbmc/invariant-failure/main.c
@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}
diff --git a/regression/cbmc/invariant-failure/test.desc b/regression/cbmc/invariant-failure/test.desc
new file mode 100644
index 00000000000..9966d66547a
--- /dev/null
+++ b/regression/cbmc/invariant-failure/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--test-invariant-failure
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/cpp-linter/assert/main.cpp b/regression/cpp-linter/assert/main.cpp
new file mode 100644
index 00000000000..cceff0cb2ea
--- /dev/null
+++ b/regression/cpp-linter/assert/main.cpp
@@ -0,0 +1,10 @@
+// Author: Martin Brain, martin.brain@diffblue.com
+
+#include <cassert>
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  assert(0);
+  return 0;
+}
diff --git a/regression/cpp-linter/assert/test.desc b/regression/cpp-linter/assert/test.desc
new file mode 100644
index 00000000000..cda85742156
--- /dev/null
+++ b/regression/cpp-linter/assert/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.cpp
+
+^main\.cpp:8:  assert is deprecated, use INVARIANT instead  \[build/deprecated\] \[4\]
+^Total errors found: 1$
+^SIGNAL=0$
diff --git a/regression/test.pl b/regression/test.pl
index d27c663b0aa..0bf364b86c3 100755
--- a/regression/test.pl
+++ b/regression/test.pl
@@ -35,7 +35,6 @@ ($$$$$)
   print LOG "  Core: $dumped_core\n";
 
   if($signal_num != 0) {
-    $failed = 1;
     print "Killed by signal $signal_num";
     if($dumped_core) {
       print " (code dumped)";
diff --git a/scripts/cpplint.py b/scripts/cpplint.py
index 66fe60a3e04..64fab3758f9 100755
--- a/scripts/cpplint.py
+++ b/scripts/cpplint.py
@@ -4629,6 +4629,27 @@ def CheckAltTokens(filename, clean_lines, linenum, error):
               _ALT_TOKEN_REPLACEMENT[match.group(1)], match.group(1)))
 
 
+def CheckAssert(filename, clean_lines, linenum, error):
+  """Check for uses of assert.
+
+  Args:
+    filename: The name of the current file.
+    clean_lines: A CleansedLines instance containing the file.
+    linenum: The number of the line to check.
+    error: The function to call with any errors found.
+  """
+  line = clean_lines.elided[linenum]
+  match = Match(r'.*\s+assert\(.*\).*', line)
+  if match:
+    if Match(r'.*\s+assert\((0|false)\).*', line):
+      error(filename, linenum, 'build/deprecated', 4,
+            'assert is deprecated, use UNREACHABLE instead')
+    else:
+      error(filename, linenum, 'build/deprecated', 4,
+            'assert is deprecated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead')
+
+
+
 def GetLineWidth(line):
   """Determines the width of the line in column positions.
 
@@ -4853,6 +4874,7 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state,
   CheckSpacingForFunctionCall(filename, clean_lines, linenum, error)
   CheckCheck(filename, clean_lines, linenum, error)
   CheckAltTokens(filename, clean_lines, linenum, error)
+  CheckAssert(filename, clean_lines, linenum, error)
   classinfo = nesting_state.InnermostClass()
   if classinfo:
     CheckSectionSpacing(filename, clean_lines, classinfo, linenum, error)
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 085672e4237..d2f1c178d8e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/language.h>
 #include <util/unicode.h>
 #include <util/memory_info.h>
+#include <util/invariant.h>
 
 #include <ansi-c/c_preprocess.h>
 
@@ -104,6 +105,27 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(1); // should contemplate EX_USAGE from sysexits.h
   }
 
+  // Test only; do not use for input validation
+  if(cmdline.isset("test-invariant-failure"))
+  {
+    // Have to catch this as the default handling of uncaught exceptions
+    // on windows appears to be silent termination.
+    try
+    {
+      INVARIANT(0, "Test invariant failure");
+    }
+    catch (const invariant_failedt &e)
+    {
+      std::cerr << e.what();
+      exit(0); // should contemplate EX_OK from sysexits.h
+    }
+    catch (...)
+    {
+      error() << "Unexpected exception type\n";
+    }
+    exit(1);
+  }
+
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 4d8e6753476..d95e60eb25b 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -63,6 +63,7 @@ class optionst;
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
+  "(test-invariant-failure)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index a514a992ecf..11f6b4c5dd1 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ieee_float.h>
 #include <util/base_type.h>
 #include <util/string2int.h>
+#include <util/invariant.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -34,7 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // Mark different kinds of error condition
 // General
-#define UNREACHABLE throw "Supposidly unreachable location reached"
 #define PARSERERROR(S) throw S
 
 // Error checking the expression type
@@ -45,7 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define UNEXPECTEDCASE(S) throw "Unexpected case: " S
 
 // General todos
-#define TODO(S) throw "TODO: " S
+#define SMT2_TODO(S) throw "TODO: " S
 
 void smt2_convt::print_assignment(std::ostream &out) const
 {
@@ -952,7 +952,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("bitnot for vectors");
+        SMT2_TODO("bitnot for vectors");
     }
     else
     {
@@ -1017,7 +1017,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         out << "))"; // mk-, let
       }
       else
-        TODO("unary minus for vector");
+        SMT2_TODO("unary minus for vector");
     }
     else
     {
@@ -1363,7 +1363,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     assert(expr.operands().size()==1);
 
     out << "false"; // TODO
-    TODO("pointer_object_has_type not implemented");
+    SMT2_TODO("pointer_object_has_type not implemented");
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -1432,7 +1432,7 @@ void smt2_convt::convert_expr(const exprt &expr)
       convert_expr(tmp);
       out << ")) bin1)"; // bvlshr, extract, =
       #endif
-      TODO("smt2: extractbits with non-constant index");
+      SMT2_TODO("smt2: extractbits with non-constant index");
     }
   }
   else if(expr.id()==ID_replication)
@@ -1944,7 +1944,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
           // This conversion is non-trivial as it requires creating a
           // new bit-vector variable and then asserting that it converts
           // to the required floating-point number.
-          TODO("bit-wise floatbv to bv");
+          SMT2_TODO("bit-wise floatbv to bv");
         }
         else
         {
@@ -2017,7 +2017,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
         out << "(_ bv" << i << " " << to_width << ")";
       }
       else
-        TODO("can't convert non-constant integer to bitvector");
+        SMT2_TODO("can't convert non-constant integer to bitvector");
     }
     else if(src_type.id()==ID_struct) // flatten a struct to a bit-vector
     {
@@ -2207,7 +2207,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
   }
   else if(dest_type.id()==ID_range)
   {
-    TODO("range typecast");
+    SMT2_TODO("range typecast");
   }
   else if(dest_type.id()==ID_floatbv)
   {
@@ -3031,11 +3031,11 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr)
     }
     else if(type.id()==ID_complex)
     {
-      TODO("+ for floatbv complex");
+      SMT2_TODO("+ for floatbv complex");
     }
     else if(type.id()==ID_vector)
     {
-      TODO("+ for floatbv vector");
+      SMT2_TODO("+ for floatbv vector");
     }
     else
       UNEXPECTEDCASE("unsupported type for +: "+type.id_string());
@@ -3093,7 +3093,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
   }
   else if(expr.type().id()==ID_pointer)
   {
-    TODO("pointer subtraction");
+    SMT2_TODO("pointer subtraction");
   }
   else if(expr.type().id()==ID_vector)
   {
@@ -3527,7 +3527,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
     typecast_exprt index_tc(index, expr_type);
 
     // TODO: SMT2-ify
-    TODO("SMT2-ify");
+    SMT2_TODO("SMT2-ify");
     out << "(bvor ";
     out << "(band ";
 
@@ -3565,7 +3565,7 @@ void smt2_convt::convert_update(const exprt &expr)
 {
   assert(expr.operands().size()==3);
 
-  TODO("smt2_convt::convert_update to be implemented");
+  SMT2_TODO("smt2_convt::convert_update to be implemented");
 }
 
 void smt2_convt::convert_index(const index_exprt &expr)
@@ -3651,7 +3651,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
       mp_integer index_int;
       if(to_integer(expr.index(), index_int))
       {
-        TODO("non-constant index on vectors");
+        SMT2_TODO("non-constant index on vectors");
       }
       else
       {
@@ -3662,7 +3662,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
     }
     else
     {
-      TODO("index on vectors");
+      SMT2_TODO("index on vectors");
     }
   }
   else
diff --git a/src/util/Makefile b/src/util/Makefile
index ce4489b18ce..d5030ef2a48 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -24,6 +24,7 @@ SRC = arith_tools.cpp \
       guard.cpp \
       identifier.cpp \
       ieee_float.cpp \
+      invariant.cpp \
       irep.cpp \
       irep_hash.cpp \
       irep_hash_container.cpp \
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index f6b4b0cad4c..cc022538949 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -9,14 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
-#include <cassert>
-
 #include <stack>
 
 #include "string2int.h"
 #include "mp_arith.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
+#include "invariant.h"
 #include "expr.h"
 #include "rational.h"
 #include "rational_tools.h"
@@ -203,7 +202,7 @@ void exprt::negate()
       else
       {
         make_nil();
-        assert(false);
+        UNREACHABLE;
       }
     }
     else
@@ -211,7 +210,8 @@ void exprt::negate()
       if(id()==ID_unary_minus)
       {
         exprt tmp;
-        assert(operands().size()==1);
+        DATA_INVARIANT(operands().size()==1,
+                       "Unary minus must have one operand");
         tmp.swap(op0());
         swap(tmp);
       }
@@ -245,7 +245,7 @@ bool exprt::is_zero() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_zero();
     }
     else if(type_id==ID_unsignedbv ||
@@ -291,7 +291,7 @@ bool exprt::is_one() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);
       return rat_value.is_one();
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index deab962d7ae..7370b165eab 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -36,14 +36,14 @@ exprt make_binary(const exprt &expr)
   const typet &type=expr.type();
 
   exprt previous=operands.front();
-  assert(previous.type()==type);
+  PRECONDITION(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
-    assert(it->type()==type);
+    PRECONDITION(it->type()==type);
 
     exprt tmp=expr;
     tmp.operands().clear();
@@ -59,7 +59,7 @@ exprt make_binary(const exprt &expr)
 with_exprt make_with_expr(const update_exprt &src)
 {
   const exprt::operandst &designator=src.designator();
-  assert(!designator.empty());
+  PRECONDITION(!designator.empty());
 
   with_exprt result;
   exprt *dest=&result;
@@ -78,7 +78,7 @@ with_exprt make_with_expr(const update_exprt &src)
       //  to_member_designator(*it).get_component_name();
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     *dest=tmp;
     dest=&to_with_expr(*dest).new_value();
@@ -108,7 +108,7 @@ exprt is_not_zero(
     src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
 
   exprt zero=from_integer(0, src_type);
-  assert(zero.is_not_nil());
+  CHECK_RETURN(zero.is_not_nil());
 
   binary_exprt comparison(src, id, zero, bool_typet());
   comparison.add_source_location()=src.source_location();
@@ -142,8 +142,8 @@ bool has_subexpr(const exprt &src, const irep_idt &id)
 
 if_exprt lift_if(const exprt &src, std::size_t operand_number)
 {
-  assert(operand_number<src.operands().size());
-  assert(src.operands()[operand_number].id()==ID_if);
+  PRECONDITION(operand_number<src.operands().size());
+  PRECONDITION(src.operands()[operand_number].id()==ID_if);
 
   const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
   const exprt true_case=if_expr.true_case();
diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp
new file mode 100644
index 00000000000..b0047cccf40
--- /dev/null
+++ b/src/util/invariant.cpp
@@ -0,0 +1,139 @@
+/*******************************************************************\
+
+Module:
+
+Author: Martin Brain, martin.brain@diffblue.com
+
+\*******************************************************************/
+
+
+#include "invariant.h"
+
+#include <string>
+#include <sstream>
+
+#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
+#include <iostream>
+#include <cstdlib>
+#endif
+
+// Backtraces compiler and C library specific
+// So we should include something explicitly from the C library
+// to check if the C library is glibc.
+#include <assert.h>
+#ifdef __GLIBC__
+
+// GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace
+#include <execinfo.h>
+#include <cxxabi.h>
+
+
+/// Attempts to demangle the function name assuming the glibc
+/// format of stack entry:
+///
+/// path '(' mangled_name '+' offset ') [' address ']\0'
+///
+/// \param out: The output stream
+/// \param stack_entry: Description of the stack_entry
+///
+/// \return True <=> the entry has been successfully demangled and printed.
+static bool output_demangled_name(
+  std::ostream &out,
+  const char * const stack_entry)
+{
+  bool return_value=false;
+
+  std::string working(stack_entry);
+
+  std::string::size_type start=working.rfind('(');  // Path may contain '(' !
+  std::string::size_type end=working.find('+', start);
+
+  if(start!=std::string::npos &&
+     end!=std::string::npos &&
+     start+1<=end-1)
+  {
+    std::string::size_type length=end-(start+1);
+    std::string mangled(working.substr(start+1, length));
+
+    int demangle_success=1;
+    char *demangled=
+      abi::__cxa_demangle(mangled.c_str(), NULL, 0, &demangle_success);
+
+    if(demangle_success==0)
+    {
+      out << working.substr(0, start+1)
+          << demangled
+          << working.substr(end);
+      return_value=true;
+    }
+
+    free(demangled);
+  }
+
+  return return_value;
+}
+#endif
+
+
+/// Checks that the given invariant condition holds and prints a back trace
+/// and / or throws an exception depending on build configuration.
+/// Does not return if condition is false.
+/// Returns with no output or state change if true.
+///
+/// \param file : C string giving the name of the file.
+/// \param function : C string giving the name of the function.
+/// \param line : The line number of the invariant
+/// \param condition : The result of evaluating the invariant condition.
+/// \param reason : C string giving the reason why the invariant should be true.
+void check_invariant(
+  const char * const file,
+  const char * const function,
+  const int line,
+  const bool condition,
+  const char * const reason)
+{
+  if(condition)
+    return;
+
+#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
+    std::ostream & out(std::cerr);
+#else
+    std::ostringstream out;
+#endif
+
+    // Flush regularly so that errors during output will result in
+    // partial error logs rather than nothing
+    out << "Invariant check failed\n" << std::flush;
+    out << "File " << file
+        << " function " << function
+        << " line " << line
+        << '\n' << std::flush;
+
+#ifdef __GLIBC__
+    out << "Backtrace\n" << std::flush;
+
+    void * stack[50] = {};
+
+    std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
+    char **description=backtrace_symbols(stack, entries);
+
+    for(std::size_t i=0; i<entries; i++)
+    {
+      if(!output_demangled_name(out, description[i]))
+        out << description[i];
+      out << '\n' << std::flush;
+    }
+
+    free(description);
+
+#else
+    out << "Backtraces not supported\n" << std::flush;
+#endif
+
+
+#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
+    abort();
+#else
+    throw invariant_failedt(out.str());
+#endif
+}
diff --git a/src/util/invariant.h b/src/util/invariant.h
new file mode 100644
index 00000000000..e5bc07b3d5c
--- /dev/null
+++ b/src/util/invariant.h
@@ -0,0 +1,142 @@
+/*******************************************************************\
+
+Module:
+
+Author: Martin Brain, martin.brain@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_INVARIANT_H
+#define CPROVER_UTIL_INVARIANT_H
+
+#include <stdexcept>
+
+/*
+** Invariants document conditions that the programmer believes to
+** be always true as a consequence of the system architecture and / or
+** preceeding code.  In principle it should be possible to (machine
+** checked) verify them.  The condition should be side-effect free and
+** evaluate to a boolean.
+**
+** As well as the condition they have a text argument that should be
+** used to say why they are true.  The reason should be a string literals.
+** Longer diagnostics should be output to error(). For example:
+**
+** INVARIANT(x > 0, "x negative and zero case handled by other branches");
+**
+** To help classify different kinds of invariants, various short-hand
+** macros are provided.
+**
+** Invariants are used to document and check design / implementation
+** knowledge.  They should *not* be used:
+**  - to validate user input or options
+**    (throw an exception or handle more gracefully)
+**  - to log information (use debug(), progress(), etc.)
+**  - as TODO notes (acceptable in private repositories but fix before PR)
+**  - to handle cases that are unlikely, tedious or expensive (ditto)
+**  - to modify the state of the system (i.e. no side effects)
+**
+** Invariants provide the following guarantee:
+**  IF the condition is false
+**  THEN an invariant_failed exception will be thrown
+**       OR there will be undefined behaviour
+**
+** Consequentally, programmers may assume that the condition of an
+** invariant is true after it has been executed.  Applications are 
+** encouraged to (at least) catch exceptions at the top level and
+** output them.
+**
+** Various different approaches to checking (or not) the invariants
+** and handling their failure are supported and can be configured with
+** CPROVER_INVARIANT_* macros.
+*/
+
+class invariant_failedt: public std::logic_error
+{
+public:
+  explicit invariant_failedt(const std::string& what) : logic_error(what) {}
+  explicit invariant_failedt(const char* what) : logic_error(what) {}
+};
+
+
+#if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
+// Used to allow CPROVER to check itself
+#define INVARIANT(CONDITION, REASON) \
+  __CPROVER_assert((CONDITION), "Invariant : " REASON)
+
+
+#elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
+// For performance builds, invariants can be ignored
+// This is *not* recommended as it can result in unpredictable behaviour
+// including silently reporting incorrect results.
+// This is also useful for checking side-effect freedom.
+#define INVARIANT(CONDITION, REASON) do {} while(0)
+
+
+#elif defined(CPROVER_INVARIANT_ASSERT)
+// Not recommended but provided for backwards compatability
+#include <cassert>
+// NOLINTNEXTLINE(*)
+#define INVARIANT(CONDITION, REASON) assert((CONDITION) && (REASON))
+
+
+#else
+// CPROVER_INVARIANT_PRINT_STACK_TRACE affects the implementation of
+// this function but not it's generation from the macro
+
+void check_invariant(
+  const char * const file,
+  const char * const function,
+  const int line,
+  const bool condition,
+  const char * const reason);
+
+#ifdef _MSC_VER
+#define INVARIANT(CONDITION, REASON) \
+  check_invariant(__FILE__, __FUNCTION__, __LINE__, (CONDITION), (REASON))
+#else
+#define INVARIANT(CONDITION, REASON)                                    \
+  check_invariant(__FILE__, __func__, __LINE__, (CONDITION), (REASON))
+#endif
+
+
+#endif
+
+
+
+// Short hand macros
+
+// The condition should only contain (unmodified) arguments to the method.
+// "The design of the system means that the arguments to this method
+//  will always meet this condition".
+#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
+
+// The condition should only contain variables that will be returned /
+// output without further modification.
+// "The implementation of this method means that the condition will hold".
+#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
+
+// The condition should only contain (unmodified) values that were
+// changed by a previous method call.
+// "The contract of the previous method call means the following
+//  condition holds".
+#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
+
+// This should be used to mark dead code
+#define UNREACHABLE INVARIANT(false, "Unreachable")
+
+// This condition should be used to document that assumptions that are
+// made on goto_functions, goto_programs, exprts, etc. being well formed.
+// "The data structure is corrupt or malformed"
+#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
+
+
+// Legacy annotations
+
+// The following should not be used in new code and are only intended
+// to migrate documentation and "error handling" in older code
+#define TODO           INVARIANT(0, "Todo")
+#define UNIMPLEMENTED  INVARIANT(0, "Unimplemented")
+#define UNHANDLED_CASE INVARIANT(0, "Unhandled case")
+
+#endif // CPROVER_UTIL_INVARIANT_H
diff --git a/src/util/irep.cpp b/src/util/irep.cpp
index d44208a25f7..6efa7ccf826 100644
--- a/src/util/irep.cpp
+++ b/src/util/irep.cpp
@@ -9,9 +9,10 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Internal Representation
 
-#include <cassert>
 #include <ostream>
 
+#include "invariant.h"
+
 #include "string2int.h"
 #include "irep.h"
 #include "string_hash.h"
@@ -87,7 +88,7 @@ void irept::detach()
     remove_ref(old_data);
   }
 
-  assert(data->ref_count==1);
+  POSTCONDITION(data->ref_count==1);
 
   #ifdef IREP_DEBUG
   std::cout << "DETACH2: " << data << '\n';
@@ -105,7 +106,7 @@ void irept::remove_ref(dt *old_data)
   nonrecursive_destructor(old_data);
   #else
 
-  assert(old_data->ref_count!=0);
+  PRECONDITION(old_data->ref_count!=0);
 
   #ifdef IREP_DEBUG
   std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
@@ -147,7 +148,7 @@ void irept::nonrecursive_destructor(dt *old_data)
     if(d==&empty_d)
       continue;
 
-    assert(d->ref_count!=0);
+    INVARIANT(d->ref_count!=0, "All contents of the stack must be in use");
     d->ref_count--;
 
     if(d->ref_count==0)
@@ -456,7 +457,8 @@ bool irept::ordering(const irept &other) const
         return false;
     }
 
-    assert(it1==X.sub.end() && it2==Y.sub.end());
+    INVARIANT(it1==X.sub.end() && it2==Y.sub.end(),
+              "Unequal lengths will return before this");
   }
 
   if(X.named_sub.size()<Y.named_sub.size())
@@ -484,7 +486,8 @@ bool irept::ordering(const irept &other) const
         return false;
     }
 
-    assert(it1==X.named_sub.end() && it2==Y.named_sub.end());
+    INVARIANT(it1==X.named_sub.end() && it2==Y.named_sub.end(),
+              "Unequal lengths will return before this");
   }
 
   return false;
@@ -521,7 +524,8 @@ int irept::compare(const irept &i) const
         return r;
     }
 
-    assert(it1==get_sub().end() && it2==i.get_sub().end());
+    INVARIANT(it1==get_sub().end() && it2==i.get_sub().end(),
+              "Unequal lengths will return before this");
   }
 
   const named_subt::size_type n_size=get_named_sub().size(),
@@ -549,8 +553,9 @@ int irept::compare(const irept &i) const
         return r;
     }
 
-    assert(it1==get_named_sub().end() &&
-           it2==i.get_named_sub().end());
+    INVARIANT(it1==get_named_sub().end() &&
+              it2==i.get_named_sub().end(),
+              "Unequal lengths will return before this");
   }
 
   // equal
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 1308daad3e4..e2ed2ad433d 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -17,8 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
-#include <cassert>
-
+#include "invariant.h"
 #include "std_types.h"
 
 /*! \defgroup gr_std_expr Conversion to specific expressions
@@ -59,7 +58,10 @@ class transt:public exprt
 */
 inline const transt &to_trans_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_trans && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_trans);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Transition systems must have three operands");
   return static_cast<const transt &>(expr);
 }
 
@@ -68,7 +70,10 @@ inline const transt &to_trans_expr(const exprt &expr)
 */
 inline transt &to_trans_expr(exprt &expr)
 {
-  assert(expr.id()==ID_trans && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_trans);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Transition systems must have three operands");
   return static_cast<transt &>(expr);
 }
 
@@ -196,7 +201,8 @@ class decorated_symbol_exprt:public symbol_exprt
 */
 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_symbol && !expr.has_operands());
+  PRECONDITION(expr.id()==ID_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
   return static_cast<const symbol_exprt &>(expr);
 }
 
@@ -205,7 +211,8 @@ inline const symbol_exprt &to_symbol_expr(const exprt &expr)
 */
 inline symbol_exprt &to_symbol_expr(exprt &expr)
 {
-  assert(expr.id()==ID_symbol && !expr.has_operands());
+  PRECONDITION(expr.id()==ID_symbol);
+  DATA_INVARIANT(!expr.has_operands(), "Symbols must not have operands");
   return static_cast<symbol_exprt &>(expr);
 }
 
@@ -271,7 +278,9 @@ class unary_exprt:public exprt
 */
 inline const unary_exprt &to_unary_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==1);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Unary expressions must have one operand");
   return static_cast<const unary_exprt &>(expr);
 }
 
@@ -280,7 +289,9 @@ inline const unary_exprt &to_unary_expr(const exprt &expr)
 */
 inline unary_exprt &to_unary_expr(exprt &expr)
 {
-  assert(expr.operands().size()==1);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Unary expressions must have one operand");
   return static_cast<unary_exprt &>(expr);
 }
 
@@ -311,7 +322,10 @@ class abs_exprt:public unary_exprt
 */
 inline const abs_exprt &to_abs_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_abs && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_abs);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Absolute value must have one operand");
   return static_cast<const abs_exprt &>(expr);
 }
 
@@ -320,7 +334,10 @@ inline const abs_exprt &to_abs_expr(const exprt &expr)
 */
 inline abs_exprt &to_abs_expr(exprt &expr)
 {
-  assert(expr.id()==ID_abs && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_abs);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Absolute value must have one operand");
   return static_cast<abs_exprt &>(expr);
 }
 
@@ -358,7 +375,10 @@ class unary_minus_exprt:public unary_exprt
 */
 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_unary_minus && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_unary_minus);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Unary minus must have one operand");
   return static_cast<const unary_minus_exprt &>(expr);
 }
 
@@ -367,7 +387,10 @@ inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
 */
 inline unary_minus_exprt &to_unary_minus_expr(exprt &expr)
 {
-  assert(expr.id()==ID_unary_minus && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_unary_minus);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Unary minus must have one operand");
   return static_cast<unary_minus_exprt &>(expr);
 }
 
@@ -500,7 +523,9 @@ class binary_exprt:public exprt
 */
 inline const binary_exprt &to_binary_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Binary expressions must have two operands");
   return static_cast<const binary_exprt &>(expr);
 }
 
@@ -509,7 +534,9 @@ inline const binary_exprt &to_binary_expr(const exprt &expr)
 */
 inline binary_exprt &to_binary_expr(exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Binary expressions must have two operands");
   return static_cast<binary_exprt &>(expr);
 }
 
@@ -591,7 +618,9 @@ class binary_relation_exprt:public binary_predicate_exprt
 */
 inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Binary relations must have two operands");
   return static_cast<const binary_relation_exprt &>(expr);
 }
 
@@ -600,7 +629,9 @@ inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr)
 */
 inline binary_relation_exprt &to_binary_relation_expr(exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Binary relations must have two operands");
   return static_cast<binary_relation_exprt &>(expr);
 }
 
@@ -703,7 +734,10 @@ class plus_exprt:public multi_ary_exprt
 */
 inline const plus_exprt &to_plus_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_plus && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_plus);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Plus must have two or more operands");
   return static_cast<const plus_exprt &>(expr);
 }
 
@@ -712,7 +746,10 @@ inline const plus_exprt &to_plus_expr(const exprt &expr)
 */
 inline plus_exprt &to_plus_expr(exprt &expr)
 {
-  assert(expr.id()==ID_plus && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_plus);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Plus must have two or more operands");
   return static_cast<plus_exprt &>(expr);
 }
 
@@ -745,7 +782,10 @@ class minus_exprt:public binary_exprt
 */
 inline const minus_exprt &to_minus_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_minus && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_minus);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Minus must have two or more operands");
   return static_cast<const minus_exprt &>(expr);
 }
 
@@ -754,7 +794,10 @@ inline const minus_exprt &to_minus_expr(const exprt &expr)
 */
 inline minus_exprt &to_minus_expr(exprt &expr)
 {
-  assert(expr.id()==ID_minus && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_minus);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Minus must have two or more operands");
   return static_cast<minus_exprt &>(expr);
 }
 
@@ -787,7 +830,10 @@ class mult_exprt:public multi_ary_exprt
 */
 inline const mult_exprt &to_mult_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_mult && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_mult);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Multiply must have two or more operands");
   return static_cast<const mult_exprt &>(expr);
 }
 
@@ -796,7 +842,10 @@ inline const mult_exprt &to_mult_expr(const exprt &expr)
 */
 inline mult_exprt &to_mult_expr(exprt &expr)
 {
-  assert(expr.id()==ID_mult && expr.operands().size()>=2);
+  PRECONDITION(expr.id()==ID_mult);
+  DATA_INVARIANT(
+    expr.operands().size()>=2,
+    "Multiply must have two or more operands");
   return static_cast<mult_exprt &>(expr);
 }
 
@@ -829,7 +878,10 @@ class div_exprt:public binary_exprt
 */
 inline const div_exprt &to_div_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_div && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_div);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Divide must have two operands");
   return static_cast<const div_exprt &>(expr);
 }
 
@@ -838,7 +890,10 @@ inline const div_exprt &to_div_expr(const exprt &expr)
 */
 inline div_exprt &to_div_expr(exprt &expr)
 {
-  assert(expr.id()==ID_div && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_div);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Divide must have two operands");
   return static_cast<div_exprt &>(expr);
 }
 
@@ -871,7 +926,8 @@ class mod_exprt:public binary_exprt
 */
 inline const mod_exprt &to_mod_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_mod && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_mod);
+  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
   return static_cast<const mod_exprt &>(expr);
 }
 
@@ -880,7 +936,8 @@ inline const mod_exprt &to_mod_expr(const exprt &expr)
 */
 inline mod_exprt &to_mod_expr(exprt &expr)
 {
-  assert(expr.id()==ID_mod && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_mod);
+  DATA_INVARIANT(expr.operands().size()==2, "Modulo must have two operands");
   return static_cast<mod_exprt &>(expr);
 }
 
@@ -913,7 +970,8 @@ class rem_exprt:public binary_exprt
 */
 inline const rem_exprt &to_rem_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_rem && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_rem);
+  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
   return static_cast<const rem_exprt &>(expr);
 }
 
@@ -922,7 +980,8 @@ inline const rem_exprt &to_rem_expr(const exprt &expr)
 */
 inline rem_exprt &to_rem_expr(exprt &expr)
 {
-  assert(expr.id()==ID_rem && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_rem);
+  DATA_INVARIANT(expr.operands().size()==2, "Remainder must have two operands");
   return static_cast<rem_exprt &>(expr);
 }
 
@@ -955,7 +1014,8 @@ class power_exprt:public binary_exprt
 */
 inline const power_exprt &to_power_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_power && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_power);
+  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
   return static_cast<const power_exprt &>(expr);
 }
 
@@ -964,7 +1024,8 @@ inline const power_exprt &to_power_expr(const exprt &expr)
 */
 inline power_exprt &to_power_expr(exprt &expr)
 {
-  assert(expr.id()==ID_power && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_power);
+  DATA_INVARIANT(expr.operands().size()==2, "Power must have two operands");
   return static_cast<power_exprt &>(expr);
 }
 
@@ -997,7 +1058,10 @@ class factorial_power_exprt:public binary_exprt
 */
 inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_factorial_power && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_factorial_power);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Factorial power must have two operands");
   return static_cast<const factorial_power_exprt &>(expr);
 }
 
@@ -1006,7 +1070,10 @@ inline const factorial_power_exprt &to_factorial_power_expr(const exprt &expr)
 */
 inline factorial_power_exprt &to_factorial_expr(exprt &expr)
 {
-  assert(expr.id()==ID_factorial_power && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_factorial_power);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Factorial power must have two operands");
   return static_cast<factorial_power_exprt &>(expr);
 }
 
@@ -1037,7 +1104,8 @@ class equal_exprt:public binary_relation_exprt
 */
 inline const equal_exprt &to_equal_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_equal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_equal);
+  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
   return static_cast<const equal_exprt &>(expr);
 }
 
@@ -1046,7 +1114,8 @@ inline const equal_exprt &to_equal_expr(const exprt &expr)
 */
 inline equal_exprt &to_equal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_equal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_equal);
+  DATA_INVARIANT(expr.operands().size()==2, "Equality must have two operands");
   return static_cast<equal_exprt &>(expr);
 }
 
@@ -1077,7 +1146,10 @@ class notequal_exprt:public binary_relation_exprt
 */
 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_notequal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_notequal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Inequality must have two operands");
   return static_cast<const notequal_exprt &>(expr);
 }
 
@@ -1086,7 +1158,10 @@ inline const notequal_exprt &to_notequal_expr(const exprt &expr)
 */
 inline notequal_exprt &to_notequal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_notequal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_notequal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Inequality must have two operands");
   return static_cast<notequal_exprt &>(expr);
 }
 
@@ -1153,7 +1228,10 @@ class index_exprt:public exprt
 */
 inline const index_exprt &to_index_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_index && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_index);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Array index must have two operands");
   return static_cast<const index_exprt &>(expr);
 }
 
@@ -1162,7 +1240,10 @@ inline const index_exprt &to_index_expr(const exprt &expr)
 */
 inline index_exprt &to_index_expr(exprt &expr)
 {
-  assert(expr.id()==ID_index && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_index);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Array index must have two operands");
   return static_cast<index_exprt &>(expr);
 }
 
@@ -1204,7 +1285,10 @@ class array_of_exprt:public unary_exprt
 */
 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_array_of && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_array_of);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "'Array of' must have one operand");
   return static_cast<const array_of_exprt &>(expr);
 }
 
@@ -1213,7 +1297,10 @@ inline const array_of_exprt &to_array_of_expr(const exprt &expr)
 */
 inline array_of_exprt &to_array_of_expr(exprt &expr)
 {
-  assert(expr.id()==ID_array_of && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_array_of);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "'Array of' must have one operand");
   return static_cast<array_of_exprt &>(expr);
 }
 
@@ -1244,7 +1331,7 @@ class array_exprt:public exprt
 */
 inline const array_exprt &to_array_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_array);
+  PRECONDITION(expr.id()==ID_array);
   return static_cast<const array_exprt &>(expr);
 }
 
@@ -1253,11 +1340,11 @@ inline const array_exprt &to_array_expr(const exprt &expr)
 */
 inline array_exprt &to_array_expr(exprt &expr)
 {
-  assert(expr.id()==ID_array);
+  PRECONDITION(expr.id()==ID_array);
   return static_cast<array_exprt &>(expr);
 }
 
-/*! \brief array constructor from list of elements
+/*! \brief vector constructor from list of elements
 */
 class vector_exprt:public exprt
 {
@@ -1284,7 +1371,7 @@ class vector_exprt:public exprt
 */
 inline const vector_exprt &to_vector_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_vector);
+  PRECONDITION(expr.id()==ID_vector);
   return static_cast<const vector_exprt &>(expr);
 }
 
@@ -1293,7 +1380,7 @@ inline const vector_exprt &to_vector_expr(const exprt &expr)
 */
 inline vector_exprt &to_vector_expr(exprt &expr)
 {
-  assert(expr.id()==ID_vector);
+  PRECONDITION(expr.id()==ID_vector);
   return static_cast<vector_exprt &>(expr);
 }
 
@@ -1353,7 +1440,10 @@ class union_exprt:public unary_exprt
 */
 inline const union_exprt &to_union_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_union && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_union);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Union constructor must have one operand");
   return static_cast<const union_exprt &>(expr);
 }
 
@@ -1362,7 +1452,10 @@ inline const union_exprt &to_union_expr(const exprt &expr)
 */
 inline union_exprt &to_union_expr(exprt &expr)
 {
-  assert(expr.id()==ID_union && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_union);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Union constructor must have one operand");
   return static_cast<union_exprt &>(expr);
 }
 
@@ -1393,7 +1486,7 @@ class struct_exprt:public exprt
 */
 inline const struct_exprt &to_struct_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_struct);
+  PRECONDITION(expr.id()==ID_struct);
   return static_cast<const struct_exprt &>(expr);
 }
 
@@ -1402,7 +1495,7 @@ inline const struct_exprt &to_struct_expr(const exprt &expr)
 */
 inline struct_exprt &to_struct_expr(exprt &expr)
 {
-  assert(expr.id()==ID_struct);
+  PRECONDITION(expr.id()==ID_struct);
   return static_cast<struct_exprt &>(expr);
 }
 
@@ -1459,7 +1552,10 @@ class complex_exprt:public binary_exprt
 */
 inline const complex_exprt &to_complex_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_complex && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_complex);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Complex constructor must have two operands");
   return static_cast<const complex_exprt &>(expr);
 }
 
@@ -1468,7 +1564,10 @@ inline const complex_exprt &to_complex_expr(const exprt &expr)
 */
 inline complex_exprt &to_complex_expr(exprt &expr)
 {
-  assert(expr.id()==ID_complex && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_complex);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Complex constructor must have two operands");
   return static_cast<complex_exprt &>(expr);
 }
 
@@ -1535,7 +1634,10 @@ class object_descriptor_exprt:public exprt
 inline const object_descriptor_exprt &to_object_descriptor_expr(
   const exprt &expr)
 {
-  assert(expr.id()==ID_object_descriptor && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_object_descriptor);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Object descriptor must have two operands");
   return static_cast<const object_descriptor_exprt &>(expr);
 }
 
@@ -1544,7 +1646,10 @@ inline const object_descriptor_exprt &to_object_descriptor_expr(
 */
 inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
 {
-  assert(expr.id()==ID_object_descriptor && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_object_descriptor);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Object descriptor must have two operands");
   return static_cast<object_descriptor_exprt &>(expr);
 }
 
@@ -1596,7 +1701,10 @@ class dynamic_object_exprt:public exprt
 inline const dynamic_object_exprt &to_dynamic_object_expr(
   const exprt &expr)
 {
-  assert(expr.id()==ID_dynamic_object && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Dynamic object must have two operands");
   return static_cast<const dynamic_object_exprt &>(expr);
 }
 
@@ -1605,7 +1713,10 @@ inline const dynamic_object_exprt &to_dynamic_object_expr(
 */
 inline dynamic_object_exprt &to_dynamic_object_expr(exprt &expr)
 {
-  assert(expr.id()==ID_dynamic_object && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Dynamic object must have two operands");
   return static_cast<dynamic_object_exprt &>(expr);
 }
 
@@ -1648,7 +1759,10 @@ class typecast_exprt:public exprt
 */
 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_typecast && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_typecast);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Typecast must have one operand");
   return static_cast<const typecast_exprt &>(expr);
 }
 
@@ -1657,7 +1771,10 @@ inline const typecast_exprt &to_typecast_expr(const exprt &expr)
 */
 inline typecast_exprt &to_typecast_expr(exprt &expr)
 {
-  assert(expr.id()==ID_typecast && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_typecast);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Typecast must have one operand");
   return static_cast<typecast_exprt &>(expr);
 }
 
@@ -1711,7 +1828,10 @@ class floatbv_typecast_exprt:public binary_exprt
 */
 inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_floatbv_typecast && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_floatbv_typecast);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Float typecast must have two operands");
   return static_cast<const floatbv_typecast_exprt &>(expr);
 }
 
@@ -1720,7 +1840,10 @@ inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr)
 */
 inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr)
 {
-  assert(expr.id()==ID_floatbv_typecast && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_floatbv_typecast);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Float typecast must have two operands");
   return static_cast<floatbv_typecast_exprt &>(expr);
 }
 
@@ -1779,7 +1902,10 @@ exprt conjunction(const exprt::operandst &);
 */
 inline const and_exprt &to_and_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_and);
+  PRECONDITION(expr.id()==ID_and);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "And must have two or more operands");
   return static_cast<const and_exprt &>(expr);
 }
 
@@ -1788,7 +1914,10 @@ inline const and_exprt &to_and_expr(const exprt &expr)
 */
 inline and_exprt &to_and_expr(exprt &expr)
 {
-  assert(expr.id()==ID_and);
+  PRECONDITION(expr.id()==ID_and);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "And must have two or more operands");
   return static_cast<and_exprt &>(expr);
 }
 
@@ -1819,7 +1948,8 @@ class implies_exprt:public binary_exprt
 */
 inline const implies_exprt &to_implies_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_implies && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_implies);
+  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
   return static_cast<const implies_exprt &>(expr);
 }
 
@@ -1828,7 +1958,8 @@ inline const implies_exprt &to_implies_expr(const exprt &expr)
 */
 inline implies_exprt &to_implies_expr(exprt &expr)
 {
-  assert(expr.id()==ID_implies && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_implies);
+  DATA_INVARIANT(expr.operands().size()==2, "Implies must have two operands");
   return static_cast<implies_exprt &>(expr);
 }
 
@@ -1887,7 +2018,10 @@ exprt disjunction(const exprt::operandst &);
 */
 inline const or_exprt &to_or_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_or);
+  PRECONDITION(expr.id()==ID_or);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Or must have two or more operands");
   return static_cast<const or_exprt &>(expr);
 }
 
@@ -1896,7 +2030,10 @@ inline const or_exprt &to_or_expr(const exprt &expr)
 */
 inline or_exprt &to_or_expr(exprt &expr)
 {
-  assert(expr.id()==ID_or);
+  PRECONDITION(expr.id()==ID_or);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Or must have two or more operands");
   return static_cast<or_exprt &>(expr);
 }
 
@@ -1915,6 +2052,36 @@ class bitnot_exprt:public unary_exprt
   }
 };
 
+/*! \brief Cast a generic exprt to a \ref bitnot_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * bitnot_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref bitnot_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_bitnot);
+  // DATA_INVARIANT(expr.operands().size()==1,
+  //                "Bit-wise not must have one operand");
+  return static_cast<const bitnot_exprt &>(expr);
+}
+
+/*! \copydoc to_bitnot_expr(const exprt &)
+ * \ingroup gr_std_expr
+*/
+inline bitnot_exprt &to_bitnot_expr(exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_bitnot);
+  // DATA_INVARIANT(expr.operands().size()==1,
+  //                "Bit-wise not must have one operand");
+  return static_cast<bitnot_exprt &>(expr);
+}
+
+
 /*! \brief Bit-wise OR
 */
 class bitor_exprt:public multi_ary_exprt
@@ -1943,7 +2110,10 @@ class bitor_exprt:public multi_ary_exprt
 */
 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_bitor);
+  PRECONDITION(expr.id()==ID_bitor);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise or must have two or more operands");
   return static_cast<const bitor_exprt &>(expr);
 }
 
@@ -1952,7 +2122,10 @@ inline const bitor_exprt &to_bitor_expr(const exprt &expr)
 */
 inline bitor_exprt &to_bitor_expr(exprt &expr)
 {
-  assert(expr.id()==ID_bitor);
+  PRECONDITION(expr.id()==ID_bitor);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise or must have two or more operands");
   return static_cast<bitor_exprt &>(expr);
 }
 
@@ -1983,7 +2156,10 @@ class bitxor_exprt:public multi_ary_exprt
 */
 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_bitxor);
+  PRECONDITION(expr.id()==ID_bitxor);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise xor must have two or more operands");
   return static_cast<const bitxor_exprt &>(expr);
 }
 
@@ -1992,7 +2168,10 @@ inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
 */
 inline bitxor_exprt &to_bitxor_expr(exprt &expr)
 {
-  assert(expr.id()==ID_bitxor);
+  PRECONDITION(expr.id()==ID_bitxor);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise xor must have two or more operands");
   return static_cast<bitxor_exprt &>(expr);
 }
 
@@ -2024,7 +2203,10 @@ class bitand_exprt:public multi_ary_exprt
 */
 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_bitand);
+  PRECONDITION(expr.id()==ID_bitand);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise and must have two or more operands");
   return static_cast<const bitand_exprt &>(expr);
 }
 
@@ -2033,7 +2215,10 @@ inline const bitand_exprt &to_bitand_expr(const exprt &expr)
 */
 inline bitand_exprt &to_bitand_expr(exprt &expr)
 {
-  assert(expr.id()==ID_bitand);
+  PRECONDITION(expr.id()==ID_bitand);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Bit-wise and must have two or more operands");
   return static_cast<bitand_exprt &>(expr);
 }
 
@@ -2094,7 +2279,9 @@ class shift_exprt:public binary_exprt
 */
 inline const shift_exprt &to_shift_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Shifts must have two operands");
   return static_cast<const shift_exprt &>(expr);
 }
 
@@ -2103,7 +2290,9 @@ inline const shift_exprt &to_shift_expr(const exprt &expr)
 */
 inline shift_exprt &to_shift_expr(exprt &expr)
 {
-  assert(expr.operands().size()==2);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Shifts must have two operands");
   return static_cast<shift_exprt &>(expr);
 }
 
@@ -2221,7 +2410,10 @@ class replication_exprt:public binary_exprt
 */
 inline const replication_exprt &to_replication_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_replication && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_replication);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Bit-wise replication must have two operands");
   return static_cast<const replication_exprt &>(expr);
 }
 
@@ -2230,7 +2422,10 @@ inline const replication_exprt &to_replication_expr(const exprt &expr)
 */
 inline replication_exprt &to_replication_expr(exprt &expr)
 {
-  assert(expr.id()==ID_replication && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_replication);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Bit-wise replication must have two operands");
   return static_cast<replication_exprt &>(expr);
 }
 
@@ -2286,7 +2481,10 @@ class extractbit_exprt:public binary_predicate_exprt
 */
 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_extractbit && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_extractbit);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Extract bit must have two operands");
   return static_cast<const extractbit_exprt &>(expr);
 }
 
@@ -2295,7 +2493,10 @@ inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
 */
 inline extractbit_exprt &to_extractbit_expr(exprt &expr)
 {
-  assert(expr.id()==ID_extractbit && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_extractbit);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Extract bit must have two operands");
   return static_cast<extractbit_exprt &>(expr);
 }
 
@@ -2368,7 +2569,10 @@ class extractbits_exprt:public exprt
 */
 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_extractbits && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_extractbits);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Extract bits must have three operands");
   return static_cast<const extractbits_exprt &>(expr);
 }
 
@@ -2377,7 +2581,10 @@ inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
 */
 inline extractbits_exprt &to_extractbits_expr(exprt &expr)
 {
-  assert(expr.id()==ID_extractbits && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_extractbits);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Extract bits must have three operands");
   return static_cast<extractbits_exprt &>(expr);
 }
 
@@ -2421,7 +2628,8 @@ class address_of_exprt:public exprt
 */
 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_address_of && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_address_of);
+  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
   return static_cast<const address_of_exprt &>(expr);
 }
 
@@ -2430,7 +2638,8 @@ inline const address_of_exprt &to_address_of_expr(const exprt &expr)
 */
 inline address_of_exprt &to_address_of_expr(exprt &expr)
 {
-  assert(expr.id()==ID_address_of && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_address_of);
+  DATA_INVARIANT(expr.operands().size()==1, "Address of must have one operand");
   return static_cast<address_of_exprt &>(expr);
 }
 
@@ -2472,7 +2681,8 @@ class not_exprt:public exprt
 */
 inline const not_exprt &to_not_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_not && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_not);
+  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
   return static_cast<const not_exprt &>(expr);
 }
 
@@ -2481,7 +2691,8 @@ inline const not_exprt &to_not_expr(const exprt &expr)
 */
 inline not_exprt &to_not_expr(exprt &expr)
 {
-  assert(expr.id()==ID_not && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_not);
+  DATA_INVARIANT(expr.operands().size()==1, "Not must have one operand");
   return static_cast<not_exprt &>(expr);
 }
 
@@ -2536,7 +2747,10 @@ class dereference_exprt:public exprt
 */
 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_dereference && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_dereference);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Dereference must have one operand");
   return static_cast<const dereference_exprt &>(expr);
 }
 
@@ -2545,7 +2759,10 @@ inline const dereference_exprt &to_dereference_expr(const exprt &expr)
 */
 inline dereference_exprt &to_dereference_expr(exprt &expr)
 {
-  assert(expr.id()==ID_dereference && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_dereference);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Dereference must have one operand");
   return static_cast<dereference_exprt &>(expr);
 }
 
@@ -2618,7 +2835,10 @@ class if_exprt:public exprt
 */
 inline const if_exprt &to_if_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_if && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_if);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "If-then-else must have three operands");
   return static_cast<const if_exprt &>(expr);
 }
 
@@ -2627,7 +2847,10 @@ inline const if_exprt &to_if_expr(const exprt &expr)
 */
 inline if_exprt &to_if_expr(exprt &expr)
 {
-  assert(expr.id()==ID_if && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_if);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "If-then-else must have three operands");
   return static_cast<if_exprt &>(expr);
 }
 
@@ -2695,7 +2918,10 @@ class with_exprt:public exprt
 */
 inline const with_exprt &to_with_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_with && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_with);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array/structure update must have three operands");
   return static_cast<const with_exprt &>(expr);
 }
 
@@ -2704,7 +2930,10 @@ inline const with_exprt &to_with_expr(const exprt &expr)
 */
 inline with_exprt &to_with_expr(exprt &expr)
 {
-  assert(expr.id()==ID_with && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_with);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array/structure update must have three operands");
   return static_cast<with_exprt &>(expr);
 }
 
@@ -2740,7 +2969,10 @@ class index_designatort:public exprt
 */
 inline const index_designatort &to_index_designator(const exprt &expr)
 {
-  assert(expr.id()==ID_index_designator && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_index_designator);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Index designator must have one operand");
   return static_cast<const index_designatort &>(expr);
 }
 
@@ -2749,7 +2981,10 @@ inline const index_designatort &to_index_designator(const exprt &expr)
 */
 inline index_designatort &to_index_designator(exprt &expr)
 {
-  assert(expr.id()==ID_index_designator && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_index_designator);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Index designator must have one operand");
   return static_cast<index_designatort &>(expr);
 }
 
@@ -2780,7 +3015,10 @@ class member_designatort:public exprt
 */
 inline const member_designatort &to_member_designator(const exprt &expr)
 {
-  assert(expr.id()==ID_member_designator && expr.operands().size()==0);
+  PRECONDITION(expr.id()==ID_member_designator);
+  DATA_INVARIANT(
+    !expr.has_operands(),
+    "Member designator must not have operands");
   return static_cast<const member_designatort &>(expr);
 }
 
@@ -2789,7 +3027,10 @@ inline const member_designatort &to_member_designator(const exprt &expr)
 */
 inline member_designatort &to_member_designator(exprt &expr)
 {
-  assert(expr.id()==ID_member_designator && expr.operands().size()==0);
+  PRECONDITION(expr.id()==ID_member_designator);
+  DATA_INVARIANT(
+    !expr.has_operands(),
+    "Member designator must not have operands");
   return static_cast<member_designatort &>(expr);
 }
 
@@ -2866,7 +3107,10 @@ class update_exprt:public exprt
 */
 inline const update_exprt &to_update_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_update && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_update);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array/structure update must have three operands");
   return static_cast<const update_exprt &>(expr);
 }
 
@@ -2875,7 +3119,10 @@ inline const update_exprt &to_update_expr(const exprt &expr)
 */
 inline update_exprt &to_update_expr(exprt &expr)
 {
-  assert(expr.id()==ID_update && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_update);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array/structure update must have three operands");
   return static_cast<update_exprt &>(expr);
 }
 
@@ -2942,7 +3189,10 @@ class array_update_exprt:public exprt
 */
 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_array_update && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_array_update);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array update must have three operands");
   return static_cast<const array_update_exprt &>(expr);
 }
 
@@ -2951,7 +3201,10 @@ inline const array_update_exprt &to_array_update_expr(const exprt &expr)
 */
 inline array_update_exprt &to_array_update_expr(exprt &expr)
 {
-  assert(expr.id()==ID_array_update && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_array_update);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "Array update must have three operands");
   return static_cast<array_update_exprt &>(expr);
 }
 #endif
@@ -3048,7 +3301,10 @@ class member_exprt:public exprt
 */
 inline const member_exprt &to_member_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_member && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_member);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Extract member must have one operand");
   return static_cast<const member_exprt &>(expr);
 }
 
@@ -3057,7 +3313,10 @@ inline const member_exprt &to_member_expr(const exprt &expr)
 */
 inline member_exprt &to_member_expr(exprt &expr)
 {
-  assert(expr.id()==ID_member && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_member);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Extract member must have one operand");
   return static_cast<member_exprt &>(expr);
 }
 
@@ -3088,7 +3347,8 @@ class isnan_exprt:public unary_predicate_exprt
 */
 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_isnan && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isnan);
+  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
   return static_cast<const isnan_exprt &>(expr);
 }
 
@@ -3097,7 +3357,8 @@ inline const isnan_exprt &to_isnan_expr(const exprt &expr)
 */
 inline isnan_exprt &to_isnan_expr(exprt &expr)
 {
-  assert(expr.id()==ID_isnan && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isnan);
+  DATA_INVARIANT(expr.operands().size()==1, "Is NaN must have one operand");
   return static_cast<isnan_exprt &>(expr);
 }
 
@@ -3128,7 +3389,10 @@ class isinf_exprt:public unary_predicate_exprt
 */
 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_isinf && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isinf);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Is infinite must have one operand");
   return static_cast<const isinf_exprt &>(expr);
 }
 
@@ -3137,7 +3401,10 @@ inline const isinf_exprt &to_isinf_expr(const exprt &expr)
 */
 inline isinf_exprt &to_isinf_expr(exprt &expr)
 {
-  assert(expr.id()==ID_isinf && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isinf);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "Is infinite must have one operand");
   return static_cast<isinf_exprt &>(expr);
 }
 
@@ -3168,7 +3435,8 @@ class isfinite_exprt:public unary_predicate_exprt
 */
 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_isfinite && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isfinite);
+  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
   return static_cast<const isfinite_exprt &>(expr);
 }
 
@@ -3177,7 +3445,8 @@ inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
 */
 inline isfinite_exprt &to_isfinite_expr(exprt &expr)
 {
-  assert(expr.id()==ID_isfinite && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isfinite);
+  DATA_INVARIANT(expr.operands().size()==1, "Is finite must have one operand");
   return static_cast<isfinite_exprt &>(expr);
 }
 
@@ -3208,7 +3477,8 @@ class isnormal_exprt:public unary_predicate_exprt
 */
 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_isnormal && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isnormal);
+  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
   return static_cast<const isnormal_exprt &>(expr);
 }
 
@@ -3217,7 +3487,8 @@ inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
 */
 inline isnormal_exprt &to_isnormal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_isnormal && expr.operands().size()==1);
+  PRECONDITION(expr.id()==ID_isnormal);
+  DATA_INVARIANT(expr.operands().size()==1, "Is normal must have one operand");
   return static_cast<isnormal_exprt &>(expr);
 }
 
@@ -3248,7 +3519,10 @@ class ieee_float_equal_exprt:public binary_relation_exprt
 */
 inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_equal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_ieee_float_equal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "IEEE equality must have two operands");
   return static_cast<const ieee_float_equal_exprt &>(expr);
 }
 
@@ -3257,11 +3531,14 @@ inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr)
 */
 inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_equal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_ieee_float_equal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "IEEE equality must have two operands");
   return static_cast<ieee_float_equal_exprt &>(expr);
 }
 
-/*! \brief IEEE-floating-point disequality
+/*! \brief IEEE floating-point disequality
 */
 class ieee_float_notequal_exprt:public binary_relation_exprt
 {
@@ -3290,7 +3567,10 @@ class ieee_float_notequal_exprt:public binary_relation_exprt
 inline const ieee_float_notequal_exprt &to_ieee_float_notequal_expr(
   const exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_notequal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_ieee_float_notequal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "IEEE inequality must have two operands");
   return static_cast<const ieee_float_notequal_exprt &>(expr);
 }
 
@@ -3299,11 +3579,14 @@ inline const ieee_float_notequal_exprt &to_ieee_float_notequal_expr(
 */
 inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_notequal && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_ieee_float_notequal);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "IEEE inequality must have two operands");
   return static_cast<ieee_float_notequal_exprt &>(expr);
 }
 
-/*! \brief IEEE-floating-point disequality
+/*! \brief IEEE floating-point operations
 */
 class ieee_float_op_exprt:public exprt
 {
@@ -3366,7 +3649,9 @@ class ieee_float_op_exprt:public exprt
 */
 inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr)
 {
-  assert(expr.operands().size()==3);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "IEEE float operations must have three arguments");
   return static_cast<const ieee_float_op_exprt &>(expr);
 }
 
@@ -3375,7 +3660,9 @@ inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr)
 */
 inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
 {
-  assert(expr.operands().size()==3);
+  DATA_INVARIANT(
+    expr.operands().size()==3,
+    "IEEE float operations must have three arguments");
   return static_cast<ieee_float_op_exprt &>(expr);
 }
 
@@ -3439,7 +3726,7 @@ class constant_exprt:public exprt
 */
 inline const constant_exprt &to_constant_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_constant);
+  PRECONDITION(expr.id()==ID_constant);
   return static_cast<const constant_exprt &>(expr);
 }
 
@@ -3448,7 +3735,7 @@ inline const constant_exprt &to_constant_expr(const exprt &expr)
 */
 inline constant_exprt &to_constant_expr(exprt &expr)
 {
-  assert(expr.id()==ID_constant);
+  PRECONDITION(expr.id()==ID_constant);
   return static_cast<constant_exprt &>(expr);
 }
 
@@ -3541,7 +3828,10 @@ class function_application_exprt:public exprt
 inline const function_application_exprt &to_function_application_expr(
   const exprt &expr)
 {
-  assert(expr.id()==ID_function_application && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_function_application);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Function application must have two operands");
   return static_cast<const function_application_exprt &>(expr);
 }
 
@@ -3550,7 +3840,10 @@ inline const function_application_exprt &to_function_application_expr(
 */
 inline function_application_exprt &to_function_application_expr(exprt &expr)
 {
-  assert(expr.id()==ID_function_application && expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_function_application);
+  DATA_INVARIANT(
+    expr.operands().size()==2,
+    "Function application must have two operands");
   return static_cast<function_application_exprt &>(expr);
 }
 
@@ -3593,7 +3886,10 @@ class concatenation_exprt:public exprt
 */
 inline const concatenation_exprt &to_concatenation_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_concatenation);
+  PRECONDITION(expr.id()==ID_concatenation);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Concatenation must have two or more operands");
   return static_cast<const concatenation_exprt &>(expr);
 }
 
@@ -3602,7 +3898,10 @@ inline const concatenation_exprt &to_concatenation_expr(const exprt &expr)
 */
 inline concatenation_exprt &to_concatenation_expr(exprt &expr)
 {
-  assert(expr.id()==ID_concatenation);
+  PRECONDITION(expr.id()==ID_concatenation);
+  // DATA_INVARIANT(
+  //   expr.operands().size()>=2,
+  //   "Concatenation must have two or more operands");
   return static_cast<concatenation_exprt &>(expr);
 }
 
@@ -3671,7 +3970,8 @@ class let_exprt:public exprt
 */
 inline const let_exprt &to_let_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_let && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_let);
+  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
   return static_cast<const let_exprt &>(expr);
 }
 
@@ -3680,7 +3980,8 @@ inline const let_exprt &to_let_expr(const exprt &expr)
 */
 inline let_exprt &to_let_expr(exprt &expr)
 {
-  assert(expr.id()==ID_let && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_let);
+  DATA_INVARIANT(expr.operands().size()==3, "Let must have three operands");
   return static_cast<let_exprt &>(expr);
 }