diff --git a/regression/goto-instrument/replace-calls-03/test.desc b/regression/goto-instrument/replace-calls-03/test.desc
index 736743235e7..7371edc8baa 100644
--- a/regression/goto-instrument/replace-calls-03/test.desc
+++ b/regression/goto-instrument/replace-calls-03/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g
-Functions f and g are not type-compatible
-^EXIT=11$
+functions f and g are not type-compatible
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/replace-calls-04/test.desc b/regression/goto-instrument/replace-calls-04/test.desc
index 736743235e7..7371edc8baa 100644
--- a/regression/goto-instrument/replace-calls-04/test.desc
+++ b/regression/goto-instrument/replace-calls-04/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g
-Functions f and g are not type-compatible
-^EXIT=11$
+functions f and g are not type-compatible
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/replace-calls-05/test.desc b/regression/goto-instrument/replace-calls-05/test.desc
index b88d8154f9e..f3552f5d564 100644
--- a/regression/goto-instrument/replace-calls-05/test.desc
+++ b/regression/goto-instrument/replace-calls-05/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --replace-calls f:g --replace-calls h:f
-Function f cannot both be replaced and be a replacement
-^EXIT=11$
+function f cannot both be replaced and be a replacement
+^EXIT=1$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp
index 39a4b33fbb0..d2ccb487be6 100644
--- a/src/goto-programs/lazy_goto_model.cpp
+++ b/src/goto-programs/lazy_goto_model.cpp
@@ -11,6 +11,7 @@
 
 #include <util/cmdline.h>
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
 #include <util/unicode.h>
 
@@ -96,8 +97,11 @@ void lazy_goto_modelt::initialize(
   const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    msg.error() << "Please provide a program" << messaget::eom;
-    throw 0;
+    throw invalid_command_line_argument_exceptiont(
+      "no program provided",
+      "source file names",
+      "one or more paths to a goto binary or a source file in a supported "
+      "language");
   }
 
   std::vector<std::string> binaries, sources;
@@ -124,9 +128,8 @@ void lazy_goto_modelt::initialize(
 
       if(!infile)
       {
-        msg.error() << "failed to open input file `" << filename
-                    << '\'' << messaget::eom;
-        throw 0;
+        throw system_exceptiont(
+          "failed to open input file `" + filename + '\'');
       }
 
       language_filet &lf=add_language_file(filename);
@@ -134,11 +137,8 @@ void lazy_goto_modelt::initialize(
 
       if(lf.language==nullptr)
       {
-        source_locationt location;
-        location.set_file(filename);
-        msg.error().source_location=location;
-        msg.error() << "failed to figure out type of file" << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont(
+          "failed to figure out type of file `" + filename + '\'');
       }
 
       languaget &language=*lf.language;
@@ -149,8 +149,7 @@ void lazy_goto_modelt::initialize(
 
       if(language.parse(infile, filename))
       {
-        msg.error() << "PARSING ERROR" << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont("PARSING ERROR");
       }
 
       lf.get_modules();
@@ -160,8 +159,7 @@ void lazy_goto_modelt::initialize(
 
     if(language_files.typecheck(symbol_table))
     {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      throw invalid_source_file_exceptiont("CONVERSION ERROR");
     }
   }
 
@@ -170,7 +168,12 @@ void lazy_goto_modelt::initialize(
     msg.status() << "Reading GOTO program from file" << messaget::eom;
 
     if(read_object_and_link(file, *goto_model, message_handler))
-      throw 0;
+    {
+      source_locationt source_location;
+      source_location.set_file(file);
+      throw incorrect_goto_program_exceptiont(
+        "failed to read/link goto model", source_location);
+    }
   }
 
   bool binaries_provided_start =
@@ -205,8 +208,7 @@ void lazy_goto_modelt::initialize(
 
   if(entry_point_generation_failed)
   {
-    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
-    throw 0;
+    throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
   }
 
   // stupid hack
diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp
index 5342c7a8fdb..dd77454fe84 100644
--- a/src/goto-programs/link_goto_model.cpp
+++ b/src/goto-programs/link_goto_model.cpp
@@ -18,6 +18,7 @@ Author: Michael Tautschnig, Daniel Kroening
 #include <util/rename_symbol.h>
 
 #include <linking/linking_class.h>
+#include <util/exception_utils.h>
 
 #include "goto_model.h"
 
@@ -171,15 +172,18 @@ void link_goto_model(
                    message_handler);
 
   if(linking.typecheck_main())
-    throw 0;
-
+  {
+    throw invalid_source_file_exceptiont("typechecking main failed");
+  }
   if(link_functions(
-      dest.symbol_table,
-      dest.goto_functions,
-      src.symbol_table,
-      src.goto_functions,
-      linking.rename_symbol,
-      weak_symbols,
-      linking.object_type_updates))
-    throw 0;
+       dest.symbol_table,
+       dest.goto_functions,
+       src.symbol_table,
+       src.goto_functions,
+       linking.rename_symbol,
+       weak_symbols,
+       linking.object_type_updates))
+  {
+    throw invalid_source_file_exceptiont("linking failed");
+  }
 }
diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp
index 86deb73eb43..d8ae62978f3 100644
--- a/src/goto-programs/loop_ids.cpp
+++ b/src/goto-programs/loop_ids.cpp
@@ -76,7 +76,7 @@ void show_loop_ids_json(
   const goto_programt &goto_program,
   json_arrayt &loops)
 {
-  assert(ui==ui_message_handlert::uit::JSON_UI); // use function above
+  PRECONDITION(ui == ui_message_handlert::uit::JSON_UI); // use function above
 
   forall_goto_program_instructions(it, goto_program)
   {
diff --git a/src/goto-programs/osx_fat_reader.cpp b/src/goto-programs/osx_fat_reader.cpp
index 574f1c74d4a..6d543205aec 100644
--- a/src/goto-programs/osx_fat_reader.cpp
+++ b/src/goto-programs/osx_fat_reader.cpp
@@ -11,8 +11,9 @@ Module: Read Mach-O
 
 #include "osx_fat_reader.h"
 
-#include <cassert>
 #include <cstdlib>
+#include <util/exception_utils.h>
+#include <util/invariant.h>
 
 #ifdef __APPLE__
 #include <mach-o/fat.h>
@@ -46,12 +47,13 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
   in.read(reinterpret_cast<char*>(&fh), sizeof(struct fat_header));
 
   if(!in)
-    throw "failed to read OSX fat header";
+    throw system_exceptiont("failed to read OSX fat header");
 
   if(!is_osx_fat_magic(reinterpret_cast<char*>(&(fh.magic))))
-    throw "OSX fat header malformed (magic)"; // NOLINT(readability/throw)
+    throw deserialization_exceptiont("OSX fat header malformed (magic)");
 
-  assert(sizeof(fh.nfat_arch)==4);
+  static_assert(
+    sizeof(fh.nfat_arch) == 4, "fat_header::nfat_arch is of type uint32_t");
   unsigned narch=__builtin_bswap32(fh.nfat_arch);
 
   for(unsigned i=0; !has_gb_arch && i<narch; ++i)
@@ -61,9 +63,10 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
     // NOLINTNEXTLINE(readability/identifiers)
     in.read(reinterpret_cast<char*>(&fa), sizeof(struct fat_arch));
 
-    assert(sizeof(fa.cputype)==4 &&
-           sizeof(fa.cpusubtype)==4 &&
-           sizeof(fa.size)==4);
+    static_assert(
+      sizeof(fa.cputype) == 4 && sizeof(fa.cpusubtype) == 4 &&
+        sizeof(fa.size) == 4,
+      "This requires a specific fat architecture");
     int cputype=__builtin_bswap32(fa.cputype);
     int cpusubtype=__builtin_bswap32(fa.cpusubtype);
     unsigned size=__builtin_bswap32(fa.size);
@@ -79,7 +82,7 @@ bool osx_fat_readert::extract_gb(
   const std::string &source,
   const std::string &dest) const
 {
-  assert(has_gb_arch);
+  PRECONDITION(has_gb_arch);
 
   return run("lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source});
 }
diff --git a/src/goto-programs/parameter_assignments.cpp b/src/goto-programs/parameter_assignments.cpp
index e0ce272328a..eb75475f9ce 100644
--- a/src/goto-programs/parameter_assignments.cpp
+++ b/src/goto-programs/parameter_assignments.cpp
@@ -46,7 +46,7 @@ void parameter_assignmentst::do_function_calls(
 
       // add x=y for f(y) where x is the parameter
 
-      assert(function_call.function().id()==ID_symbol);
+      PRECONDITION(function_call.function().id() == ID_symbol);
 
       const irep_idt &identifier=
         to_symbol_expr(function_call.function()).get_identifier();
diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp
index 8c23425af48..bc566a21159 100644
--- a/src/goto-programs/pointer_arithmetic.cpp
+++ b/src/goto-programs/pointer_arithmetic.cpp
@@ -32,32 +32,33 @@ void pointer_arithmetict::read(const exprt &src)
   }
   else if(src.id()==ID_minus)
   {
-    assert(src.operands().size()==2);
-    read(src.op0());
-    const unary_minus_exprt o(src.op1(), src.op1().type());
-    add_to_offset(o);
+    auto const &minus_src = to_minus_expr(src);
+    read(minus_src.op0());
+    const unary_minus_exprt unary_minus(
+      minus_src.op1(), minus_src.op1().type());
+    add_to_offset(unary_minus);
   }
   else if(src.id()==ID_address_of)
   {
-    assert(src.operands().size()==1);
-    if(src.op0().id()==ID_index)
+    auto const &address_of_src = to_address_of_expr(src);
+    if(address_of_src.op().id() == ID_index)
     {
-      const index_exprt &index_expr=
-        to_index_expr(src.op0());
+      const index_exprt &index_expr = to_index_expr(address_of_src.op());
 
       if(index_expr.index().is_zero())
-        make_pointer(src);
+        make_pointer(address_of_src);
       else
       {
         add_to_offset(index_expr.index());
         // produce &x[0] + i instead of &x[i]
-        exprt new_src=src;
-        new_src.op0().op1()=from_integer(0, index_expr.index().type());
-        make_pointer(new_src);
+        auto new_address_of_src = address_of_src;
+        new_address_of_src.op().op1() =
+          from_integer(0, index_expr.index().type());
+        make_pointer(new_address_of_src);
       }
     }
     else
-      make_pointer(src);
+      make_pointer(address_of_src);
   }
   else
     make_pointer(src);
diff --git a/src/goto-programs/printf_formatter.cpp b/src/goto-programs/printf_formatter.cpp
index 1cbbf879546..98c714ef8c1 100644
--- a/src/goto-programs/printf_formatter.cpp
+++ b/src/goto-programs/printf_formatter.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "printf_formatter.h"
 
-#include <cassert>
 #include <sstream>
 
 #include <util/c_types.h>
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index 0543c0d2ad9..a9b5a246ead 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -145,7 +145,10 @@ static bool read_bin_goto_object_v4(
       {
         unsigned n=*nit;
         rev_target_mapt::const_iterator entry=rev_target_map.find(n);
-        assert(entry!=rev_target_map.end());
+        INVARIANT(
+          entry != rev_target_map.end(),
+          "something from the target map should also be in the reverse target "
+          "map");
         ins->targets.push_back(entry->second);
       }
     }
diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp
index 19a475237ac..40eca4304dd 100644
--- a/src/goto-programs/remove_complex.cpp
+++ b/src/goto-programs/remove_complex.cpp
@@ -32,10 +32,9 @@ static exprt complex_member(const exprt &expr, irep_idt id)
   }
   else
   {
-    assert(expr.type().id()==ID_struct);
     const struct_typet &struct_type=
       to_struct_type(expr.type());
-    assert(struct_type.components().size()==2);
+    PRECONDITION(struct_type.components().size() == 2);
     return member_exprt(expr, id, struct_type.components().front().type());
   }
 }
@@ -105,20 +104,19 @@ static void remove_complex(exprt &expr)
 
   if(expr.id()==ID_typecast)
   {
-    assert(expr.operands().size()==1);
-    if(expr.op0().type().id()==ID_complex)
+    auto const &typecast_expr = to_typecast_expr(expr);
+    if(typecast_expr.op().type().id() == ID_complex)
     {
-      if(expr.type().id()==ID_complex)
+      if(typecast_expr.type().id() == ID_complex)
       {
         // complex to complex
       }
       else
       {
         // cast complex to non-complex is (T)__real__ x
-        unary_exprt tmp(
-          ID_complex_real, expr.op0(), expr.op0().type().subtype());
+        complex_real_exprt complex_real_expr(typecast_expr.op());
 
-        expr=typecast_exprt(tmp, expr.type());
+        expr = typecast_exprt(complex_real_expr, typecast_expr.type());
       }
     }
   }
@@ -131,7 +129,11 @@ static void remove_complex(exprt &expr)
     if(expr.id()==ID_plus || expr.id()==ID_minus ||
        expr.id()==ID_mult || expr.id()==ID_div)
     {
-      assert(expr.operands().size()==2);
+      // FIXME plus and mult are defined as n-ary operations
+      //      rather than binary. This code assumes that they
+      //      can only have exactly 2 operands, and it is not clear
+      //      that it is safe to do so in this context
+      PRECONDITION(expr.operands().size() == 2);
       // do component-wise:
       // x+y -> complex(x.r+y.r,x.i+y.i)
       struct_exprt struct_expr(expr.type());
@@ -153,62 +155,69 @@ static void remove_complex(exprt &expr)
     }
     else if(expr.id()==ID_unary_minus)
     {
-      assert(expr.operands().size()==1);
+      auto const &unary_minus_expr = to_unary_minus_expr(expr);
       // do component-wise:
       // -x -> complex(-x.r,-x.i)
-      struct_exprt struct_expr(expr.type());
+      struct_exprt struct_expr(unary_minus_expr.type());
       struct_expr.operands().resize(2);
 
-      struct_expr.op0()=
-        unary_minus_exprt(complex_member(expr.op0(), ID_real));
+      struct_expr.op0() =
+        unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real));
 
-      struct_expr.op0().add_source_location()=expr.source_location();
+      struct_expr.op0().add_source_location() =
+        unary_minus_expr.source_location();
 
-      struct_expr.op1()=
-        unary_minus_exprt(complex_member(expr.op0(), ID_imag));
+      struct_expr.op1() =
+        unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag));
 
-      struct_expr.op1().add_source_location()=expr.source_location();
+      struct_expr.op1().add_source_location() =
+        unary_minus_expr.source_location();
 
       expr=struct_expr;
     }
     else if(expr.id()==ID_complex)
     {
-      assert(expr.operands().size()==2);
-      expr.id(ID_struct);
+      auto const &complex_expr = to_complex_expr(expr);
+      auto struct_expr = struct_exprt(complex_expr.type());
+      struct_expr.add_source_location() = complex_expr.source_location();
+      struct_expr.copy_to_operands(complex_expr.real(), complex_expr.imag());
+      expr.swap(struct_expr);
     }
     else if(expr.id()==ID_typecast)
     {
-      assert(expr.operands().size()==1);
-      typet subtype=expr.type().subtype();
+      auto const &typecast_expr = to_typecast_expr(expr);
+      typet subtype = typecast_expr.type().subtype();
 
-      if(expr.op0().type().id()==ID_struct)
+      if(typecast_expr.op().type().id() == ID_struct)
       {
         // complex to complex -- do typecast per component
 
-        struct_exprt struct_expr(expr.type());
+        struct_exprt struct_expr(typecast_expr.type());
         struct_expr.operands().resize(2);
 
-        struct_expr.op0()=
-          typecast_exprt(complex_member(expr.op0(), ID_real), subtype);
+        struct_expr.op0() =
+          typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype);
 
-        struct_expr.op0().add_source_location()=expr.source_location();
+        struct_expr.op0().add_source_location() =
+          typecast_expr.source_location();
 
-        struct_expr.op1()=
-          typecast_exprt(complex_member(expr.op0(), ID_imag), subtype);
+        struct_expr.op1() =
+          typecast_exprt(complex_member(typecast_expr.op(), ID_imag), subtype);
 
-        struct_expr.op1().add_source_location()=expr.source_location();
+        struct_expr.op1().add_source_location() =
+          typecast_expr.source_location();
 
         expr=struct_expr;
       }
       else
       {
         // non-complex to complex
-        struct_exprt struct_expr(expr.type());
+        struct_exprt struct_expr(typecast_expr.type());
         struct_expr.operands().resize(2);
 
-        struct_expr.op0()=typecast_exprt(expr.op0(), subtype);
+        struct_expr.op0() = typecast_exprt(typecast_expr.op(), subtype);
         struct_expr.op1()=from_integer(0, subtype);
-        struct_expr.add_source_location()=expr.source_location();
+        struct_expr.add_source_location() = typecast_expr.source_location();
 
         expr=struct_expr;
       }
@@ -217,13 +226,11 @@ static void remove_complex(exprt &expr)
 
   if(expr.id()==ID_complex_real)
   {
-    assert(expr.operands().size()==1);
-    expr=complex_member(expr.op0(), ID_real);
+    expr = complex_member(to_complex_real_expr(expr).op0(), ID_real);
   }
   else if(expr.id()==ID_complex_imag)
   {
-    assert(expr.operands().size()==1);
-    expr=complex_member(expr.op0(), ID_imag);
+    expr = complex_member(to_complex_imag_expr(expr).op0(), ID_imag);
   }
 
   remove_complex(expr.type());
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 531a9bbc51a..acc49169674 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -127,7 +127,7 @@ exprt remove_const_function_pointerst::resolve_symbol(
 bool remove_const_function_pointerst::try_resolve_function_call(
   const exprt &expr, functionst &out_functions)
 {
-  assert(out_functions.empty());
+  PRECONDITION(out_functions.empty());
   const exprt &simplified_expr=simplify_expr(expr, ns);
   bool resolved=false;
   functionst resolved_functions;
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 846371c0ce7..c82f2966e02 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -281,7 +281,7 @@ void remove_function_pointerst::remove_function_pointer(
   const code_function_callt &code=
     to_code_function_call(target->code);
 
-  const exprt &function=code.function();
+  const auto &function = to_dereference_expr(code.function());
 
   // this better have the right type
   code_typet call_type=to_code_type(function.type());
@@ -296,12 +296,9 @@ void remove_function_pointerst::remove_function_pointer(
         code_typet::parametert(it->type()));
   }
 
-  assert(function.id()==ID_dereference);
-  assert(function.operands().size()==1);
-
   bool found_functions;
 
-  const exprt &pointer=function.op0();
+  const exprt &pointer = function.pointer();
   remove_const_function_pointerst::functionst functions;
   does_remove_constt const_removal_check(goto_program, ns);
   const auto does_remove_const = const_removal_check();
diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp
index 85cb1e3364c..6577c44d10e 100644
--- a/src/goto-programs/remove_unused_functions.cpp
+++ b/src/goto-programs/remove_unused_functions.cpp
@@ -77,9 +77,6 @@ void find_used_functions(
         {
           const code_function_callt &call = to_code_function_call(it->code);
 
-          // check that this is actually a simple call
-          assert(call.function().id()==ID_symbol);
-
           const irep_idt &identifier =
             to_symbol_expr(call.function()).get_identifier();
 
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index 0230c951c99..a0802876c72 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -82,13 +82,18 @@ static void remove_vector(exprt &expr)
        expr.id()==ID_mod  || expr.id()==ID_bitxor ||
        expr.id()==ID_bitand || expr.id()==ID_bitor)
     {
+      // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
+      //      operations rather than binary. This code assumes that they
+      //      can only have exactly 2 operands, and it is not clear
+      //      that it is safe to do so in this context
+      PRECONDITION(expr.operands().size() == 2);
+      auto const &binary_expr = to_binary_expr(expr);
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
       mp_integer dimension;
       to_integer(array_type.size(), dimension);
 
-      assert(expr.operands().size()==2);
       const typet subtype=array_type.subtype();
       // do component-wise:
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
@@ -99,22 +104,23 @@ static void remove_vector(exprt &expr)
       {
         exprt index=from_integer(i, array_type.size().type());
 
-        array_expr.operands()[i]=
-          binary_exprt(index_exprt(expr.op0(), index, subtype), expr.id(),
-                       index_exprt(expr.op1(), index, subtype));
+        array_expr.operands()[i] = binary_exprt(
+          index_exprt(binary_expr.op0(), index, subtype),
+          binary_expr.id(),
+          index_exprt(binary_expr.op1(), index, subtype));
       }
 
       expr=array_expr;
     }
     else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
     {
+      auto const &unary_expr = to_unary_expr(expr);
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
       mp_integer dimension;
       to_integer(array_type.size(), dimension);
 
-      assert(expr.operands().size()==1);
       const typet subtype=array_type.subtype();
       // do component-wise:
       // -x -> vector(-x[0],-x[1],...)
@@ -125,8 +131,8 @@ static void remove_vector(exprt &expr)
       {
         exprt index=from_integer(i, array_type.size().type());
 
-        array_expr.operands()[i]=
-          unary_exprt(expr.id(), index_exprt(expr.op0(), index, subtype));
+        array_expr.operands()[i] = unary_exprt(
+          unary_expr.id(), index_exprt(unary_expr.op0(), index, subtype));
       }
 
       expr=array_expr;
diff --git a/src/goto-programs/replace_calls.cpp b/src/goto-programs/replace_calls.cpp
index 2552dff0424..38e727983a2 100644
--- a/src/goto-programs/replace_calls.cpp
+++ b/src/goto-programs/replace_calls.cpp
@@ -16,6 +16,7 @@ Author: Daniel Poetzl
 #include <goto-programs/remove_returns.h>
 
 #include <util/base_type.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/irep.h>
 #include <util/string_utils.h>
@@ -105,8 +106,9 @@ void replace_callst::operator()(
       if(rhs.id() == ID_symbol)
       {
         const symbol_exprt &se = to_symbol_expr(rhs);
-        if(has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX))
-          throw "Returns must not be removed before replacing calls";
+        INVARIANT(
+          !has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX),
+          "returns must not be removed before replacing calls");
       }
     }
 
@@ -132,7 +134,10 @@ replace_callst::replacement_mapt replace_callst::parse_replacement_list(
       replacement_map.insert(std::make_pair(original, replacement));
 
     if(!r.second)
-      throw "Conflicting replacement for function " + original;
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "conflicting replacement for function " + original, "--replace-calls");
+    }
   }
 
   return replacement_map;
@@ -146,22 +151,26 @@ void replace_callst::check_replacement_map(
   for(const auto &p : replacement_map)
   {
     if(replacement_map.find(p.second) != replacement_map.end())
-      throw "Function " + id2string(p.second) +
-        " cannot both be replaced and "
-        "be a replacement";
+      throw invalid_command_line_argument_exceptiont(
+        "function " + id2string(p.second) +
+          " cannot both be replaced and be a replacement",
+        "--replace-calls");
 
     auto it2 = goto_functions.function_map.find(p.second);
 
     if(it2 == goto_functions.function_map.end())
-      throw "Replacement function " + id2string(p.second) +
-        " needs to be present";
+      throw invalid_command_line_argument_exceptiont(
+        "replacement function " + id2string(p.second) + " needs to be present",
+        "--replace-calls");
 
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
       if(!base_type_eq(it1->second.type, it2->second.type, ns))
-        throw "Functions " + id2string(p.first) + " and " +
-          id2string(p.second) + " are not type-compatible";
+        throw invalid_command_line_argument_exceptiont(
+          "functions " + id2string(p.first) + " and " + id2string(p.second) +
+            " are not type-compatible",
+          "--replace-calls");
     }
   }
 }