diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 40523caaba3..5435ef4a5db 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -15,9 +15,10 @@ Author: Daniel Kroening
 
 #include <cassert>
 
-#include <util/threeval.h>
-#include <util/simplify_expr.h>
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/simplify_expr.h>
+#include <util/threeval.h>
 
 #include <solvers/prop/prop_conv.h>
 #include <solvers/prop/prop.h>
@@ -92,8 +93,11 @@ exprt build_full_lhs_rec(
           id==ID_byte_extract_big_endian)
   {
     exprt tmp=src_original;
-    assert(tmp.operands().size()==2);
-    tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
+    tmp.op0() = build_full_lhs_rec(
+      prop_conv,
+      ns,
+      to_byte_extract_expr(tmp).op(),
+      to_byte_extract_expr(src_ssa).op());
 
     // re-write into big case-split
   }
@@ -229,7 +233,7 @@ void build_goto_trace(
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;
 
-      assert(current_time>=0);
+      INVARIANT(current_time >= 0, "time keeping inconsistency");
       // move any steps gathered in an atomic section
 
       if(time_before<0)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 9d87de62880..40f5054155e 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -14,10 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cstdlib>
 #include <iostream>
 
-#include <util/invariant.h>
 #include <util/base_exceptions.h>
-#include <util/std_expr.h>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
 #include <util/prefix.h>
+#include <util/std_expr.h>
 
 #include <analyses/dirty.h>
 
@@ -51,8 +52,7 @@ void goto_symex_statet::level0t::operator()(
 
   const symbolt *s;
   const bool found_l0 = !ns.lookup(obj_identifier, s);
-  DATA_INVARIANT(
-    found_l0, "level0: failed to find " + id2string(obj_identifier));
+  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
 
   // don't rename shared variables or functions
   if(s->type.id()==ID_code ||
@@ -187,10 +187,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   }
   else if(expr.id()==ID_member)
   {
-    if(expr.operands().size()!=1)
-      throw "member expects one operand";
-
-    return constant_propagation_reference(expr.op0());
+    return constant_propagation_reference(to_member_expr(expr).compound());
   }
   else if(expr.id()==ID_string_constant)
     return true;
@@ -345,7 +342,8 @@ void goto_symex_statet::assignment(
 
   // see #305 on GitHub for a simple example and possible discussion
   if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
-    throw "pointer handling for concurrency is unsound";
+    throw unsupported_operation_exceptiont(
+      "pointer handling for concurrency is unsound");
 
   // for value propagation -- the RHS is L2
 
@@ -495,13 +493,9 @@ void goto_symex_statet::rename(
   }
   else if(expr.id()==ID_address_of)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, "address_of should have a single operand");
-    rename_address(expr.op0(), ns, level);
-    DATA_INVARIANT(
-      expr.type().id() == ID_pointer,
-      "type of address_of should be ID_pointer");
-    expr.type().subtype()=expr.op0().type();
+    auto &address_of_expr = to_address_of_expr(expr);
+    rename_address(address_of_expr.object(), ns, level);
+    expr.type().subtype() = address_of_expr.object().type();
   }
   else
   {
diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp
index d8487e629fd..729d47eabb0 100644
--- a/src/goto-symex/memory_model_pso.cpp
+++ b/src/goto-symex/memory_model_pso.cpp
@@ -30,8 +30,8 @@ bool memory_model_psot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
index a09f9652f30..9575a09c920 100644
--- a/src/goto-symex/memory_model_sc.cpp
+++ b/src/goto-symex/memory_model_sc.cpp
@@ -36,8 +36,8 @@ bool memory_model_sct::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   return false;
 }
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
index 32551d53bc1..9062ab2b4df 100644
--- a/src/goto-symex/memory_model_tso.cpp
+++ b/src/goto-symex/memory_model_tso.cpp
@@ -39,8 +39,8 @@ bool memory_model_tsot::program_order_is_relaxed(
   partial_order_concurrencyt::event_it e1,
   partial_order_concurrencyt::event_it e2) const
 {
-  assert(e1->is_shared_read() || e1->is_shared_write());
-  assert(e2->is_shared_read() || e2->is_shared_write());
+  PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
+  PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
 
   // no po relaxation within atomic sections
   if(e1->atomic_section_id!=0 &&
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index fb9529a83fb..5da484df641 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -142,8 +142,8 @@ symbol_exprt partial_order_concurrencyt::clock(
   event_it event,
   axiomt axiom)
 {
+  PRECONDITION(!numbering.empty());
   irep_idt identifier;
-  assert(!numbering.empty());
 
   if(event->is_shared_write())
     identifier=rw_clock_id(event, axiom);
@@ -163,7 +163,7 @@ symbol_exprt partial_order_concurrencyt::clock(
 
 void partial_order_concurrencyt::build_clock_type()
 {
-  assert(!numbering.empty());
+  PRECONDITION(!numbering.empty());
 
   std::size_t width = address_bits(numbering.size());
   clock_type = unsignedbv_typet(width);
@@ -198,7 +198,7 @@ exprt partial_order_concurrencyt::before(
         binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
   }
 
-  assert(!ops.empty());
+  POSTCONDITION(!ops.empty());
 
   return conjunction(ops);
 }
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 57624a25d56..61d0a7b4655 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -76,21 +76,16 @@ bool postconditiont::is_used_address_of(
   }
   else if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
-
-    return
-      is_used_address_of(expr.op0(), identifier) ||
-      is_used(expr.op1(), identifier);
+    return is_used_address_of(to_index_expr(expr).array(), identifier) ||
+           is_used(to_index_expr(expr).index(), identifier);
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    return is_used_address_of(expr.op0(), identifier);
+    return is_used_address_of(to_member_expr(expr).compound(), identifier);
   }
   else if(expr.id()==ID_dereference)
   {
-    assert(expr.operands().size()==1);
-    return is_used(expr.op0(), identifier);
+    return is_used(to_dereference_expr(expr).pointer(), identifier);
   }
 
   return false;
@@ -154,9 +149,7 @@ bool postconditiont::is_used(
 {
   if(expr.id()==ID_address_of)
   {
-    // only do index!
-    assert(expr.operands().size()==1);
-    return is_used_address_of(expr.op0(), identifier);
+    return is_used_address_of(to_address_of_expr(expr).object(), identifier);
   }
   else if(expr.id()==ID_symbol &&
           expr.get_bool(ID_C_SSA_symbol))
@@ -169,12 +162,9 @@ bool postconditiont::is_used(
   }
   else if(expr.id()==ID_dereference)
   {
-    assert(expr.operands().size()==1);
-
     // aliasing may happen here
-
     value_setst::valuest expr_set;
-    value_set.get_value_set(expr.op0(), expr_set, ns);
+    value_set.get_value_set(to_dereference_expr(expr).pointer(), expr_set, ns);
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 69d26cd19f6..8b604408108 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -78,19 +78,17 @@ void preconditiont::compute_address_of(exprt &dest)
   }
   else if(dest.id()==ID_index)
   {
-    assert(dest.operands().size()==2);
-    compute_address_of(dest.op0());
-    compute(dest.op1());
+    auto &index_expr = to_index_expr(dest);
+    compute_address_of(index_expr.array());
+    compute(index_expr.index());
   }
   else if(dest.id()==ID_member)
   {
-    assert(dest.operands().size()==1);
-    compute_address_of(dest.op0());
+    compute_address_of(to_member_expr(dest).compound());
   }
   else if(dest.id()==ID_dereference)
   {
-    assert(dest.operands().size()==1);
-    compute(dest.op0());
+    compute(to_dereference_expr(dest).pointer());
   }
 }
 
@@ -104,19 +102,18 @@ void preconditiont::compute_rec(exprt &dest)
   if(dest.id()==ID_address_of)
   {
     // only do index!
-    assert(dest.operands().size()==1);
-    compute_address_of(dest.op0());
+    compute_address_of(to_address_of_expr(dest).object());
   }
   else if(dest.id()==ID_dereference)
   {
-    assert(dest.operands().size()==1);
+    auto &deref_expr = to_dereference_expr(dest);
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 
     // aliasing may happen here
 
     value_setst::valuest expr_set;
-    value_sets.get_values(target, dest.op0(), expr_set);
+    value_sets.get_values(target, deref_expr.pointer(), expr_set);
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator
@@ -129,15 +126,15 @@ void preconditiont::compute_rec(exprt &dest)
     {
       // may alias!
       exprt tmp;
-      tmp.swap(dest.op0());
+      tmp.swap(deref_expr.pointer());
       dereference(target, tmp, ns, value_sets);
-      dest.swap(tmp);
-      compute_rec(dest);
+      deref_expr.swap(tmp);
+      compute_rec(deref_expr);
     }
     else
     {
       // nah, ok
-      compute_rec(dest.op0());
+      compute_rec(deref_expr.pointer());
     }
   }
   else if(dest==SSA_step.ssa_lhs.get_original_expr())
diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
index 6116759b66c..cc89ed39624 100644
--- a/src/goto-symex/show_vcc.cpp
+++ b/src/goto-symex/show_vcc.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
 
+#include <util/exception_utils.h>
 #include <util/json.h>
 #include <util/json_expr.h>
 #include <util/ui_message.h>
@@ -165,7 +166,8 @@ void show_vcc(
   {
     of.open(filename);
     if(!of)
-      throw "failed to open file " + filename;
+      throw invalid_user_input_exceptiont(
+        "invalid file to read trace from: " + filename, "--outfile");
   }
 
   std::ostream &out = have_file ? of : std::cout;
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 8e9af5e820e..fbf6d1ff017 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -112,7 +112,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
 void symex_slicet::slice_assignment(
   symex_target_equationt::SSA_stept &SSA_step)
 {
-  assert(SSA_step.ssa_lhs.id()==ID_symbol);
+  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
   const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
 
   if(depends.find(id)==depends.end())
@@ -127,8 +127,7 @@ void symex_slicet::slice_assignment(
 void symex_slicet::slice_decl(
   symex_target_equationt::SSA_stept &SSA_step)
 {
-  assert(SSA_step.ssa_lhs.id()==ID_symbol);
-  const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
+  const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();
 
   if(depends.find(id)==depends.end())
   {
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index d02b54ed3e7..b0d6a4a8647 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -16,12 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <iostream>
 
-#include <util/string2int.h>
-#include <util/simplify_expr.h>
 #include <util/arith_tools.h>
-#include <util/std_expr.h>
-#include <util/guard.h>
+#include <util/exception_utils.h>
 #include <util/format_expr.h>
+#include <util/guard.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/string2int.h>
 
 void symex_slice_by_tracet::slice_by_trace(
   std::string trace_files,
@@ -79,6 +80,11 @@ void symex_slice_by_tracet::slice_by_trace(
   {
     exprt g_copy(*i);
 
+    DATA_INVARIANT(
+      g_copy.id() == ID_symbol || g_copy.id() == ID_not ||
+        g_copy.id() == ID_and || g_copy.id() == ID_constant,
+      "guards should only be and, symbol, constant, or `not'");
+
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {
       g_copy.make_not();
@@ -92,10 +98,6 @@ void symex_slice_by_tracet::slice_by_trace(
       simplify(copy_last, ns);
       implications.insert(copy_last);
     }
-    else if(!(g_copy.id()==ID_constant))
-    {
-      throw "guards should only be and, symbol, constant, or `not'";
-    }
   }
 
   slice_SSA_steps(equation, implications); // Slice based on implications
@@ -122,7 +124,8 @@ void symex_slice_by_tracet::read_trace(std::string filename)
   std::cout << "Reading trace from file " << filename << '\n';
   std::ifstream file(filename);
   if(file.fail())
-    throw "failed to read from trace file";
+    throw invalid_user_input_exceptiont(
+      "invalid file to read trace from: " + filename, "");
 
   // In case not the first trace read
   alphabet.clear();
@@ -219,9 +222,10 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
     const std::string::size_type vnext=read_line.find(",", vidx);
     std::string event=read_line.substr(vidx, vnext - vidx);
     eis.insert(event);
-    if((!alphabet.empty()) &&
-       ((alphabet.count(event)!=0)!=alphabet_parity))
-      throw "trace uses symbol not in alphabet: "+event;
+    PRECONDITION(!alphabet.empty());
+    INVARIANT(
+      (alphabet.count(event) != 0) == alphabet_parity,
+      "trace uses symbol not in alphabet: " + event);
     if(vnext==std::string::npos)
       break;
     vidx=vnext;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 03ab8f10b0a..3000679c73f 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
+#include <util/exception_utils.h>
 #include <util/pointer_offset_size.h>
 
 #include "goto_symex_state.h"
@@ -37,15 +38,19 @@ void goto_symext::symex_assign(
 
     if(statement==ID_function_call)
     {
-      assert(!side_effect_expr.operands().empty());
+      DATA_INVARIANT(
+        !side_effect_expr.operands().empty(),
+        "function call stamement expects non-empty list of side effects");
 
-      if(side_effect_expr.op0().id()!=ID_symbol)
-        throw "symex_assign: expected symbol as function";
+      DATA_INVARIANT(
+        side_effect_expr.op0().id() == ID_symbol,
+        "expected symbol as function");
 
       const irep_idt &identifier=
         to_symbol_expr(side_effect_expr.op0()).get_identifier();
 
-      throw "symex_assign: unexpected function call: "+id2string(identifier);
+      throw unsupported_operation_exceptiont(
+        "symex_assign: unexpected function call: " + id2string(identifier));
     }
     else if(
       statement == ID_cpp_new || statement == ID_cpp_new_array ||
@@ -55,14 +60,13 @@ void goto_symext::symex_assign(
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
     {
-      if(lhs.is_not_nil())
-        throw "printf: unexpected assignment";
+      PRECONDITION(lhs.is_nil());
       symex_printf(state, side_effect_expr);
     }
     else if(statement==ID_gcc_builtin_va_arg_next)
       symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
     else
-      throw "symex_assign: unexpected side effect: "+id2string(statement);
+      UNREACHABLE;
   }
   else
   {
@@ -91,12 +95,12 @@ exprt goto_symext::add_to_lhs(
   const exprt &lhs,
   const exprt &what)
 {
-  assert(lhs.id()!=ID_symbol);
+  PRECONDITION(lhs.id() != ID_symbol);
   exprt tmp_what=what;
 
   if(tmp_what.id()!=ID_symbol)
   {
-    assert(tmp_what.operands().size()>=1);
+    PRECONDITION(tmp_what.operands().size() >= 1);
     tmp_what.op0().make_nil();
   }
 
@@ -106,12 +110,16 @@ exprt goto_symext::add_to_lhs(
 
   while(p->is_not_nil())
   {
-    assert(p->id()!=ID_symbol);
-    assert(p->operands().size()>=1);
+    INVARIANT(
+      p->id() != ID_symbol,
+      "expected pointed-to expression not to be a symbol");
+    INVARIANT(
+      p->operands().size() >= 1,
+      "expected pointed-to expression to have at least one operand");
     p=&p->op0();
   }
 
-  assert(p->is_nil());
+  INVARIANT(p->is_nil(), "expected pointed-to expression to be nil");
 
   *p=tmp_what;
   return new_lhs;
@@ -141,12 +149,13 @@ void goto_symext::symex_assign_rec(
     else if(type.id()==ID_union)
     {
       // should have been replaced by byte_extract
-      throw "symex_assign_rec: unexpected assignment to union member";
+      throw unsupported_operation_exceptiont(
+        "symex_assign_rec: unexpected assignment to union member");
     }
     else
-      throw
-        "symex_assign_rec: unexpected assignment to member of `"+
-        type.id_string()+"'";
+      throw unsupported_operation_exceptiont(
+        "symex_assign_rec: unexpected assignment to member of `" +
+        type.id_string() + "'");
   }
   else if(lhs.id()==ID_if)
     symex_assign_if(
@@ -170,6 +179,7 @@ void goto_symext::symex_assign_rec(
   }
   else if(lhs.id() == ID_complex_real)
   {
+    // this is stuff like __real__ x = 1;
     const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
 
     const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
@@ -193,7 +203,8 @@ void goto_symext::symex_assign_rec(
       state, complex_imag_expr.op(), full_lhs, new_rhs, guard, assignment_type);
   }
   else
-    throw "assignment to `"+lhs.id_string()+"' not handled";
+    throw unsupported_operation_exceptiont(
+      "assignment to `" + lhs.id_string() + "' not handled");
 }
 
 void goto_symext::symex_assign_symbol(
@@ -283,9 +294,6 @@ void goto_symext::symex_assign_typecast(
   assignment_typet assignment_type)
 {
   // these may come from dereferencing on the lhs
-
-  assert(lhs.operands().size()==1);
-
   exprt rhs_typecasted=rhs;
   rhs_typecasted.make_typecast(lhs.op0().type());
 
@@ -303,29 +311,20 @@ void goto_symext::symex_assign_array(
   guardt &guard,
   assignment_typet assignment_type)
 {
-  // lhs must be index operand
-  // that takes two operands: the first must be an array
-  // the second is the index
-
-  if(lhs.operands().size()!=2)
-    throw "index must have two operands";
-
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
-  const typet &lhs_type=ns.follow(lhs_array.type());
+  const typet &lhs_index_type = ns.follow(lhs_array.type());
 
-  if(lhs_type.id()!=ID_array)
-    throw "index must take array type operand, but got `"+
-          lhs_type.id_string()+"'";
+  PRECONDITION(lhs_index_type.id() == ID_array);
 
-  #ifdef USE_UPDATE
+#ifdef USE_UPDATE
 
   // turn
   //   a[i]=e
   // into
   //   a'==UPDATE(a, [i], e)
 
-  update_exprt new_rhs(lhs_type);
+  update_exprt new_rhs(lhs_index_type);
   new_rhs.old()=lhs_array;
   new_rhs.designator().push_back(index_designatort(lhs_index));
   new_rhs.new_value()=rhs;
@@ -342,7 +341,7 @@ void goto_symext::symex_assign_array(
   //   a'==a WITH [i:=e]
 
   with_exprt new_rhs(lhs_array, lhs_index, rhs);
-  new_rhs.type() = lhs_type;
+  new_rhs.type() = lhs_index_type;
 
   exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
 
@@ -369,9 +368,7 @@ void goto_symext::symex_assign_struct_member(
   // typecasts involved? C++ does that for inheritance.
   if(lhs_struct.id()==ID_typecast)
   {
-    assert(lhs_struct.operands().size()==1);
-
-    if(lhs_struct.op0().id() == ID_null_object)
+    if(to_typecast_expr(lhs_struct).op0().id() == ID_null_object)
     {
       // ignore, and give up
       return;
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index c243cafbcd4..b3d1f0b8dae 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -11,15 +11,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
+#include <util/exception_utils.h>
+
 void goto_symext::symex_atomic_begin(statet &state)
 {
   if(state.guard.is_false())
     return;
 
-  // we don't allow any nesting of atomic sections
-  if(state.atomic_section_id!=0)
-    throw "nested atomic section detected at "+
-      state.source.pc->source_location.as_string();
+  if(state.atomic_section_id != 0)
+    throw incorrect_goto_program_exceptiont(
+      "we don't support nesting of atomic sections",
+      state.source.pc->source_location);
 
   state.atomic_section_id=++atomic_section_counter;
   state.read_in_atomic_section.clear();
@@ -36,8 +38,9 @@ void goto_symext::symex_atomic_end(statet &state)
   if(state.guard.is_false())
     return;
 
-  if(state.atomic_section_id==0)
-    throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
+  if(state.atomic_section_id == 0)
+    throw incorrect_goto_program_exceptiont(
+      "ATOMIC_END unmatched", state.source.pc->source_location);
 
   const unsigned atomic_section_id=state.atomic_section_id;
   state.atomic_section_id=0;
@@ -51,7 +54,7 @@ void goto_symext::symex_atomic_end(statet &state)
     r.set_level_2(r_it->second.first);
 
     // guard is the disjunction over reads
-    assert(!r_it->second.second.empty());
+    PRECONDITION(!r_it->second.second.empty());
     guardt read_guard(r_it->second.second.front());
     for(std::list<guardt>::const_iterator
         it=++(r_it->second.second.begin());
@@ -77,7 +80,7 @@ void goto_symext::symex_atomic_end(statet &state)
     w.set_level_2(state.level2.current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
-    assert(!w_it->second.empty());
+    PRECONDITION(!w_it->second.empty());
     guardt write_guard(w_it->second.front());
     for(std::list<guardt>::const_iterator
         it=++(w_it->second.begin());
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index f23726cd88a..f67d37febf2 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/invariant_utils.h>
+#include <util/optional.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
@@ -45,8 +46,7 @@ void goto_symext::symex_allocate(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=2)
-    throw "allocate expected to have two operands";
+  PRECONDITION(code.operands().size() == 2);
 
   if(lhs.is_nil())
     return; // ignore
@@ -162,8 +162,8 @@ void goto_symext::symex_allocate(
   state.rename(zero_init, ns); // to allow constant propagation
   simplify(zero_init, ns);
 
-  if(!zero_init.is_constant())
-    throw "allocate expects constant as second argument";
+  INVARIANT(
+    zero_init.is_constant(), "allocate expects constant as second argument");
 
   if(!zero_init.is_zero() && !zero_init.is_false())
   {
@@ -175,13 +175,9 @@ void goto_symext::symex_allocate(
         ns,
         null_message);
 
-    if(zero_value.is_not_nil())
-    {
-      code_assignt assignment(value_symbol.symbol_expr(), zero_value);
-      symex_assign(state, assignment);
-    }
-    else
-      throw "failed to zero initialize dynamic object";
+    CHECK_RETURN(zero_value.is_not_nil());
+    code_assignt assignment(value_symbol.symbol_expr(), zero_value);
+    symex_assign(state, assignment);
   }
   else
   {
@@ -234,8 +230,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  if(code.operands().size()!=1)
-    throw "va_arg_next expected to have one operand";
+  PRECONDITION(code.operands().size() == 1);
 
   if(lhs.is_nil())
     return; // ignore
@@ -313,8 +308,7 @@ void goto_symext::symex_printf(
   statet &state,
   const exprt &rhs)
 {
-  if(rhs.operands().empty())
-    throw "printf expected to have at least one operand";
+  PRECONDITION(!rhs.operands().empty());
 
   exprt tmp_rhs=rhs;
   state.rename(tmp_rhs, ns);
@@ -339,8 +333,7 @@ void goto_symext::symex_input(
   statet &state,
   const codet &code)
 {
-  if(code.operands().size()<2)
-    throw "input expected to have at least two operands";
+  PRECONDITION(code.operands().size() >= 2);
 
   exprt id_arg=code.op0();
 
@@ -364,8 +357,7 @@ void goto_symext::symex_output(
   statet &state,
   const codet &code)
 {
-  if(code.operands().size()<2)
-    throw "output expected to have at least two operands";
+  PRECONDITION(code.operands().size() >= 2);
 
   exprt id_arg=code.op0();
 
@@ -397,8 +389,7 @@ void goto_symext::symex_cpp_new(
 {
   bool do_array;
 
-  if(code.type().id()!=ID_pointer)
-    throw "new expected to return pointer";
+  PRECONDITION(code.type().id() == ID_pointer);
 
   do_array =
     (code.get(ID_statement) == ID_cpp_new_array ||
@@ -466,23 +457,22 @@ void goto_symext::symex_trace(
   statet &state,
   const code_function_callt &code)
 {
-  if(code.arguments().size()<2)
-    // NOLINTNEXTLINE(readability/throw)
-    throw "symex_trace expects at least two arguments";
+  PRECONDITION(code.arguments().size() >= 2);
 
   int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
 
   mp_integer debug_lvl;
-
-  if(to_integer(code.arguments()[0], debug_lvl))
-    // NOLINTNEXTLINE(readability/throw)
-    throw "CBMC_trace expects constant as first argument";
-
-  if(code.arguments()[1].id()!="implicit_address_of" ||
-     code.arguments()[1].operands().size()!=1 ||
-     code.arguments()[1].op0().id()!=ID_string_constant)
-    // NOLINTNEXTLINE(readability/throw)
-    throw "CBMC_trace expects string constant as second argument";
+  optionalt<mp_integer> maybe_debug =
+    numeric_cast<mp_integer>(code.arguments()[0]);
+  DATA_INVARIANT(
+    maybe_debug.has_value(), "CBMC_trace expects constant as first argument");
+  debug_lvl = maybe_debug.value();
+
+  DATA_INVARIANT(
+    code.arguments()[1].id() == "implicit_address_of" &&
+      code.arguments()[1].operands().size() == 1 &&
+      code.arguments()[1].op0().id() == ID_string_constant,
+    "CBMC_trace expects string constant as second argument");
 
   if(mp_integer(debug_thresh)>=debug_lvl)
   {
@@ -532,37 +522,33 @@ void goto_symext::symex_macro(
 {
   const irep_idt &identifier=code.op0().get(ID_identifier);
 
-  if(identifier==CPROVER_MACRO_PREFIX "waitfor")
-  {
-    #if 0
-    exprt new_fc("waitfor", fc.type());
+  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor");
+#if 0
+  exprt new_fc("waitfor", fc.type());
 
-    if(fc.operands().size()!=4)
-      throw "waitfor expected to have four operands";
+  if(fc.operands().size()!=4)
+    throw "waitfor expected to have four operands";
 
-    exprt &cycle_var=fc.op1();
-    exprt &bound=fc.op2();
-    exprt &predicate=fc.op3();
+  exprt &cycle_var=fc.op1();
+  exprt &bound=fc.op2();
+  exprt &predicate=fc.op3();
 
-    if(cycle_var.id()!=ID_symbol)
-      throw "waitfor expects symbol as first operand but got "+
-            cycle_var.id();
+  if(cycle_var.id()!=ID_symbol)
+    throw "waitfor expects symbol as first operand but got "+
+          cycle_var.id();
 
-    exprt new_cycle_var(cycle_var);
-    new_cycle_var.id("waitfor_symbol");
-    new_cycle_var.copy_to_operands(bound);
+  exprt new_cycle_var(cycle_var);
+  new_cycle_var.id("waitfor_symbol");
+  new_cycle_var.copy_to_operands(bound);
 
-    replace_expr(cycle_var, new_cycle_var, predicate);
+  replace_expr(cycle_var, new_cycle_var, predicate);
 
-    new_fc.operands().resize(4);
-    new_fc.op0().swap(cycle_var);
-    new_fc.op1().swap(new_cycle_var);
-    new_fc.op2().swap(bound);
-    new_fc.op3().swap(predicate);
+  new_fc.operands().resize(4);
+  new_fc.op0().swap(cycle_var);
+  new_fc.op1().swap(new_cycle_var);
+  new_fc.op2().swap(bound);
+  new_fc.op3().swap(predicate);
 
-    fc.swap(new_fc);
-    #endif
-  }
-  else
-    throw "unknown macro: "+id2string(identifier);
+  fc.swap(new_fc);
+#endif
 }
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index ee6c582bf5f..8e951d6eeb8 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -21,30 +21,23 @@ void goto_symext::symex_dead(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const codet &code = instruction.code;
-
-  if(code.operands().size()!=1)
-    throw "dead expects one operand";
-
-  if(code.op0().id()!=ID_symbol)
-    throw "dead expects symbol as first operand";
+  const code_deadt &code = to_code_dead(instruction.code);
 
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(to_symbol_expr(code.op0()));
+  ssa_exprt ssa(to_symbol_expr(code.symbol()));
   state.rename(ssa, ns, goto_symex_statet::L1);
 
   // in case of pointers, put something into the value set
   if(ns.follow(code.op0().type()).id()==ID_pointer)
   {
-    exprt failed=
-      get_failed_symbol(to_symbol_expr(code.op0()), ns);
+    exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
 
     exprt rhs;
 
     if(failed.is_not_nil())
-      rhs=address_of_exprt(failed, to_pointer_type(code.op0().type()));
+      rhs = address_of_exprt(failed, to_pointer_type(code.symbol().type()));
     else
       rhs=exprt(ID_invalid);
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 2961684a3fc..fbbbf5f7abe 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -25,14 +25,10 @@ void goto_symext::symex_decl(statet &state)
 
   const codet &code = instruction.code;
 
-  if(code.operands().size()==2)
-    throw "two-operand decl not supported here";
-
-  if(code.operands().size()!=1)
-    throw "decl expects one operand";
-
-  if(code.op0().id()!=ID_symbol)
-    throw "decl expects symbol as first operand";
+  // two-operand decl not supported here
+  // we handle the decl with only one operand
+  PRECONDITION(code.operands().size() == 1);
+  PRECONDITION(code.op0().id() == ID_symbol);
 
   symex_decl(state, to_symbol_expr(code.op0()));
 }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 7fcec279a2c..94e32e8a75d 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 
@@ -215,7 +216,8 @@ exprt goto_symext::address_arithmetic(
       result=address_of_exprt(result);
   }
   else
-    throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
+    throw unsupported_operation_exceptiont(
+      "goto_symext::address_arithmetic does not handle " + expr.id_string());
 
   const typet &expr_type=ns.follow(expr.type());
   INVARIANT((expr_type.id()==ID_array && !keep_array) ||
@@ -233,9 +235,7 @@ void goto_symext::dereference_rec(
 {
   if(expr.id()==ID_dereference)
   {
-    if(expr.operands().size()!=1)
-      throw "dereference takes one operand";
-
+    dereference_exprt to_check = to_dereference_expr(expr);
     bool expr_is_not_null = false;
 
     if(state.threads.size() == 1)
@@ -243,7 +243,6 @@ void goto_symext::dereference_rec(
       const irep_idt &expr_function = state.source.pc->function;
       if(!expr_function.empty())
       {
-        dereference_exprt to_check = to_dereference_expr(expr);
         state.get_original_name(to_check);
 
         expr_is_not_null =
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 073f58daf2c..13eaa80842a 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 
 bool goto_symext::get_unwind_recursion(
@@ -53,8 +54,9 @@ void goto_symext::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    if(identifier.empty())
-      throw "no identifier for function parameter";
+    INVARIANT(
+      !identifier.empty(),
+      "function pointer parameter must have an identifier");
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
@@ -119,7 +121,7 @@ void goto_symext::parameter_assignments(
           error << "function call: parameter \"" << identifier
                 << "\" type mismatch: got " << rhs.type().pretty()
                 << ", expected " << parameter_type.pretty();
-          throw error.str();
+          throw unsupported_operation_exceptiont(error.str());
         }
       }
 
@@ -172,14 +174,11 @@ void goto_symext::symex_function_call(
 {
   const exprt &function=code.function();
 
-  if(function.id()==ID_symbol)
-    symex_function_call_symbol(get_goto_function, state, code);
-  else if(function.id()==ID_if)
-    throw "symex_function_call can't do if";
-  else if(function.id()==ID_dereference)
-    throw "symex_function_call can't do dereference";
-  else
-    throw "unexpected function for symex_function_call: "+function.id_string();
+  // If at some point symex_function_call can support more
+  // expression ids(), like ID_Dereference, please expand the
+  // precondition appropriately.
+  PRECONDITION(function.id() == ID_symbol);
+  symex_function_call_symbol(get_goto_function, state, code);
 }
 
 void goto_symext::symex_function_call_symbol(
@@ -434,28 +433,18 @@ void goto_symext::return_assignment(statet &state)
 
   target.location(state.guard.as_expr(), state.source);
 
-  if(code.operands().size()==1)
-  {
-    exprt value=code.op0();
+  PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
 
-    if(frame.return_value.is_not_nil())
-    {
-      code_assignt assignment(frame.return_value, value);
+  exprt value = code.op0();
 
-      if(!base_type_eq(assignment.lhs().type(),
-                       assignment.rhs().type(), ns))
-        throw
-          "goto_symext::return_assignment type mismatch at "+
-          instruction.source_location.as_string()+":\n"+
-          "assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
-          "assignment.rhs().type():\n"+assignment.rhs().type().pretty();
-
-      symex_assign(state, assignment);
-    }
-  }
-  else
+  if(frame.return_value.is_not_nil())
   {
-    if(frame.return_value.is_not_nil())
-      throw "return with unexpected value";
+    code_assignt assignment(frame.return_value, value);
+
+    INVARIANT(
+      base_type_eq(assignment.lhs().type(), assignment.rhs().type(), ns),
+      "goto_symext::return_assignment type mismatch");
+
+    symex_assign(state, assignment);
   }
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 0bed128088f..3d4426325e1 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
@@ -48,8 +49,8 @@ void goto_symext::symex_goto(statet &state)
     !instruction.targets.empty(), "goto should have at least one target");
 
   // we only do deterministic gotos for now
-  if(instruction.targets.size()!=1)
-    throw "no support for non-deterministic gotos";
+  DATA_INVARIANT(
+    instruction.targets.size() == 1, "no support for non-deterministic gotos");
 
   goto_programt::const_targett goto_target=
     instruction.get_target();
@@ -345,8 +346,10 @@ void goto_symext::merge_goto(
   statet &state)
 {
   // check atomic section
-  if(state.atomic_section_id!=goto_state.atomic_section_id)
-    throw "atomic sections differ across branches";
+  if(state.atomic_section_id != goto_state.atomic_section_id)
+    throw incorrect_goto_program_exceptiont(
+      "atomic sections differ across branches",
+      state.source.pc->source_location);
 
   // do SSA phi functions
   phi_function(goto_state, state);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 587c4305e1c..2127bbd2d5e 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -14,10 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <memory>
 
+#include <util/exception_utils.h>
+#include <util/make_unique.h>
+#include <util/replace_symbol.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
-#include <util/replace_symbol.h>
-#include <util/make_unique.h>
 
 #include <analyses/dirty.h>
 
@@ -107,13 +108,12 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   {
     // forall X. P -> P
     // we keep the quantified variable unique by means of L2 renaming
-    PRECONDITION(expr.operands().size()==2);
-    PRECONDITION(expr.op0().id()==ID_symbol);
-    symbol_exprt tmp0=
-      to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
+    auto &quant_expr = to_quantifier_expr(expr);
+    symbol_exprt tmp0 =
+      to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
     symex_decl(state, tmp0);
-    exprt tmp=expr.op1();
-    expr.swap(tmp);
+    exprt tmp = quant_expr.where();
+    quant_expr.swap(tmp);
   }
 }
 
@@ -283,7 +283,7 @@ void goto_symext::symex_from_entry_point_of(
   }
   catch(const std::out_of_range &)
   {
-    throw "the program has no entry point";
+    throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
   statet state;
@@ -461,9 +461,9 @@ void goto_symext::symex_step(
     break;
 
   case NO_INSTRUCTION_TYPE:
-    throw "symex got NO_INSTRUCTION";
+    throw unsupported_operation_exceptiont("symex got NO_INSTRUCTION");
 
   default:
-    throw "symex got unexpected instruction";
+    UNREACHABLE;
   }
 }
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 9fed77da727..47a5603a88d 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -140,7 +140,7 @@ void goto_symext::symex_other(
     // - array_replace: the type of the second array (even if it is smaller)
     DATA_INVARIANT(
       code.operands().size() == 2,
-      "array_copy/array_replace takes two operands");
+      "expected array_copy/array_replace statement to have two operands");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());
@@ -188,7 +188,9 @@ void goto_symext::symex_other(
     // process_array_expr)
     // 3. use the type of the resulting array to construct an array_of
     // expression
-    DATA_INVARIANT(code.operands().size() == 2, "array_set takes two operands");
+    DATA_INVARIANT(
+      code.operands().size() == 2,
+      "expected array_set statement to have two operands");
 
     // we need to add dereferencing for the first operand
     exprt array_expr = dereference_exprt(code.op0());
@@ -235,7 +237,7 @@ void goto_symext::symex_other(
     // if the types don't match the result trivially is false
     DATA_INVARIANT(
       code.operands().size() == 3,
-      "array_equal expected to take three arguments");
+      "expected array_equal statement to have three operands");
 
     // we need to add dereferencing for the first two
     dereference_exprt array1(code.op0());
@@ -267,8 +269,9 @@ void goto_symext::symex_other(
   }
   else if(statement==ID_havoc_object)
   {
-    DATA_INVARIANT(code.operands().size()==1,
-                   "havoc_object must have one operand");
+    DATA_INVARIANT(
+      code.operands().size() == 1,
+      "expected havoc_object statement to have one operand");
 
     // we need to add dereferencing for the first operand
     dereference_exprt object(code.op0(), empty_typet());
@@ -277,5 +280,5 @@ void goto_symext::symex_other(
     havoc_rec(state, guardt(), object);
   }
   else
-    throw "unexpected statement: "+id2string(statement);
+    UNREACHABLE;
 }
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 9986812598e..acd8791a871 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
+#include <util/exception_utils.h>
 #include <util/expr_initializer.h>
 
 void goto_symext::symex_start_thread(statet &state)
@@ -18,18 +19,18 @@ void goto_symext::symex_start_thread(statet &state)
   if(state.guard.is_false())
     return;
 
-  // we don't allow spawning threads out of atomic sections
-  // this would require amendments to ordering constraints
-  if(state.atomic_section_id!=0)
-    throw "start_thread in atomic section detected";
+  if(state.atomic_section_id != 0)
+    throw incorrect_goto_program_exceptiont(
+      "spawning threads out of atomic sections is not allowed; "
+      "this would require amendments to ordering constraints",
+      state.source.pc->source_location);
 
   // record this
   target.spawn(state.guard.as_expr(), state.source);
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  if(instruction.targets.size()!=1)
-    throw "start_thread expects one target";
+  INVARIANT(instruction.targets.size() == 1, "start_thread expects one target");
 
   goto_programt::const_targett thread_target=
     instruction.get_target();