diff --git a/src/util/std_code.h b/src/util/std_code.h
index 9f0f0a62e21..5e282b95c49 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -10,11 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_STD_CODE_H
 #define CPROVER_UTIL_STD_CODE_H
 
-#include <cassert>
 #include <list>
 
 #include "expr.h"
 #include "expr_cast.h"
+#include "invariant.h"
 
 /// Data structure for representing an arbitrary statement in a program. Every
 /// specific type of statement (e.g. block of statements, assignment,
@@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class codet:public exprt
 {
 public:
-  DEPRECATED("Use codet(statement) instead")
+  DEPRECATED("use codet(statement) instead")
   codet():exprt(ID_code, typet(ID_code))
   {
   }
@@ -86,13 +86,13 @@ template<> inline bool can_cast_expr<codet>(const exprt &base)
 
 inline const codet &to_code(const exprt &expr)
 {
-  assert(expr.id()==ID_code);
+  PRECONDITION(expr.id() == ID_code);
   return static_cast<const codet &>(expr);
 }
 
 inline codet &to_code(exprt &expr)
 {
-  assert(expr.id()==ID_code);
+  PRECONDITION(expr.id() == ID_code);
   return static_cast<codet &>(expr);
 }
 
@@ -155,7 +155,8 @@ class code_blockt:public codet
       }
       else if(statement==ID_label)
       {
-        assert(last->operands().size()==1);
+        DATA_INVARIANT(
+          last->operands().size() == 1, "label must have one operand");
         last=&(to_code(last->op0()));
       }
       else
@@ -176,13 +177,13 @@ template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
 
 inline const code_blockt &to_code_block(const codet &code)
 {
-  assert(code.get_statement()==ID_block);
+  PRECONDITION(code.get_statement() == ID_block);
   return static_cast<const code_blockt &>(code);
 }
 
 inline code_blockt &to_code_block(codet &code)
 {
-  assert(code.get_statement()==ID_block);
+  PRECONDITION(code.get_statement() == ID_block);
   return static_cast<code_blockt &>(code);
 }
 
@@ -247,18 +248,22 @@ template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
 
 inline void validate_expr(const code_assignt & x)
 {
-  validate_operands(x, 2, "Assignment must have two operands");
+  validate_operands(x, 2, "assignment must have two operands");
 }
 
 inline const code_assignt &to_code_assign(const codet &code)
 {
-  assert(code.get_statement()==ID_assign && code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_assign);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "assignment must have two operands");
   return static_cast<const code_assignt &>(code);
 }
 
 inline code_assignt &to_code_assign(codet &code)
 {
-  assert(code.get_statement()==ID_assign && code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_assign);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "assignment must have two operands");
   return static_cast<code_assignt &>(code);
 }
 
@@ -269,7 +274,7 @@ inline code_assignt &to_code_assign(codet &code)
 class code_declt:public codet
 {
 public:
-  DEPRECATED("Use code_declt(symbol) instead")
+  DEPRECATED("use code_declt(symbol) instead")
   code_declt():codet(ID_decl)
   {
     operands().resize(1);
@@ -300,20 +305,26 @@ template<> inline bool can_cast_expr<code_declt>(const exprt &base)
 
 inline void validate_expr(const code_declt &x)
 {
-  validate_operands(x, 1, "Decls must have one or more operands", true);
+  validate_operands(x, 1, "decls must have one or more operands", true);
 }
 
 inline const code_declt &to_code_decl(const codet &code)
 {
+  PRECONDITION(code.get_statement() == ID_decl);
+
   // will be size()==1 in the future
-  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
+  DATA_INVARIANT(
+    code.operands().size() >= 1, "decls must have one or more operands");
   return static_cast<const code_declt &>(code);
 }
 
 inline code_declt &to_code_decl(codet &code)
 {
+  PRECONDITION(code.get_statement() == ID_decl);
+
   // will be size()==1 in the future
-  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
+  DATA_INVARIANT(
+    code.operands().size() >= 1, "decls must have one or more operands");
   return static_cast<code_declt &>(code);
 }
 
@@ -322,7 +333,7 @@ inline code_declt &to_code_decl(codet &code)
 class code_deadt:public codet
 {
 public:
-  DEPRECATED("Use code_deadt(symbol) instead")
+  DEPRECATED("use code_deadt(symbol) instead")
   code_deadt():codet(ID_dead)
   {
     operands().resize(1);
@@ -353,18 +364,22 @@ template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
 
 inline void validate_expr(const code_deadt &x)
 {
-  validate_operands(x, 1, "Dead code must have one operand");
+  validate_operands(x, 1, "dead statement must have one operand");
 }
 
 inline const code_deadt &to_code_dead(const codet &code)
 {
-  assert(code.get_statement()==ID_dead && code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_dead);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "dead statement must have one operand");
   return static_cast<const code_deadt &>(code);
 }
 
 inline code_deadt &to_code_dead(codet &code)
 {
-  assert(code.get_statement()==ID_dead && code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_dead);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "dead statement must have one operand");
   return static_cast<code_deadt &>(code);
 }
 
@@ -372,7 +387,7 @@ inline code_deadt &to_code_dead(codet &code)
 class code_assumet:public codet
 {
 public:
-  DEPRECATED("Use code_assumet(expr) instead")
+  DEPRECATED("use code_assumet(expr) instead")
   code_assumet():codet(ID_assume)
   {
     operands().resize(1);
@@ -404,13 +419,13 @@ template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
 
 inline const code_assumet &to_code_assume(const codet &code)
 {
-  assert(code.get_statement()==ID_assume);
+  PRECONDITION(code.get_statement() == ID_assume);
   return static_cast<const code_assumet &>(code);
 }
 
 inline code_assumet &to_code_assume(codet &code)
 {
-  assert(code.get_statement()==ID_assume);
+  PRECONDITION(code.get_statement() == ID_assume);
   return static_cast<code_assumet &>(code);
 }
 
@@ -419,7 +434,7 @@ inline code_assumet &to_code_assume(codet &code)
 class code_assertt:public codet
 {
 public:
-  DEPRECATED("Use code_assertt(expr) instead")
+  DEPRECATED("use code_assertt(expr) instead")
   code_assertt():codet(ID_assert)
   {
     operands().resize(1);
@@ -451,13 +466,13 @@ template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
 
 inline const code_assertt &to_code_assert(const codet &code)
 {
-  assert(code.get_statement()==ID_assert);
+  PRECONDITION(code.get_statement() == ID_assert);
   return static_cast<const code_assertt &>(code);
 }
 
 inline code_assertt &to_code_assert(codet &code)
 {
-  assert(code.get_statement()==ID_assert);
+  PRECONDITION(code.get_statement() == ID_assert);
   return static_cast<code_assertt &>(code);
 }
 
@@ -530,20 +545,22 @@ template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
 
 inline void validate_expr(const code_ifthenelset &x)
 {
-  validate_operands(x, 3, "If-then-else must have three operands");
+  validate_operands(x, 3, "if-then-else must have three operands");
 }
 
 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
 {
-  assert(code.get_statement()==ID_ifthenelse &&
-         code.operands().size()==3);
+  PRECONDITION(code.get_statement() == ID_ifthenelse);
+  DATA_INVARIANT(
+    code.operands().size() == 3, "if-then-else must have three operands");
   return static_cast<const code_ifthenelset &>(code);
 }
 
 inline code_ifthenelset &to_code_ifthenelse(codet &code)
 {
-  assert(code.get_statement()==ID_ifthenelse &&
-         code.operands().size()==3);
+  PRECONDITION(code.get_statement() == ID_ifthenelse);
+  DATA_INVARIANT(
+    code.operands().size() == 3, "if-then-else must have three operands");
   return static_cast<code_ifthenelset &>(code);
 }
 
@@ -551,7 +568,7 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code)
 class code_switcht:public codet
 {
 public:
-  DEPRECATED("Use code_switcht(value, body) instead")
+  DEPRECATED("use code_switcht(value, body) instead")
   code_switcht():codet(ID_switch)
   {
     operands().resize(2);
@@ -592,20 +609,20 @@ template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
 
 inline void validate_expr(const code_switcht &x)
 {
-  validate_operands(x, 2, "Switch must have two operands");
+  validate_operands(x, 2, "switch must have two operands");
 }
 
 inline const code_switcht &to_code_switch(const codet &code)
 {
-  assert(code.get_statement()==ID_switch &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_switch);
+  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
   return static_cast<const code_switcht &>(code);
 }
 
 inline code_switcht &to_code_switch(codet &code)
 {
-  assert(code.get_statement()==ID_switch &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_switch);
+  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
   return static_cast<code_switcht &>(code);
 }
 
@@ -613,7 +630,7 @@ inline code_switcht &to_code_switch(codet &code)
 class code_whilet:public codet
 {
 public:
-  DEPRECATED("Use code_whilet(cond, body) instead")
+  DEPRECATED("use code_whilet(cond, body) instead")
   code_whilet():codet(ID_while)
   {
     operands().resize(2);
@@ -654,20 +671,20 @@ template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
 
 inline void validate_expr(const code_whilet &x)
 {
-  validate_operands(x, 2, "While must have two operands");
+  validate_operands(x, 2, "while must have two operands");
 }
 
 inline const code_whilet &to_code_while(const codet &code)
 {
-  assert(code.get_statement()==ID_while &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_while);
+  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
   return static_cast<const code_whilet &>(code);
 }
 
 inline code_whilet &to_code_while(codet &code)
 {
-  assert(code.get_statement()==ID_while &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_while);
+  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
   return static_cast<code_whilet &>(code);
 }
 
@@ -675,7 +692,7 @@ inline code_whilet &to_code_while(codet &code)
 class code_dowhilet:public codet
 {
 public:
-  DEPRECATED("Use code_dowhilet(cond, body) instead")
+  DEPRECATED("use code_dowhilet(cond, body) instead")
   code_dowhilet():codet(ID_dowhile)
   {
     operands().resize(2);
@@ -716,20 +733,22 @@ template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
 
 inline void validate_expr(const code_dowhilet &x)
 {
-  validate_operands(x, 2, "Do-while must have two operands");
+  validate_operands(x, 2, "do-while must have two operands");
 }
 
 inline const code_dowhilet &to_code_dowhile(const codet &code)
 {
-  assert(code.get_statement()==ID_dowhile &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_dowhile);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "do-while must have two operands");
   return static_cast<const code_dowhilet &>(code);
 }
 
 inline code_dowhilet &to_code_dowhile(codet &code)
 {
-  assert(code.get_statement()==ID_dowhile &&
-         code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_dowhile);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "do-while must have two operands");
   return static_cast<code_dowhilet &>(code);
 }
 
@@ -791,20 +810,20 @@ template<> inline bool can_cast_expr<code_fort>(const exprt &base)
 
 inline void validate_expr(const code_fort &x)
 {
-  validate_operands(x, 4, "For must have four operands");
+  validate_operands(x, 4, "for must have four operands");
 }
 
 inline const code_fort &to_code_for(const codet &code)
 {
-  assert(code.get_statement()==ID_for &&
-         code.operands().size()==4);
+  PRECONDITION(code.get_statement() == ID_for);
+  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
   return static_cast<const code_fort &>(code);
 }
 
 inline code_fort &to_code_for(codet &code)
 {
-  assert(code.get_statement()==ID_for &&
-         code.operands().size()==4);
+  PRECONDITION(code.get_statement() == ID_for);
+  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
   return static_cast<code_fort &>(code);
 }
 
@@ -812,7 +831,7 @@ inline code_fort &to_code_for(codet &code)
 class code_gotot:public codet
 {
 public:
-  DEPRECATED("Use code_gotot(label) instead")
+  DEPRECATED("use code_gotot(label) instead")
   code_gotot():codet(ID_goto)
   {
   }
@@ -840,20 +859,20 @@ template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
 
 inline void validate_expr(const code_gotot &x)
 {
-  validate_operands(x, 0, "Goto must not have operands");
+  validate_operands(x, 0, "goto must not have operands");
 }
 
 inline const code_gotot &to_code_goto(const codet &code)
 {
-  assert(code.get_statement()==ID_goto &&
-         code.operands().empty());
+  PRECONDITION(code.get_statement() == ID_goto);
+  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
   return static_cast<const code_gotot &>(code);
 }
 
 inline code_gotot &to_code_goto(codet &code)
 {
-  assert(code.get_statement()==ID_goto &&
-         code.operands().empty());
+  PRECONDITION(code.get_statement() == ID_goto);
+  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
   return static_cast<code_gotot &>(code);
 }
 
@@ -944,13 +963,13 @@ template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
 
 inline const code_function_callt &to_code_function_call(const codet &code)
 {
-  assert(code.get_statement()==ID_function_call);
+  PRECONDITION(code.get_statement() == ID_function_call);
   return static_cast<const code_function_callt &>(code);
 }
 
 inline code_function_callt &to_code_function_call(codet &code)
 {
-  assert(code.get_statement()==ID_function_call);
+  PRECONDITION(code.get_statement() == ID_function_call);
   return static_cast<code_function_callt &>(code);
 }
 
@@ -997,13 +1016,13 @@ template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
 
 inline const code_returnt &to_code_return(const codet &code)
 {
-  assert(code.get_statement()==ID_return);
+  PRECONDITION(code.get_statement() == ID_return);
   return static_cast<const code_returnt &>(code);
 }
 
 inline code_returnt &to_code_return(codet &code)
 {
-  assert(code.get_statement()==ID_return);
+  PRECONDITION(code.get_statement() == ID_return);
   return static_cast<code_returnt &>(code);
 }
 
@@ -1011,7 +1030,7 @@ inline code_returnt &to_code_return(codet &code)
 class code_labelt:public codet
 {
 public:
-  DEPRECATED("Use code_labelt(label) instead")
+  DEPRECATED("use code_labelt(label) instead")
   code_labelt():codet(ID_label)
   {
     operands().resize(1);
@@ -1059,18 +1078,20 @@ template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
 
 inline void validate_expr(const code_labelt &x)
 {
-  validate_operands(x, 1, "Label must have one operand");
+  validate_operands(x, 1, "label must have one operand");
 }
 
 inline const code_labelt &to_code_label(const codet &code)
 {
-  assert(code.get_statement()==ID_label && code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_label);
+  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
   return static_cast<const code_labelt &>(code);
 }
 
 inline code_labelt &to_code_label(codet &code)
 {
-  assert(code.get_statement()==ID_label && code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_label);
+  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
   return static_cast<code_labelt &>(code);
 }
 
@@ -1079,7 +1100,7 @@ inline code_labelt &to_code_label(codet &code)
 class code_switch_caset:public codet
 {
 public:
-  DEPRECATED("Use code_switch_caset(case_op, code) instead")
+  DEPRECATED("use code_switch_caset(case_op, code) instead")
   code_switch_caset():codet(ID_switch_case)
   {
     operands().resize(2);
@@ -1129,18 +1150,22 @@ template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
 
 inline void validate_expr(const code_switch_caset &x)
 {
-  validate_operands(x, 2, "Switch-case must have two operands");
+  validate_operands(x, 2, "switch-case must have two operands");
 }
 
 inline const code_switch_caset &to_code_switch_case(const codet &code)
 {
-  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_switch_case);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "switch-case must have two operands");
   return static_cast<const code_switch_caset &>(code);
 }
 
 inline code_switch_caset &to_code_switch_case(codet &code)
 {
-  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
+  PRECONDITION(code.get_statement() == ID_switch_case);
+  DATA_INVARIANT(
+    code.operands().size() == 2, "switch-case must have two operands");
   return static_cast<code_switch_caset &>(code);
 }
 
@@ -1164,13 +1189,13 @@ template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
 
 inline const code_breakt &to_code_break(const codet &code)
 {
-  assert(code.get_statement()==ID_break);
+  PRECONDITION(code.get_statement() == ID_break);
   return static_cast<const code_breakt &>(code);
 }
 
 inline code_breakt &to_code_break(codet &code)
 {
-  assert(code.get_statement()==ID_break);
+  PRECONDITION(code.get_statement() == ID_break);
   return static_cast<code_breakt &>(code);
 }
 
@@ -1194,13 +1219,13 @@ template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
 
 inline const code_continuet &to_code_continue(const codet &code)
 {
-  assert(code.get_statement()==ID_continue);
+  PRECONDITION(code.get_statement() == ID_continue);
   return static_cast<const code_continuet &>(code);
 }
 
 inline code_continuet &to_code_continue(codet &code)
 {
-  assert(code.get_statement()==ID_continue);
+  PRECONDITION(code.get_statement() == ID_continue);
   return static_cast<code_continuet &>(code);
 }
 
@@ -1238,13 +1263,13 @@ template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
 
 inline code_asmt &to_code_asm(codet &code)
 {
-  assert(code.get_statement()==ID_asm);
+  PRECONDITION(code.get_statement() == ID_asm);
   return static_cast<code_asmt &>(code);
 }
 
 inline const code_asmt &to_code_asm(const codet &code)
 {
-  assert(code.get_statement()==ID_asm);
+  PRECONDITION(code.get_statement() == ID_asm);
   return static_cast<const code_asmt &>(code);
 }
 
@@ -1253,7 +1278,7 @@ inline const code_asmt &to_code_asm(const codet &code)
 class code_expressiont:public codet
 {
 public:
-  DEPRECATED("Use code_expressiont(expr) instead")
+  DEPRECATED("use code_expressiont(expr) instead")
   code_expressiont():codet(ID_expression)
   {
     operands().resize(1);
@@ -1282,20 +1307,22 @@ template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
 
 inline void validate_expr(const code_expressiont &x)
 {
-  validate_operands(x, 1, "Expression must have one operand");
+  validate_operands(x, 1, "expression statement must have one operand");
 }
 
 inline code_expressiont &to_code_expression(codet &code)
 {
-  assert(code.get_statement()==ID_expression &&
-         code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_expression);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "expression statement must have one operand");
   return static_cast<code_expressiont &>(code);
 }
 
 inline const code_expressiont &to_code_expression(const codet &code)
 {
-  assert(code.get_statement()==ID_expression &&
-         code.operands().size()==1);
+  PRECONDITION(code.get_statement() == ID_expression);
+  DATA_INVARIANT(
+    code.operands().size() == 1, "expression statement must have one operand");
   return static_cast<const code_expressiont &>(code);
 }
 
@@ -1307,13 +1334,13 @@ inline const code_expressiont &to_code_expression(const codet &code)
 class side_effect_exprt:public exprt
 {
 public:
-  DEPRECATED("Use side_effect_exprt(statement, type, loc) instead")
+  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
   explicit side_effect_exprt(const irep_idt &statement) : exprt(ID_side_effect)
   {
     set_statement(statement);
   }
 
-  DEPRECATED("Use side_effect_exprt(statement, type, loc) instead")
+  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
   side_effect_exprt(const irep_idt &statement, const typet &_type):
     exprt(ID_side_effect, _type)
   {
@@ -1361,13 +1388,13 @@ template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
 
 inline side_effect_exprt &to_side_effect_expr(exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
+  PRECONDITION(expr.id() == ID_side_effect);
   return static_cast<side_effect_exprt &>(expr);
 }
 
 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
+  PRECONDITION(expr.id() == ID_side_effect);
   return static_cast<const side_effect_exprt &>(expr);
 }
 
@@ -1375,13 +1402,13 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
 class side_effect_expr_nondett:public side_effect_exprt
 {
 public:
-  DEPRECATED("Use side_effect_expr_nondett(statement, type, loc) instead")
+  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
   side_effect_expr_nondett():side_effect_exprt(ID_nondet)
   {
     set_nullable(true);
   }
 
-  DEPRECATED("Use side_effect_expr_nondett(statement, type, loc) instead")
+  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
   explicit side_effect_expr_nondett(const typet &_type):
     side_effect_exprt(ID_nondet, _type)
   {
@@ -1413,7 +1440,7 @@ inline bool can_cast_expr<side_effect_expr_nondett>(const exprt &base)
 inline side_effect_expr_nondett &to_side_effect_expr_nondet(exprt &expr)
 {
   auto &side_effect_expr_nondet=to_side_effect_expr(expr);
-  assert(side_effect_expr_nondet.get_statement()==ID_nondet);
+  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
   return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
 }
 
@@ -1421,7 +1448,7 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet(
   const exprt &expr)
 {
   const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
-  assert(side_effect_expr_nondet.get_statement()==ID_nondet);
+  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
   return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
 }
 
@@ -1430,7 +1457,7 @@ class side_effect_expr_function_callt:public side_effect_exprt
 {
 public:
   DEPRECATED(
-    "Use side_effect_expr_function_callt("
+    "use side_effect_expr_function_callt("
     "function, arguments, type, loc) instead")
   side_effect_expr_function_callt()
     : side_effect_exprt(ID_function_call, typet(), source_locationt())
@@ -1440,7 +1467,7 @@ class side_effect_expr_function_callt:public side_effect_exprt
   }
 
   DEPRECATED(
-    "Use side_effect_expr_function_callt("
+    "use side_effect_expr_function_callt("
     "function, arguments, type, loc) instead")
   side_effect_expr_function_callt(
     const exprt &_function,
@@ -1454,7 +1481,7 @@ class side_effect_expr_function_callt:public side_effect_exprt
   }
 
   DEPRECATED(
-    "Use side_effect_expr_function_callt("
+    "use side_effect_expr_function_callt("
     "function, arguments, type, loc) instead")
   side_effect_expr_function_callt(
     const exprt &_function,
@@ -1507,16 +1534,16 @@ inline bool can_cast_expr<side_effect_expr_function_callt>(const exprt &base)
 inline side_effect_expr_function_callt
   &to_side_effect_expr_function_call(exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
-  assert(expr.get(ID_statement)==ID_function_call);
+  PRECONDITION(expr.id() == ID_side_effect);
+  PRECONDITION(expr.get(ID_statement) == ID_function_call);
   return static_cast<side_effect_expr_function_callt &>(expr);
 }
 
 inline const side_effect_expr_function_callt
   &to_side_effect_expr_function_call(const exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
-  assert(expr.get(ID_statement)==ID_function_call);
+  PRECONDITION(expr.id() == ID_side_effect);
+  PRECONDITION(expr.get(ID_statement) == ID_function_call);
   return static_cast<const side_effect_expr_function_callt &>(expr);
 }
 
@@ -1525,7 +1552,7 @@ inline const side_effect_expr_function_callt
 class side_effect_expr_throwt:public side_effect_exprt
 {
 public:
-  DEPRECATED("Use side_effect_expr_throwt(exception_list) instead")
+  DEPRECATED("use side_effect_expr_throwt(exception_list) instead")
   side_effect_expr_throwt():side_effect_exprt(ID_throw)
   {
   }
@@ -1551,16 +1578,16 @@ inline bool can_cast_expr<side_effect_expr_throwt>(const exprt &base)
 
 inline side_effect_expr_throwt &to_side_effect_expr_throw(exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
-  assert(expr.get(ID_statement)==ID_throw);
+  PRECONDITION(expr.id() == ID_side_effect);
+  PRECONDITION(expr.get(ID_statement) == ID_throw);
   return static_cast<side_effect_expr_throwt &>(expr);
 }
 
 inline const side_effect_expr_throwt &to_side_effect_expr_throw(
   const exprt &expr)
 {
-  assert(expr.id()==ID_side_effect);
-  assert(expr.get(ID_statement)==ID_throw);
+  PRECONDITION(expr.id() == ID_side_effect);
+  PRECONDITION(expr.get(ID_statement) == ID_throw);
   return static_cast<const side_effect_expr_throwt &>(expr);
 }
 
@@ -1650,13 +1677,13 @@ template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
 
 static inline code_push_catcht &to_code_push_catch(codet &code)
 {
-  assert(code.get_statement()==ID_push_catch);
+  PRECONDITION(code.get_statement() == ID_push_catch);
   return static_cast<code_push_catcht &>(code);
 }
 
 static inline const code_push_catcht &to_code_push_catch(const codet &code)
 {
-  assert(code.get_statement()==ID_push_catch);
+  PRECONDITION(code.get_statement() == ID_push_catch);
   return static_cast<const code_push_catcht &>(code);
 }
 
@@ -1681,13 +1708,13 @@ template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
 
 static inline code_pop_catcht &to_code_pop_catch(codet &code)
 {
-  assert(code.get_statement()==ID_pop_catch);
+  PRECONDITION(code.get_statement() == ID_pop_catch);
   return static_cast<code_pop_catcht &>(code);
 }
 
 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
 {
-  assert(code.get_statement()==ID_pop_catch);
+  PRECONDITION(code.get_statement() == ID_pop_catch);
   return static_cast<const code_pop_catcht &>(code);
 }
 
@@ -1726,13 +1753,13 @@ template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
 
 static inline code_landingpadt &to_code_landingpad(codet &code)
 {
-  assert(code.get_statement()==ID_exception_landingpad);
+  PRECONDITION(code.get_statement() == ID_exception_landingpad);
   return static_cast<code_landingpadt &>(code);
 }
 
 static inline const code_landingpadt &to_code_landingpad(const codet &code)
 {
-  assert(code.get_statement()==ID_exception_landingpad);
+  PRECONDITION(code.get_statement() == ID_exception_landingpad);
   return static_cast<const code_landingpadt &>(code);
 }
 
@@ -1757,25 +1784,25 @@ class code_try_catcht:public codet
 
   code_declt &get_catch_decl(unsigned i)
   {
-    assert((2*i+2)<operands().size());
+    PRECONDITION((2 * i + 2) < operands().size());
     return to_code_decl(to_code(operands()[2*i+1]));
   }
 
   const code_declt &get_catch_decl(unsigned i) const
   {
-    assert((2*i+2)<operands().size());
+    PRECONDITION((2 * i + 2) < operands().size());
     return to_code_decl(to_code(operands()[2*i+1]));
   }
 
   codet &get_catch_code(unsigned i)
   {
-    assert((2*i+2)<operands().size());
+    PRECONDITION((2 * i + 2) < operands().size());
     return to_code(operands()[2*i+2]);
   }
 
   const codet &get_catch_code(unsigned i) const
   {
-    assert((2*i+2)<operands().size());
+    PRECONDITION((2 * i + 2) < operands().size());
     return to_code(operands()[2*i+2]);
   }
 
@@ -1794,18 +1821,22 @@ template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
 
 inline void validate_expr(const code_try_catcht &x)
 {
-  validate_operands(x, 3, "Try-catch must have three or more operands", true);
+  validate_operands(x, 3, "try-catch must have three or more operands", true);
 }
 
 inline const code_try_catcht &to_code_try_catch(const codet &code)
 {
-  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
+  PRECONDITION(code.get_statement() == ID_try_catch);
+  DATA_INVARIANT(
+    code.operands().size() >= 3, "try-catch must have three or more operands");
   return static_cast<const code_try_catcht &>(code);
 }
 
 inline code_try_catcht &to_code_try_catch(codet &code)
 {
-  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
+  PRECONDITION(code.get_statement() == ID_try_catch);
+  DATA_INVARIANT(
+    code.operands().size() >= 3, "try-catch must have three or more operands");
   return static_cast<code_try_catcht &>(code);
 }