diff --git a/regression/ansi-c/goto_convert_break/main.c b/regression/ansi-c/goto_convert_break/main.c
new file mode 100644
index 00000000000..42c65e6175e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_break/main.c
@@ -0,0 +1,5 @@
+int main()
+{
+  break;
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_break/test.desc b/regression/ansi-c/goto_convert_break/test.desc
new file mode 100644
index 00000000000..20185aa29ee
--- /dev/null
+++ b/regression/ansi-c/goto_convert_break/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_continue/main.c b/regression/ansi-c/goto_convert_continue/main.c
new file mode 100644
index 00000000000..a226cb128b6
--- /dev/null
+++ b/regression/ansi-c/goto_convert_continue/main.c
@@ -0,0 +1,5 @@
+int main()
+{
+  continue;
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_continue/test.desc b/regression/ansi-c/goto_convert_continue/test.desc
new file mode 100644
index 00000000000..988f44bb507
--- /dev/null
+++ b/regression/ansi-c/goto_convert_continue/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
diff --git a/regression/ansi-c/goto_convert_invalid_goto_label/main.c b/regression/ansi-c/goto_convert_invalid_goto_label/main.c
new file mode 100644
index 00000000000..002a4382e7c
--- /dev/null
+++ b/regression/ansi-c/goto_convert_invalid_goto_label/main.c
@@ -0,0 +1,8 @@
+int main()
+{
+  goto x;
+
+  // x:
+
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_invalid_goto_label/test.desc b/regression/ansi-c/goto_convert_invalid_goto_label/test.desc
new file mode 100644
index 00000000000..92d37c3047e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_invalid_goto_label/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_switch_range_bounds/main.c b/regression/ansi-c/goto_convert_switch_range_bounds/main.c
new file mode 100644
index 00000000000..2335d8d8210
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_bounds/main.c
@@ -0,0 +1,13 @@
+int main()
+{
+  int x;
+  int n = 5;
+  switch(x)
+  {
+  case 0 ... n:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_bounds/test.desc b/regression/ansi-c/goto_convert_switch_range_bounds/test.desc
new file mode 100644
index 00000000000..92d37c3047e
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_bounds/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/main.c b/regression/ansi-c/goto_convert_switch_range_case_valid/main.c
new file mode 100644
index 00000000000..d46f19d2100
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_case_valid/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#define false 0
+
+int main(void)
+{
+  int x = 5;
+  switch (x)
+  {
+    case 0 ... 10:
+      break;
+    default:
+      assert(false);
+      break;
+  }
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
new file mode 100644
index 00000000000..936c704a3e2
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
diff --git a/regression/ansi-c/goto_convert_switch_range_empty/main.c b/regression/ansi-c/goto_convert_switch_range_empty/main.c
new file mode 100644
index 00000000000..4e6ed4c28cd
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_empty/main.c
@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 10 ... 0:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_empty/test.desc b/regression/ansi-c/goto_convert_switch_range_empty/test.desc
new file mode 100644
index 00000000000..2718746733c
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_empty/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
diff --git a/regression/ansi-c/goto_convert_switch_range_operands_count/main.c b/regression/ansi-c/goto_convert_switch_range_operands_count/main.c
new file mode 100644
index 00000000000..7a553052182
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_operands_count/main.c
@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 0 ... 10 20:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}
diff --git a/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc b/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc
new file mode 100644
index 00000000000..035bb37fe27
--- /dev/null
+++ b/regression/ansi-c/goto_convert_switch_range_operands_count/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^PARSING ERROR$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 09cc717343d..ead2b6d80cd 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
@@ -611,6 +612,12 @@ int cbmc_parse_optionst::get_goto_program(
     log.status() << config.object_bits_info() << log.eom;
   }
 
+  catch(incorrect_goto_program_exceptiont &e)
+  {
+    log.error() << e.what() << log.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
   catch(const char *e)
   {
     log.error() << e << log.eom;
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index fc45aa43707..12837784077 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -11,10 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_convert.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
+#include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/prefix.h>
@@ -116,11 +115,11 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       labelst::const_iterator l_it=
         targets.labels.find(goto_label);
 
-      if(l_it==targets.labels.end())
+      if(l_it == targets.labels.end())
       {
-        error().source_location=i.code.find_source_location();
-        error() << "goto label `" << goto_label << "' not found" << eom;
-        throw 0;
+        throw incorrect_goto_program_exceptiont(
+          "goto label \'" + id2string(goto_label) + "\' not found",
+          i.code.find_source_location());
       }
 
       i.targets.push_back(l_it->second.first);
@@ -131,11 +130,11 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
 
       labelst::const_iterator l_it=targets.labels.find(goto_label);
 
-      if(l_it==targets.labels.end())
+      if(l_it == targets.labels.end())
       {
-        error().source_location=i.code.find_source_location();
-        error() << "goto label `" << goto_label << "' not found" << eom;
-        throw 0;
+        throw incorrect_goto_program_exceptiont(
+          "goto label \'" + id2string(goto_label) + "\' not found",
+          i.code.find_source_location());
       }
 
       i.complete_goto(l_it->second.first);
@@ -184,9 +183,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
     }
     else
     {
-      error().source_location=i.code.find_source_location();
-      error() << "finish_gotos: unexpected goto" << eom;
-      throw 0;
+      UNREACHABLE;
     }
   }
 
@@ -198,12 +195,8 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
   for(auto &g_it : targets.computed_gotos)
   {
     goto_programt::instructiont &i=*g_it;
-    exprt destination=i.code.op0();
-
-    assert(destination.id()==ID_dereference);
-    assert(destination.operands().size()==1);
-
-    exprt pointer=destination.op0();
+    dereference_exprt destination = to_dereference_expr(i.code.op0());
+    const exprt pointer = destination.pointer();
 
     // remember the expression for later checks
     i.type=OTHER;
@@ -310,13 +303,6 @@ void goto_convertt::convert_label(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "label statement expected to have one operand" << eom;
-    throw 0;
-  }
-
   // grab the label
   const irep_idt &label=code.get_label();
 
@@ -329,8 +315,8 @@ void goto_convertt::convert_label(
   {
     // the body of the thread is expected to be
     // in the operand.
-    INVARIANT(code.op0().is_not_nil(),
-      "op0 in magic thread creation label is null");
+    DATA_INVARIANT(
+      code.op0().is_not_nil(), "op0 in magic thread creation label is null");
 
     // replace the magic thread creation label with a
     // thread block (START_THREAD...END_THREAD).
@@ -395,25 +381,20 @@ void goto_convertt::convert_gcc_switch_case_range(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location=code.find_source_location();
-    error() << "GCC's switch-case-range statement expected to have "
-            << "three operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 3,
+    "GCC's switch-case-range statement expected to have three operands",
+    code.find_source_location());
 
   const auto lb = numeric_cast<mp_integer>(code.op0());
   const auto ub = numeric_cast<mp_integer>(code.op1());
 
-  if(!lb.has_value() || !ub.has_value())
-  {
-    error().source_location = code.find_source_location();
-    error() << "GCC's switch-case-range statement requires constant bounds"
-            << eom;
-    throw 0;
-  }
-  else if(*lb > *ub)
+  INVARIANT_WITH_DIAGNOSTICS(
+    lb.has_value() && ub.has_value(),
+    "GCC's switch-case-range statement requires constant bounds",
+    code.find_source_location());
+
+  if(*lb > *ub)
   {
     warning().source_location = code.find_source_location();
     warning() << "GCC's switch-case-range statement with empty case range"
@@ -523,24 +504,14 @@ void goto_convertt::convert(
     convert_asm(to_code_asm(code), dest);
   else if(statement==ID_static_assert)
   {
-    assert(code.operands().size()==2);
+    PRECONDITION(code.operands().size() == 2);
     exprt assertion=code.op0();
     assertion.make_typecast(bool_typet());
     simplify(assertion, ns);
-    if(assertion.is_false())
-    {
-      error().source_location=code.op0().find_source_location();
-      error() << "static assertion "
-              << get_string_constant(code.op1()) << eom;
-      throw 0;
-    }
-    else if(assertion.is_true())
-    {
-    }
-    else
-    {
-      // we may wish to complain
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      !assertion.is_false(),
+      "static assertion " + id2string(get_string_constant(code.op1())),
+      code.op0().find_source_location());
   }
   else if(statement==ID_dead)
     copy(code, DEAD, dest);
@@ -602,14 +573,7 @@ void goto_convertt::convert_expression(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "expression statement takes one operand" << eom;
-    throw 0;
-  }
-
-  exprt expr=code.op0();
+  exprt expr = code.expression();
 
   if(expr.id()==ID_if)
   {
@@ -646,16 +610,7 @@ void goto_convertt::convert_decl(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  const exprt &op = code.symbol();
-
-  if(op.id() != ID_symbol)
-  {
-    error().source_location = op.find_source_location();
-    error() << "decl statement expects symbol as operand" << eom;
-    throw 0;
-  }
-
-  const irep_idt &identifier = to_symbol_expr(op).get_identifier();
+  const irep_idt &identifier = to_symbol_expr(code.symbol()).get_identifier();
 
   const symbolt &symbol = ns.lookup(identifier);
 
@@ -729,12 +684,10 @@ void goto_convertt::convert_assign(
   if(rhs.id()==ID_side_effect &&
      rhs.get(ID_statement)==ID_function_call)
   {
-    if(rhs.operands().size()!=2)
-    {
-      error().source_location=rhs.find_source_location();
-      error() << "function_call sideeffect takes two operands" << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      rhs.operands().size() == 2,
+      "function_call sideeffect takes two operands",
+      rhs.find_source_location());
 
     Forall_operands(it, rhs)
       clean_expr(*it, dest, mode);
@@ -802,11 +755,8 @@ void goto_convertt::convert_assign(
 
     if(lhs.id()==ID_typecast)
     {
-      assert(lhs.operands().size()==1);
-
       // add a typecast to the rhs
-      exprt new_rhs=rhs;
-      rhs.make_typecast(lhs.op0().type());
+      rhs.make_typecast(to_typecast_expr(lhs).op().type());
 
       // remove typecast from lhs
       exprt tmp=lhs.op0();
@@ -826,12 +776,10 @@ void goto_convertt::convert_init(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=2)
-  {
-    error().source_location=code.find_source_location();
-    error() <<"init statement takes two operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 2,
+    "init statement takes two operands",
+    code.find_source_location());
 
   // make it an assignment
   codet assignment=code;
@@ -844,12 +792,10 @@ void goto_convertt::convert_cpp_delete(
   const codet &code,
   goto_programt &dest)
 {
-  if(code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "cpp_delete statement takes one operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 1,
+    "cpp_delete statement takes one operand",
+    code.find_source_location());
 
   exprt tmp_op=code.op0();
 
@@ -890,7 +836,9 @@ void goto_convertt::convert_cpp_delete(
   // now do "free"
   exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
 
-  assert(to_code_type(delete_symbol.type()).parameters().size()==1);
+  DATA_INVARIANT(
+    to_code_type(delete_symbol.type()).parameters().size() == 1,
+    "delete statement takes 1 parameter");
 
   typet arg_type=
     to_code_type(delete_symbol.type()).parameters().front().type();
@@ -955,14 +903,13 @@ void goto_convertt::convert_loop_invariant(
 
   goto_programt no_sideeffects;
   clean_expr(invariant, no_sideeffects, mode);
-  if(!no_sideeffects.instructions.empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "loop invariant is not side-effect free" << eom;
-    throw 0;
-  }
 
-  assert(loop->is_goto());
+  INVARIANT_WITH_DIAGNOSTICS(
+    no_sideeffects.instructions.empty(),
+    "loop invariant is not side-effect free",
+    code.find_source_location());
+
+  PRECONDITION(loop->is_goto());
   loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
 }
 
@@ -1132,6 +1079,11 @@ void goto_convertt::convert_dowhile(
   goto_programt &dest,
   const irep_idt &mode)
 {
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().size() == 2,
+    "dowhile takes two operands",
+    code.find_source_location());
+
   // save source location
   source_locationt condition_location=code.cond().find_source_location();
 
@@ -1197,27 +1149,28 @@ exprt goto_convertt::case_guard(
   const exprt &value,
   const exprt::operandst &case_op)
 {
-  exprt dest=exprt(ID_or, bool_typet());
-  dest.reserve_operands(case_op.size());
+  PRECONDITION(!case_op.empty());
 
-  forall_expr(it, case_op)
+  if(case_op.size() == 1)
+    return equal_exprt(value, case_op.at(0));
+  else
   {
-    equal_exprt eq_expr;
-    eq_expr.lhs()=value;
-    eq_expr.rhs()=*it;
-    dest.move_to_operands(eq_expr);
-  }
+    exprt dest = exprt(ID_or, bool_typet());
+    dest.reserve_operands(case_op.size());
 
-  assert(!dest.operands().empty());
+    forall_expr(it, case_op)
+    {
+      equal_exprt eq_expr;
+      eq_expr.lhs() = value;
+      eq_expr.rhs() = *it;
+      dest.move_to_operands(eq_expr);
+    }
+    INVARIANT(
+      case_op.size() == dest.operands().size(),
+      "case guard conversion should preserve the number of cases");
 
-  if(dest.operands().size()==1)
-  {
-    exprt tmp;
-    tmp.swap(dest.op0());
-    dest.swap(tmp);
+    return dest;
   }
-
-  return dest;
 }
 
 void goto_convertt::convert_switch(
@@ -1331,12 +1284,8 @@ void goto_convertt::convert_break(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(!targets.break_set)
-  {
-    error().source_location=code.find_source_location();
-    error() << "break without target" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    targets.break_set, "break without target", code.find_source_location());
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1355,18 +1304,14 @@ void goto_convertt::convert_return(
 {
   if(!targets.return_set)
   {
-    error().source_location=code.find_source_location();
-    error() << "return without target" << eom;
-    throw 0;
+    throw incorrect_goto_program_exceptiont(
+      "return without target", code.find_source_location());
   }
 
-  if(!code.operands().empty() &&
-     code.operands().size()!=1)
-  {
-    error().source_location=code.find_source_location();
-    error() << "return takes none or one operand" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().empty() || code.operands().size() == 1,
+    "return takes none or one operand",
+    code.find_source_location());
 
   code_returnt new_code(code);
 
@@ -1386,12 +1331,10 @@ void goto_convertt::convert_return(
 
   if(targets.has_return_value)
   {
-    if(!new_code.has_return_value())
-    {
-      error().source_location=new_code.find_source_location();
-      error() << "function must return value" << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      new_code.has_return_value(),
+      "function must return value",
+      new_code.find_source_location());
 
     // Now add a return node to set the return value.
     goto_programt::targett t=dest.add_instruction();
@@ -1401,13 +1344,11 @@ void goto_convertt::convert_return(
   }
   else
   {
-    if(new_code.has_return_value() &&
-       new_code.return_value().type().id()!=ID_empty)
-    {
-      error().source_location=new_code.find_source_location();
-      error() << "function must not return value" << eom;
-      throw 0;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      !new_code.has_return_value() ||
+        new_code.return_value().type().id() == ID_empty,
+      "function must not return value",
+      code.find_source_location());
   }
 
   // Need to process _entire_ destructor stack.
@@ -1424,12 +1365,10 @@ void goto_convertt::convert_continue(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(!targets.continue_set)
-  {
-    error().source_location=code.find_source_location();
-    error() << "continue without target" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    targets.continue_set,
+    "continue without target",
+    code.find_source_location());
 
   // need to process destructor stack
   unwind_destructor_stack(
@@ -1483,12 +1422,10 @@ void goto_convertt::convert_end_thread(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "end_thread expects no operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().empty(),
+    "end_thread expects no operands",
+    code.find_source_location());
 
   copy(code, END_THREAD, dest);
 }
@@ -1497,12 +1434,10 @@ void goto_convertt::convert_atomic_begin(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "atomic_begin expects no operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().empty(),
+    "atomic_begin expects no operands",
+    code.find_source_location());
 
   copy(code, ATOMIC_BEGIN, dest);
 }
@@ -1511,12 +1446,10 @@ void goto_convertt::convert_atomic_end(
   const codet &code,
   goto_programt &dest)
 {
-  if(!code.operands().empty())
-  {
-    error().source_location=code.find_source_location();
-    error() << "atomic_end expects no operands" << eom;
-    throw 0;
-  }
+  INVARIANT_WITH_DIAGNOSTICS(
+    code.operands().empty(),
+    ": atomic_end expects no operands",
+    code.find_source_location());
 
   copy(code, ATOMIC_END, dest);
 }
@@ -1526,14 +1459,7 @@ void goto_convertt::convert_ifthenelse(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  if(code.operands().size()!=3)
-  {
-    error().source_location=code.find_source_location();
-    error() << "ifthenelse takes three operands" << eom;
-    throw 0;
-  }
-
-  assert(code.then_case().is_not_nil());
+  DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
 
   bool has_else=
     !code.else_case().is_nil();
@@ -1733,7 +1659,7 @@ void goto_convertt::generate_ifthenelse(
 
   // x: goto z;
   x->make_goto(z);
-  assert(!tmp_w.instructions.empty());
+  CHECK_RETURN(!tmp_w.instructions.empty());
   x->source_location=tmp_w.instructions.back().source_location;
 
   dest.destructive_append(tmp_v);
@@ -1811,10 +1737,14 @@ void goto_convertt::generate_conditional_branch(
 {
   if(guard.id()==ID_not)
   {
-    assert(guard.operands().size()==1);
     // simply swap targets
     generate_conditional_branch(
-      guard.op0(), target_false, target_true, source_location, dest, mode);
+      to_not_expr(guard).op(),
+      target_false,
+      target_true,
+      source_location,
+      dest,
+      mode);
     return;
   }
 
@@ -1924,14 +1854,12 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr)
 {
   irep_idt result;
 
-  if(get_string_constant(expr, result))
-  {
-    error().source_location=expr.find_source_location();
-    error() << "expected string constant, but got: "
-      << expr.pretty() << eom;
-
-    throw 0;
-  }
+  const bool res = get_string_constant(expr, result);
+  INVARIANT_WITH_DIAGNOSTICS(
+    !res,
+    "expected string constant",
+    expr.find_source_location(),
+    expr.pretty());
 
   return result;
 }
@@ -2013,33 +1941,8 @@ void goto_convert(
   message_handlert &message_handler,
   const irep_idt &mode)
 {
-  const std::size_t errors_before=
-    message_handler.get_message_count(messaget::M_ERROR);
-
   goto_convertt goto_convert(symbol_table, message_handler);
-
-  try
-  {
-    goto_convert.goto_convert(code, dest, mode);
-  }
-
-  catch(int)
-  {
-    goto_convert.error();
-  }
-
-  catch(const char *e)
-  {
-    goto_convert.error() << e << messaget::eom;
-  }
-
-  catch(const std::string &e)
-  {
-    goto_convert.error() << e << messaget::eom;
-  }
-
-  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
-    throw 0;
+  goto_convert.goto_convert(code, dest, mode);
 }
 
 void goto_convert(
@@ -2051,8 +1954,8 @@ void goto_convert(
   const symbol_tablet::symbolst::const_iterator s_it=
     symbol_table.symbols.find("main");
 
-  if(s_it==symbol_table.symbols.end())
-    throw "failed to find main symbol";
+  DATA_INVARIANT(
+    s_it != symbol_table.symbols.end(), "failed to find main symbol");
 
   const symbolt &symbol=s_it->second;
 
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 5e282b95c49..2367849b6ca 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -315,6 +315,9 @@ inline const code_declt &to_code_decl(const codet &code)
   // will be size()==1 in the future
   DATA_INVARIANT(
     code.operands().size() >= 1, "decls must have one or more operands");
+  DATA_INVARIANT(
+    code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\"");
+
   return static_cast<const code_declt &>(code);
 }