diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp
index 5686b41400c..95bfbc53d98 100644
--- a/src/goto-programs/goto_convert_exceptions.cpp
+++ b/src/goto-programs/goto_convert_exceptions.cpp
@@ -18,12 +18,10 @@ void goto_convertt::convert_msc_try_finally(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() << "msc_try_finally expects two arguments" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 2,
+    "msc_try_finally expects two arguments",
+    code.find_source_location());
 
   goto_programt tmp;
   tmp.add_instruction(SKIP)->source_location=code.source_location();
@@ -57,12 +55,10 @@ void goto_convertt::convert_msc_try_except(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location=code.find_source_location();
-    error() << "msc_try_except expects three arguments" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 3,
+    "msc_try_except expects three arguments",
+    code.find_source_location());
 
   convert(to_code(code.op0()), dest, mode);
 
@@ -74,12 +70,8 @@ void goto_convertt::convert_msc_leave(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(!targets.leave_set)
-  {
-    error().source_location=code.find_source_location();
-    error() << "leave without target" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    targets.leave_set, "leave without target", code.find_source_location());
 
   // need to process destructor stack
   for(std::size_t d=targets.destructor_stack.size();
@@ -101,7 +93,10 @@ void goto_convertt::convert_try_catch(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  assert(code.operands().size()>=2);
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() >= 2,
+    "try_catch expects at least two arguments",
+    code.find_source_location());
 
   // add the CATCH-push instruction to 'dest'
   goto_programt::targett catch_push_instruction=dest.add_instruction();
@@ -159,12 +154,10 @@ void goto_convertt::convert_CPROVER_try_catch(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() << "CPROVER_try_catch expects two arguments" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 2,
+    "CPROVER_try_catch expects two arguments",
+    code.find_source_location());
 
   // this is where we go after 'throw'
   goto_programt tmp;
@@ -235,12 +228,10 @@ void goto_convertt::convert_CPROVER_try_finally(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() << "CPROVER_try_finally expects two arguments" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 2,
+    "CPROVER_try_finally expects two arguments",
+    code.find_source_location());
 
   // first put 'finally' code onto destructor stack
   targets.destructor_stack.push_back(to_code(code.op1()));
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index cbb05af524d..0df30f68679 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -60,12 +60,10 @@ void goto_convertt::remove_assignment(
           statement==ID_assign_bitxor ||
           statement==ID_assign_bitor)
   {
-    if(expr.operands().size()!=2)
-    {
-      error().source_location=expr.find_source_location();
-      error() << statement << " takes two arguments" << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      expr.operands().size() == 2,
+      id2string(statement) + " expects two arguments",
+      expr.find_source_location());
 
     irep_idt new_id;
 
@@ -93,10 +91,7 @@ void goto_convertt::remove_assignment(
       new_id=ID_bitor;
     else
     {
-      error().source_location=expr.find_source_location();
-      error() << "assignment `" << statement << "' not yet supported"
-              << eom;
-      throw 0;
+      UNREACHABLE;
     }
 
     exprt rhs;
@@ -143,17 +138,16 @@ void goto_convertt::remove_pre(
   bool result_is_used,
   const irep_idt &mode)
 {
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "preincrement/predecrement must have one operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == 1,
+    "preincrement/predecrement must have one operand",
+    expr.find_source_location());
 
   const irep_idt statement=expr.get_statement();
 
-  assert(statement==ID_preincrement ||
-         statement==ID_predecrement);
+  DATA_INVARIANT(
+    statement == ID_preincrement || statement == ID_predecrement,
+    "expects preincrement or predecrement");
 
   exprt rhs;
   rhs.add_source_location()=expr.source_location();
@@ -198,9 +192,7 @@ void goto_convertt::remove_pre(
       constant_type=op_type;
     else
     {
-      error().source_location=expr.find_source_location();
-      error() << "no constant one of type " << op_type.pretty() << eom;
-      throw 0;
+      UNREACHABLE;
     }
 
     exprt constant=from_integer(1, constant_type);
@@ -235,18 +227,16 @@ void goto_convertt::remove_post(
 
   // we have ...(op++)...
 
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "postincrement/postdecrement must have one operand"
-            << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == 1,
+    "postincrement/postdecrement must have one operand",
+    expr.find_source_location());
 
   const irep_idt statement=expr.get_statement();
 
-  assert(statement==ID_postincrement ||
-         statement==ID_postdecrement);
+  DATA_INVARIANT(
+    statement == ID_postincrement || statement == ID_postdecrement,
+    "expects postincrement or postdecrement");
 
   exprt rhs;
   rhs.add_source_location()=expr.source_location();
@@ -291,9 +281,7 @@ void goto_convertt::remove_post(
       constant_type=op_type;
     else
     {
-      error().source_location=expr.find_source_location();
-      error() << "no constant one of type " << op_type.pretty() << eom;
-      throw 0;
+      UNREACHABLE;
     }
 
     exprt constant;
@@ -338,9 +326,13 @@ void goto_convertt::remove_function_call(
   const irep_idt &mode,
   bool result_is_used)
 {
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == 2,
+    "function_call expects two operands",
+    expr.find_source_location());
+
   if(!result_is_used)
   {
-    assert(expr.operands().size()==2);
     code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
     call.add_source_location()=expr.source_location();
     convert_function_call(call, dest, mode);
@@ -350,20 +342,10 @@ void goto_convertt::remove_function_call(
 
   // get name of function, if available
 
-  if(expr.id()!=ID_side_effect ||
-     expr.get(ID_statement)!=ID_function_call)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "expected function call" << eom;
-    throw 0;
-  }
-
-  if(expr.operands().empty())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "function_call expects at least one operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
+    "expects function call",
+    expr.find_source_location());
 
   std::string new_base_name = "return_value";
   irep_idt new_symbol_mode = mode;
@@ -445,7 +427,7 @@ void goto_convertt::remove_cpp_delete(
   side_effect_exprt &expr,
   goto_programt &dest)
 {
-  assert(expr.operands().size()==1);
+  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
 
   codet tmp(expr.get_statement());
   tmp.add_source_location()=expr.source_location();
@@ -498,13 +480,10 @@ void goto_convertt::remove_temporary_object(
   goto_programt &dest)
 {
   const irep_idt &mode = expr.get(ID_mode);
-  if(expr.operands().size()!=1 &&
-     !expr.operands().empty())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "temporary_object takes 0 or 1 operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() <= 1,
+    "temporary_object takes zero or one operands",
+    expr.find_source_location());
 
   symbolt &new_symbol = new_tmp_symbol(
     expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -518,7 +497,10 @@ void goto_convertt::remove_temporary_object(
 
   if(expr.find(ID_initializer).is_not_nil())
   {
-    assert(expr.operands().empty());
+    INVARIANT_WITH_DIAGNOSTICS(
+      expr.operands().empty(),
+      "temporary_object takes zero operands",
+      expr.find_source_location());
     exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
     replace_new_object(new_symbol.symbol_expr(), initializer);
 
@@ -539,19 +521,15 @@ void goto_convertt::remove_statement_expression(
   // The expression is copied into a temporary before the
   // scope is destroyed.
 
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "statement_expression takes 1 operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == 1,
+    "statement_expression takes one operand",
+    expr.find_source_location());
 
-  if(expr.op0().id()!=ID_code)
-  {
-    error().source_location=expr.op0().find_source_location();
-    error() << "statement_expression takes code as operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    expr.op0().id() == ID_code,
+    "statement_expression takes code as operand",
+    expr.find_source_location());
 
   codet &code=to_code(expr.op0());
 
@@ -562,20 +540,15 @@ void goto_convertt::remove_statement_expression(
     return;
   }
 
-  if(code.get_statement()!=ID_block)
-  {
-    error().source_location=code.find_source_location();
-    error() << "statement_expression takes block as operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.get_statement() == ID_block,
+    "statement_expression takes block as operand",
+    code.find_source_location());
 
-  if(code.operands().empty())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "statement_expression takes non-empty block as operand"
-            << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    !code.operands().empty(),
+    "statement_expression takes non-empty block as operand",
+    expr.find_source_location());
 
   // get last statement from block, following labels
   codet &last=to_code_block(code).find_last_statement();
@@ -604,10 +577,7 @@ void goto_convertt::remove_statement_expression(
   }
   else
   {
-    error() << "statement_expression expects expression as "
-            << "last statement, but got `"
-            << last.get(ID_statement) << "'" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 
   {
@@ -683,8 +653,6 @@ void goto_convertt::remove_side_effect(
   }
   else
   {
-    error().source_location=expr.find_source_location();
-    error() << "cannot remove side effect (" << statement << ")" << eom;
-    throw 0;
+    UNREACHABLE;
   }
 }
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index 253aaa51268..fdf4721e036 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #endif
 
-#include <cassert>
-
 #include <util/base_type.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -56,12 +54,9 @@ void goto_inlinet::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    if(identifier.empty())
-    {
-      error().source_location=source_location;
-      error() << "no identifier for function parameter" << eom;
-      throw 0;
-    }
+    DATA_INVARIANT(
+      !identifier.empty(),
+      source_location.as_string() + ": no identifier for function parameter");
 
     {
       const symbolt &symbol=ns.lookup(identifier);
@@ -123,16 +118,7 @@ void goto_inlinet::parameter_assignments(
         }
         else
         {
-          error().source_location=actual.find_source_location();
-
-          error() << "function call: argument `" << identifier
-                  << "' type mismatch: argument is `"
-                  // << from_type(ns, identifier, actual.type())
-                  << actual.type().pretty()
-                  << "', parameter is `"
-                  << from_type(ns, identifier, par_type)
-                  << "'" << eom;
-          throw 0;
+          UNREACHABLE;
         }
       }
 
@@ -176,12 +162,9 @@ void goto_inlinet::parameter_destruction(
   {
     const irep_idt &identifier=parameter.get_identifier();
 
-    if(identifier.empty())
-    {
-      error().source_location=source_location;
-      error() << "no identifier for function parameter" << eom;
-      throw 0;
-    }
+    INVARIANT(
+      !identifier.empty(),
+      source_location.as_string() + ": no identifier for function parameter");
 
     {
       const symbolt &symbol=ns.lookup(identifier);
@@ -626,9 +609,8 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
   }
 
   goto_functiont &cached=cache[identifier];
-  INVARIANT(
-    cached.body.empty(),
-    "body of new function in cache must be empty");
+  DATA_INVARIANT(
+    cached.body.empty(), "body of new function in cache must be empty");
 
   progress() << "Creating copy of " << identifier << eom;
   progress() << "Number of instructions: "
@@ -688,7 +670,7 @@ bool goto_inlinet::check_inline_map(
   goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);
 
-  PRECONDITION(f_it!=goto_functions.function_map.end());
+  PRECONDITION(f_it != goto_functions.function_map.end());
 
   inline_mapt::const_iterator im_it=inline_map.find(identifier);
 
@@ -762,7 +744,9 @@ void goto_inlinet::output_inline_map(
        !call_list.empty())
     {
       const goto_functiont &goto_function=f_it->second;
-      PRECONDITION(goto_function.body_available());
+      DATA_INVARIANT(
+        goto_function.body_available(),
+        "cannot inline function with empty body");
 
       const goto_programt &goto_program=goto_function.body;
 
@@ -825,10 +809,12 @@ void goto_inlinet::goto_inline_logt::add_segment(
 {
   PRECONDITION(!goto_program.empty());
   PRECONDITION(!function.empty());
-  PRECONDITION(end_location_number>=begin_location_number);
+  PRECONDITION(end_location_number >= begin_location_number);
 
   goto_programt::const_targett start=goto_program.instructions.begin();
-  PRECONDITION(log_map.find(start)==log_map.end());
+  INVARIANT(
+    log_map.find(start) == log_map.end(),
+    "inline function should be registered once in map of inline functions");
 
   goto_programt::const_targett end=goto_program.instructions.end();
   end--;
@@ -847,21 +833,27 @@ void goto_inlinet::goto_inline_logt::copy_from(
   const goto_programt &from,
   const goto_programt &to)
 {
-  PRECONDITION(from.instructions.size()==to.instructions.size());
+  PRECONDITION(from.instructions.size() == to.instructions.size());
 
   goto_programt::const_targett it1=from.instructions.begin();
   goto_programt::const_targett it2=to.instructions.begin();
 
   for(; it1!=from.instructions.end(); it1++, it2++)
   {
-    assert(it2!=to.instructions.end());
-    assert(it1->location_number==it2->location_number);
+    DATA_INVARIANT(
+      it2 != to.instructions.end(),
+      "'to' target function is not allowed to be empty");
+    DATA_INVARIANT(
+      it1->location_number == it2->location_number,
+      "both functions' instruction should point to the same source");
 
     log_mapt::const_iterator l_it=log_map.find(it1);
     if(l_it!=log_map.end()) // a segment starts here
     {
       // as 'to' is a fresh copy
-      assert(log_map.find(it2)==log_map.end());
+      DATA_INVARIANT(
+        log_map.find(it2) == log_map.end(),
+        "'to' target is not expected to be in the log_map");
 
       goto_inline_log_infot info=l_it->second;
       goto_programt::const_targett end=info.end;
@@ -896,7 +888,7 @@ jsont goto_inlinet::goto_inline_logt::output_inline_log_json() const
     const goto_inline_log_infot &info=it.second;
     goto_programt::const_targett end=info.end;
 
-    assert(start->location_number<=end->location_number);
+    PRECONDITION(start->location_number <= end->location_number);
 
     object["call"]=json_numbert(std::to_string(info.call_location_number));
     object["function"]=json_stringt(info.function.c_str());
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 69dfcbf952b..48a99d276bd 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -163,8 +163,10 @@ std::ostream &goto_programt::output_instruction(
       unsigned i=0;
       const irept::subt &exception_list=
         instruction.code.find(ID_exception_list).get_sub();
-      DATA_INVARIANT(instruction.targets.size()==exception_list.size(),
-                     "size of target list");
+      DATA_INVARIANT(
+        instruction.targets.size() == exception_list.size(),
+        "unexpected discrepancy between sizes of instruction"
+        "targets and exception list");
       for(instructiont::targetst::const_iterator
             gt_it=instruction.targets.begin();
           gt_it!=instruction.targets.end();
@@ -208,7 +210,7 @@ std::ostream &goto_programt::output_instruction(
     break;
 
   default:
-    throw "unknown statement";
+    UNREACHABLE;
   }
 
   return out;
@@ -221,10 +223,12 @@ void goto_programt::get_decl_identifiers(
   {
     if(it->is_decl())
     {
-      DATA_INVARIANT(it->code.get_statement()==ID_decl,
-                     "declaration statements");
-      DATA_INVARIANT(it->code.operands().size()==1,
-                     "operand of declaration statement");
+      DATA_INVARIANT(
+        it->code.get_statement() == ID_decl,
+        "expected statement to be declaration statement");
+      DATA_INVARIANT(
+        it->code.operands().size() == 1,
+        "declaration statement expects one operand");
       const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
       decl_identifiers.insert(symbol_expr.get_identifier());
     }
@@ -235,26 +239,24 @@ void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
 {
   if(src.id()==ID_dereference)
   {
-    assert(src.operands().size()==1);
-    dest.push_back(src.op0());
+    dest.push_back(to_dereference_expr(src).pointer());
   }
   else if(src.id()==ID_index)
   {
-    assert(src.operands().size()==2);
-    dest.push_back(src.op1());
-    parse_lhs_read(src.op0(), dest);
+    auto &index_expr = to_index_expr(src);
+    dest.push_back(index_expr.index());
+    parse_lhs_read(index_expr.array(), dest);
   }
   else if(src.id()==ID_member)
   {
-    assert(src.operands().size()==1);
-    parse_lhs_read(src.op0(), dest);
+    parse_lhs_read(to_member_expr(src).compound(), dest);
   }
   else if(src.id()==ID_if)
   {
-    assert(src.operands().size()==3);
-    dest.push_back(src.op0());
-    parse_lhs_read(src.op1(), dest);
-    parse_lhs_read(src.op2(), dest);
+    auto &if_expr = to_if_expr(src);
+    dest.push_back(if_expr.cond());
+    parse_lhs_read(if_expr.true_case(), dest);
+    parse_lhs_read(if_expr.false_case(), dest);
   }
 }
 
@@ -344,9 +346,9 @@ void objects_read(
   else if(src.id()==ID_dereference)
   {
     // this reads what is pointed to plus the pointer
-    assert(src.operands().size()==1);
-    dest.push_back(src);
-    objects_read(src.op0(), dest);
+    auto &deref = to_dereference_expr(src);
+    dest.push_back(deref);
+    objects_read(deref.pointer(), dest);
   }
   else
   {
@@ -374,9 +376,9 @@ void objects_written(
 {
   if(src.id()==ID_if)
   {
-    assert(src.operands().size()==3);
-    objects_written(src.op1(), dest);
-    objects_written(src.op2(), dest);
+    auto &if_expr = to_if_expr(src);
+    objects_written(if_expr.true_case(), dest);
+    objects_written(if_expr.false_case(), dest);
   }
   else
     dest.push_back(src);
@@ -483,7 +485,7 @@ std::string as_string(
     return "END THREAD";
 
   default:
-    throw "unknown statement";
+    UNREACHABLE;
   }
 }
 
@@ -555,7 +557,8 @@ void goto_programt::compute_target_numbers()
     if(i.is_target())
     {
       i.target_number=++cnt;
-      DATA_INVARIANT(i.target_number!=0, "target numbers");
+      DATA_INVARIANT(
+        i.target_number != 0, "GOTO instruction target cannot be zero");
     }
   }
 
@@ -568,10 +571,11 @@ void goto_programt::compute_target_numbers()
     {
       if(t!=instructions.end())
       {
-        DATA_INVARIANT(t->target_number!=0,
-                       "target numbers");
-        DATA_INVARIANT(t->target_number!=instructiont::nil_target,
-                       "target numbers");
+        DATA_INVARIANT(
+          t->target_number != 0, "instruction's number cannot be zero");
+        DATA_INVARIANT(
+          t->target_number != instructiont::nil_target,
+          "GOTO instruction target cannot be nil_target");
       }
     }
   }
@@ -610,8 +614,7 @@ void goto_programt::copy_from(const goto_programt &src)
       targets_mappingt::iterator
         m_target_it=targets_mapping.find(t);
 
-      if(m_target_it==targets_mapping.end())
-        throw "copy_from: target not found";
+      CHECK_RETURN(m_target_it != targets_mapping.end());
 
       t=m_target_it->second;
     }
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index b00579c569b..64d8001cf8d 100644
--- a/src/goto-programs/goto_trace.h
+++ b/src/goto-programs/goto_trace.h
@@ -191,7 +191,7 @@ class goto_tracet
   // delete all steps after (not including) s
   void trim_after(stepst::iterator s)
   {
-    assert(s!=steps.end());
+    PRECONDITION(s != steps.end());
     steps.erase(++s, steps.end());
   }
 };
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 2c382d76f98..1fcb1e603f5 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -108,7 +108,8 @@ std::string graphml_witnesst::convert_assign_rec(
          has_prefix(id2string(comp.get_name()), "$pad"))
         continue;
 
-      assert(it!=assign.rhs().operands().end());
+      INVARIANT(
+        it != assign.rhs().operands().end(), "expression must have operands");
 
       member_exprt member(
         assign.lhs(),