diff --git a/.travis.yml b/.travis.yml
index 0cf80acccf5..1145190171c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -159,7 +159,7 @@ install:
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}
diff --git a/regression/Makefile b/regression/Makefile
index b6d109b604a..87dcd7c93f3 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -6,6 +6,7 @@ DIRS = ansi-c \
        goto-instrument \
        goto-instrument-typedef \
        goto-diff \
+       invariants \
        test-script \
        # Empty last line
 
diff --git a/regression/cbmc/invariant-failure/main.c b/regression/cbmc/invariant-failure/main.c
deleted file mode 100644
index f8b643afbf2..00000000000
--- a/regression/cbmc/invariant-failure/main.c
+++ /dev/null
@@ -1,4 +0,0 @@
-int main()
-{
-  return 0;
-}
diff --git a/regression/invariants/.gitignore b/regression/invariants/.gitignore
new file mode 100644
index 00000000000..e54525b1ee9
--- /dev/null
+++ b/regression/invariants/.gitignore
@@ -0,0 +1 @@
+driver
diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile
new file mode 100644
index 00000000000..b561a960830
--- /dev/null
+++ b/regression/invariants/Makefile
@@ -0,0 +1,32 @@
+default: tests.log
+
+SRC = driver.cpp
+
+INCLUDES = -I ../../src
+
+OBJ += ../../src/util/util$(LIBEXT)
+
+include ../../src/config.inc
+include ../../src/common
+
+test: driver$(EXEEXT)
+	@if ! ../test.pl -c ../driver ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl driver$(EXEEXT)
+	@if ! ../test.pl -c ../driver ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+driver$(EXEEXT): $(OBJ)
+	$(LINKBIN)
diff --git a/regression/invariants/driver.cpp b/regression/invariants/driver.cpp
new file mode 100644
index 00000000000..824ae588c03
--- /dev/null
+++ b/regression/invariants/driver.cpp
@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+Module: Invariant violation testing
+
+Author: Chris Smowton, chris.smowton@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// Invariant violation testing
+
+#include <string>
+#include <sstream>
+#include <util/invariant.h>
+
+/// An example of structured invariants-- this contains fields to
+/// describe the error to a catcher, and also produces a human-readable
+/// message containing all the information for use by the current aborting
+/// invariant implementation and/or any generic error catcher in the future.
+class structured_error_testt: public invariant_failedt
+{
+  std::string pretty_print(int code, const std::string &desc)
+  {
+    std::ostringstream ret;
+    ret << "Error code: " << code
+        << "\nDescription: " << desc;
+    return ret.str();
+  }
+
+public:
+  const int error_code;
+  const std::string description;
+
+  structured_error_testt(
+    const std::string &file,
+    const std::string &function,
+    int line,
+    const std::string &backtrace,
+    int code,
+    const std::string &_description):
+    invariant_failedt(
+      file,
+      function,
+      line,
+      backtrace,
+      pretty_print(code, _description)),
+    error_code(code),
+    description(_description)
+  {
+  }
+};
+
+/// Causes an invariant failure dependent on first argument value.
+/// One ignored argument is accepted to conform with the test.pl script,
+/// which would be the input source file for other cbmc driver programs.
+/// Returns 1 on unexpected arguments.
+int main(int argc, char** argv)
+{
+  if(argc!=3)
+    return 1;
+  std::string arg=argv[1];
+  if(arg=="structured")
+    INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="string")
+    INVARIANT(false, "Test invariant failure");
+  else if(arg=="precondition-structured")
+    PRECONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="precondition-string")
+    PRECONDITION(false);
+  else if(arg=="postcondition-structured")
+    POSTCONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="postcondition-string")
+    POSTCONDITION(false);
+  else if(arg=="check-return-structured")
+    CHECK_RETURN_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="check-return-string")
+    CHECK_RETURN(false);
+  else if(arg=="unreachable-structured")
+    UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="unreachable-string")
+    UNREACHABLE;
+  else if(arg=="data-invariant-structured")
+    DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="data-invariant-string")
+    DATA_INVARIANT(false, "Test invariant failure");
+  else
+    return 1;
+}
diff --git a/regression/cbmc/invariant-failure/test.desc b/regression/invariants/invariant-failure/test.desc
similarity index 62%
rename from regression/cbmc/invariant-failure/test.desc
rename to regression/invariants/invariant-failure/test.desc
index 9966d66547a..70628a2e064 100644
--- a/regression/cbmc/invariant-failure/test.desc
+++ b/regression/invariants/invariant-failure/test.desc
@@ -1,8 +1,10 @@
 CORE
-main.c
---test-invariant-failure
+dummy_parameter.c
+string
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
+--- begin invariant violation report ---
+Test invariant failure
 Invariant check failed
 ^(Backtrace)|(Backtraces not supported)$
 --
diff --git a/regression/invariants/invariant-failure10/test.desc b/regression/invariants/invariant-failure10/test.desc
new file mode 100644
index 00000000000..fae345f2b2a
--- /dev/null
+++ b/regression/invariants/invariant-failure10/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+unreachable-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure11/test.desc b/regression/invariants/invariant-failure11/test.desc
new file mode 100644
index 00000000000..fc160b21308
--- /dev/null
+++ b/regression/invariants/invariant-failure11/test.desc
@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+data-invariant-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Test invariant failure
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure12/test.desc b/regression/invariants/invariant-failure12/test.desc
new file mode 100644
index 00000000000..498af6f2cc5
--- /dev/null
+++ b/regression/invariants/invariant-failure12/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+data-invariant-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure2/test.desc b/regression/invariants/invariant-failure2/test.desc
new file mode 100644
index 00000000000..daadab22c44
--- /dev/null
+++ b/regression/invariants/invariant-failure2/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure3/test.desc b/regression/invariants/invariant-failure3/test.desc
new file mode 100644
index 00000000000..42aba0fc5bd
--- /dev/null
+++ b/regression/invariants/invariant-failure3/test.desc
@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+precondition-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Precondition
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure4/test.desc b/regression/invariants/invariant-failure4/test.desc
new file mode 100644
index 00000000000..6339338d491
--- /dev/null
+++ b/regression/invariants/invariant-failure4/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+precondition-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure5/test.desc b/regression/invariants/invariant-failure5/test.desc
new file mode 100644
index 00000000000..f6f6971351f
--- /dev/null
+++ b/regression/invariants/invariant-failure5/test.desc
@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+postcondition-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Postcondition
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure6/test.desc b/regression/invariants/invariant-failure6/test.desc
new file mode 100644
index 00000000000..1b83f2630b1
--- /dev/null
+++ b/regression/invariants/invariant-failure6/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+postcondition-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure7/test.desc b/regression/invariants/invariant-failure7/test.desc
new file mode 100644
index 00000000000..9b25a5ac5e8
--- /dev/null
+++ b/regression/invariants/invariant-failure7/test.desc
@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+check-return-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Check return value
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure8/test.desc b/regression/invariants/invariant-failure8/test.desc
new file mode 100644
index 00000000000..1165b32a25f
--- /dev/null
+++ b/regression/invariants/invariant-failure8/test.desc
@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+check-return-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/invariants/invariant-failure9/test.desc b/regression/invariants/invariant-failure9/test.desc
new file mode 100644
index 00000000000..38aebd70d61
--- /dev/null
+++ b/regression/invariants/invariant-failure9/test.desc
@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+unreachable-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Unreachable
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 65a4386077b..2943d9a18d7 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -106,27 +106,6 @@ 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 d95e60eb25b..4d8e6753476 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -63,7 +63,6 @@ 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/util/invariant.cpp b/src/util/invariant.cpp
index b0047cccf40..eb63382ef76 100644
--- a/src/util/invariant.cpp
+++ b/src/util/invariant.cpp
@@ -12,10 +12,7 @@ Author: Martin Brain, martin.brain@diffblue.com
 #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
@@ -39,7 +36,7 @@ Author: Martin Brain, martin.brain@diffblue.com
 /// \return True <=> the entry has been successfully demangled and printed.
 static bool output_demangled_name(
   std::ostream &out,
-  const char * const stack_entry)
+  const std::string &stack_entry)
 {
   bool return_value=false;
 
@@ -75,40 +72,11 @@ static bool output_demangled_name(
 #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)
+/// Prints a back trace to 'out'
+/// \param out: Stream to print backtrace
+void print_backtrace(
+  std::ostream &out)
 {
-  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;
 
@@ -129,11 +97,39 @@ void check_invariant(
 #else
     out << "Backtraces not supported\n" << std::flush;
 #endif
+}
 
+/// Returns a backtrace
+/// \return backtrace with a file / function / line header.
+std::string get_backtrace()
+{
+  std::ostringstream ostr;
+  print_backtrace(ostr);
+  return ostr.str();
+}
 
-#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
-    abort();
-#else
-    throw invariant_failedt(out.str());
-#endif
+/// Dump exception report to stderr
+void report_exception_to_stderr(const invariant_failedt &reason)
+{
+  std::cerr << "--- begin invariant violation report ---\n";
+  std::cerr << reason.what() << '\n';
+  std::cerr << "--- end invariant violation report ---\n";
+}
+
+std::string invariant_failedt::get_invariant_failed_message(
+  const std::string &file,
+  const std::string &function,
+  int line,
+  const std::string &backtrace,
+  const std::string &reason)
+{
+  std::ostringstream out;
+  out << "Invariant check failed\n"
+      << "File " << file
+      << " function " << function
+      << " line " << line << '\n'
+      << "Reason: " << reason
+      << "Backtrace:\n"
+      << backtrace << '\n';
+  return out.str();
 }
diff --git a/src/util/invariant.h b/src/util/invariant.h
index e5bc07b3d5c..325020a0d6e 100644
--- a/src/util/invariant.h
+++ b/src/util/invariant.h
@@ -10,6 +10,9 @@ Author: Martin Brain, martin.brain@diffblue.com
 #define CPROVER_UTIL_INVARIANT_H
 
 #include <stdexcept>
+#include <type_traits>
+#include <string>
+#include <cstdlib>
 
 /*
 ** Invariants document conditions that the programmer believes to
@@ -42,7 +45,7 @@ Author: Martin Brain, martin.brain@diffblue.com
 **       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 
+** invariant is true after it has been executed.  Applications are
 ** encouraged to (at least) catch exceptions at the top level and
 ** output them.
 **
@@ -51,13 +54,63 @@ Author: Martin Brain, martin.brain@diffblue.com
 ** CPROVER_INVARIANT_* macros.
 */
 
+/// A logic error, augmented with a distinguished field to hold a backtrace.
+/// Classes that extend this one should share the same initial constructor
+/// parameters: their constructor signature should be of the form:
+/// my_invariantt::my_invariantt(
+///   const std::string &file,
+///   const std::string &function,
+///   int line,
+///   const std::string &backtrace,
+///   T1 arg1,
+///   T2 arg2 ...
+///   Tn argn)
+/// It should pretty-print the T1 ... Tn arguments and pass it as `reason` to
+/// invariant_failedt's constructor, or else simply pass a reason string
+/// through.
+/// Conforming to this pattern allows the class to be used with the INVARIANT
+/// family of macros, allowing constructs like
+/// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)`
+///
 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) {}
-};
+ private:
+  std::string get_invariant_failed_message(
+    const std::string &file,
+    const std::string &function,
+    int line,
+    const std::string &backtrace,
+    const std::string &reason);
+
+ public:
 
+  const std::string file;
+  const std::string function;
+  const int line;
+  const std::string backtrace;
+  const std::string reason;
+
+  invariant_failedt(
+    const std::string &_file,
+    const std::string &_function,
+    int _line,
+    const std::string &_backtrace,
+    const std::string &_reason):
+    logic_error(
+      get_invariant_failed_message(
+        _file,
+        _function,
+        _line,
+        _backtrace,
+        _reason)),
+    file(_file),
+    function(_function),
+    line(_line),
+    backtrace(_backtrace),
+    reason(_reason)
+  {
+  }
+};
 
 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
 // Used to allow CPROVER to check itself
@@ -70,66 +123,129 @@ class invariant_failedt: public std::logic_error
 // 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)
-
+#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))
-
+#define INVARIANT(CONDITION, REASON, ...) assert((CONDITION) && ((REASON), true))
 
 #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,
+void print_backtrace(std::ostream &out);
+
+std::string get_backtrace();
+
+void report_exception_to_stderr(const invariant_failedt &);
+
+/// Takes a backtrace, gives it to the reason structure, then aborts, printing
+/// reason.what() (which therefore includes the backtrace).
+/// In future this may throw `reason` instead of aborting.
+/// \param ET : (template type parameter), type of exception to construct
+/// \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 params : (variadic) parameters to forward to ET's constructor
+///  its backtrace member will be set before it is used.
+template<class ET, typename ...Params>
+typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
+invariant_violated_structured(
+  const std::string &file,
+  const std::string &function,
   const int line,
-  const bool condition,
-  const char * const reason);
+  Params &&... params)
+{
+  std::string backtrace=get_backtrace();
+  ET to_throw(file, function, line, backtrace, std::forward<Params>(params)...);
+  // We now have a structured exception ready to use;
+  // in future this is the place to put a 'throw'.
+  report_exception_to_stderr(to_throw);
+  abort();
+}
 
+/// Takes a backtrace, constructs an invariant_violatedt from reason and the
+/// backtrace, aborts printing the invariant's description.
+/// In future this may throw rather than aborting.
+/// \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 reason : brief description of the invariant violation.
+inline void invariant_violated_string(
+  const std::string &file,
+  const std::string &function,
+  const int line,
+  const std::string &reason)
+{
+  invariant_violated_structured<invariant_failedt>(
+    file,
+    function,
+    line,
+    reason);
+}
+
+// These require a trailing semicolon by the user, such that INVARIANT
+// behaves syntactically like a function call.
+// NOLINT as macro definitions confuse the linter it seems.
 #ifdef _MSC_VER
-#define INVARIANT(CONDITION, REASON) \
-  check_invariant(__FILE__, __FUNCTION__, __LINE__, (CONDITION), (REASON))
+#define __this_function__ __FUNCTION__
 #else
-#define INVARIANT(CONDITION, REASON)                                    \
-  check_invariant(__FILE__, __func__, __LINE__, (CONDITION), (REASON))
+#define __this_function__ __func__
 #endif
 
+#define INVARIANT(CONDITION, REASON) \
+  do /* NOLINT */ \
+  { \
+  if(!(CONDITION)) \
+    invariant_violated_string(__FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */  \
+  } while(0)
 
-#endif
-
+#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
+  do /* NOLINT */ \
+  { \
+  if(!(CONDITION)) \
+    invariant_violated_structured<TYPENAME>(__FILE__, __this_function__, __LINE__, __VA_ARGS__); /* NOLINT */ \
+  } while(0)
 
+#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
 
-// Short hand macros
+// Short hand macros. The second variant of each one permits including an
+// explanation or structured exception, in which case they are synonyms
+// for INVARIANT.
 
 // 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")
+#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
+  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // 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")
+#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
+  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // 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")
+#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...)  \
+  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // This should be used to mark dead code
 #define UNREACHABLE INVARIANT(false, "Unreachable")
+#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
+  INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
 
 // 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)
-
+#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
+  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
 
 // Legacy annotations