diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 02913f9360a..aef07c8d3f1 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -79,7 +79,7 @@ void constant_propagator_domaint::assign_rec(
         cond = simplify_expr(cond,ns);
       }
       else
-        assert(0);
+        UNREACHABLE;
 
       assign(values, to_symbol_expr(lhs), cond, ns);
 	}
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index da5bd52fb61..a81a08e6e67 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -296,7 +296,7 @@ void custom_bitvector_domaint::transform(
             else if(identifier=="__CPROVER_clear_may")
               mode=modet::CLEAR_MAY;
             else
-              assert(false);
+              UNREACHABLE;
 
             exprt lhs=code_function_call.arguments()[0];
 
@@ -411,7 +411,7 @@ void custom_bitvector_domaint::transform(
         else if(statement=="clear_may")
           mode=modet::CLEAR_MAY;
         else
-          assert(false);
+          UNREACHABLE;
 
         exprt lhs=instruction.code.op0();
 
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 4ab7d399117..b6ee194dd9f 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -833,7 +833,7 @@ void goto_checkt::nan_check(
           equal_exprt(expr.op1(), minus_inf)));
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   isnan.make_not();
 
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index c7de024f6f9..571d8bd0ad1 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -713,7 +713,7 @@ void goto_rw(goto_programt::const_targett target,
   switch(target->type)
   {
   case NO_INSTRUCTION_TYPE:
-    assert(false);
+    UNREACHABLE;
     break;
 
   case GOTO:
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index a91c0349bbb..718df977b33 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -474,7 +474,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
       }
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
   else if(expr.id()==ID_equal)
   {
@@ -673,7 +673,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
     else if(expr.id()==ID_notequal)
       return is_ne(p);
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   return tvt::unknown();
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 23be0fdb935..1a67c80c4fa 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -460,7 +460,7 @@ void ansi_c_convert_typet::write(typet &type)
         else
           type=unsigned_long_long_int_type();
       else
-        assert(false);
+        UNREACHABLE;
     }
     else if(gcc_int128_cnt)
     {
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index 00beb3a92cf..a0ef86cffe0 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/config.h>
 #include <util/std_types.h>
+#include <util/invariant.h>
 
 void ansi_c_declaratort::build(irept &src)
 {
@@ -36,7 +37,7 @@ void ansi_c_declaratort::build(irept &src)
     else if(t.id().empty() ||
             t.is_nil())
     {
-      assert(0);
+      UNREACHABLE;
     }
     else if(t.id()==ID_abstract)
     {
@@ -108,7 +109,7 @@ typet ansi_c_declarationt::full_type(
       p=&(p->subtypes().back());
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   *p=type();
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index b22896bd7f7..af1f6c1cb51 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -305,7 +305,7 @@ bool ansi_c_entry_point(
           max=to_unsignedbv_type(envp_size_symbol.type).largest();
         }
         else
-          assert(false);
+          UNREACHABLE;
 
         exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
 
@@ -431,7 +431,7 @@ bool ansi_c_entry_point(
       }
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
   else
   {
diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 927a928b187..26fb22355ff 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -106,7 +106,7 @@ static std::string type_max(const typet &src)
     return integer2string(
       power(2, to_unsignedbv_type(src).get_width()-1)-1);
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 /// quote a string for bash and CMD
@@ -766,7 +766,7 @@ bool c_preprocess_gcc_clang(
     else if(config.ansi_c.wchar_t_width==config.ansi_c.char_width)
       command+=" -D__WCHAR_TYPE__=\""+sig+" char\"";
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   if(config.ansi_c.char_is_unsigned)
@@ -804,7 +804,7 @@ bool c_preprocess_gcc_clang(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 
   // Standard Defines, ANSI9899 6.10.8
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index ce451e79f75..edf95e5379e 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -378,11 +378,11 @@ void c_typecastt::implicit_typecast_arithmetic(
     }
     return;
 
-  case BOOL:       assert(false); // should always be promoted to int
-  case CHAR:       assert(false); // should always be promoted to int
-  case UCHAR:      assert(false); // should always be promoted to int
-  case SHORT:      assert(false); // should always be promoted to int
-  case USHORT:     assert(false); // should always be promoted to int
+  case BOOL:       UNREACHABLE; // should always be promoted to int
+  case CHAR:       UNREACHABLE; // should always be promoted to int
+  case UCHAR:      UNREACHABLE; // should always be promoted to int
+  case SHORT:      UNREACHABLE; // should always be promoted to int
+  case USHORT:     UNREACHABLE; // should always be promoted to int
   case INT:        new_type=signed_int_type(); break;
   case UINT:       new_type=unsigned_int_type(); break;
   case LONG:       new_type=signed_long_int_type(); break;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index fee4e8685d1..54eab363d7b 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -77,7 +77,7 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
       else if(expr.id()==ID_minus)
         expr.id(ID_floatbv_minus);
       else
-        assert(false);
+        UNREACHABLE;
 
       expr.op2()=from_integer(0, unsigned_int_type());
     }
@@ -875,7 +875,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
   else if(last_statement==ID_function_call)
   {
     // this is suspected to be dead
-    assert(false);
+    UNREACHABLE;
 
     // make the last statement an expression
 
@@ -2852,7 +2852,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
         else if(expr.id()==ID_bitxor)
           expr.id(ID_xor);
         else
-          assert(false);
+          UNREACHABLE;
         expr.type()=type0;
         return;
       }
@@ -3010,7 +3010,7 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
     else
     {
       p_op=int_op=nullptr;
-      assert(false);
+      UNREACHABLE;
     }
 
     const typet &int_op_type=follow(int_op->type());
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 1bc494c8d4a..7d388cc68dd 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -344,7 +344,7 @@ void c_typecheck_baset::designator_enter(
     entry.subtype=vector_type.subtype();
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   designator.push_entry(entry);
 }
@@ -478,7 +478,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       dest=&(dest->op0());
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   // second phase: assign value
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 5195e653364..393be7dbf54 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -380,7 +380,7 @@ void c_typecheck_baset::typecheck_custom_type(typet &type)
     type.set(ID_f, integer2string(f_int));
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void c_typecheck_baset::typecheck_code_type(code_typet &type)
@@ -759,7 +759,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
       else if(compound_symbol.type.id()==ID_union)
         compound_symbol.type.id(ID_incomplete_union);
       else
-        assert(false);
+        UNREACHABLE;
 
       symbolt *new_symbol;
       move_symbol(compound_symbol, new_symbol);
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index e5159d720f1..eecc856a0f7 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -114,7 +114,7 @@ void expr2ct::get_shorthands(const exprt &expr)
     ns_collision[symbol->location.get_function()].insert(sh);
 
     if(!shorthands.insert(std::make_pair(*it, sh)).second)
-      assert(false);
+      UNREACHABLE;
   }
 
   for(find_symbols_sett::const_iterator
diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h
index 89c4614cc12..42b95de39f4 100644
--- a/src/cbmc/all_properties_class.h
+++ b/src/cbmc/all_properties_class.h
@@ -56,7 +56,7 @@ class bmc_all_propertiest:
       }
 
       // make some poor compilers happy
-      assert(false);
+      UNREACHABLE;
       return "";
     }
 
diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp
index 3cee2da664b..9522107d922 100644
--- a/src/cbmc/counterexample_beautification.cpp
+++ b/src/cbmc/counterexample_beautification.cpp
@@ -74,7 +74,7 @@ counterexample_beautificationt::get_failed_property(
        prop_conv.l_get(it->cond_literal).is_false())
       return it;
 
-  assert(false);
+  UNREACHABLE;
   return equation.SSA_steps.end();
 }
 
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index 0f7da6270f9..adcfd3dff20 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -73,7 +73,7 @@ fault_localizationt::get_failed_property()
        bmc.prop_conv.l_get(it->cond_literal).is_false())
       return it;
 
-  assert(false);
+  UNREACHABLE;
   return bmc.equation.SSA_steps.end();
 }
 
diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index f9ac9cc207d..dc9fef60567 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -247,7 +247,7 @@ void goto_program_coverage_recordt::compute_coverage_lines(
       branches_total+=2;
       if(!entry.first->second.conditions.insert(
           {it, coverage_conditiont()}).second)
-        assert(false);
+        UNREACHABLE;
     }
 
     symex_coveraget::coveraget::const_iterator c_entry=
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 7df4d5fa56f..66fc8fb6896 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -433,7 +433,7 @@ void clobber_parse_optionst::report_success()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -458,7 +458,7 @@ void clobber_parse_optionst::show_counterexample(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -481,7 +481,7 @@ void clobber_parse_optionst::report_failure()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp
index df037cda6cb..e2eeaae1ca6 100644
--- a/src/cpp/cpp_constructor.cpp
+++ b/src/cpp/cpp_constructor.cpp
@@ -183,7 +183,7 @@ codet cpp_typecheckt::cpp_constructor(
   }
   else if(tmp_type.id()==ID_union)
   {
-    assert(0); // Todo: union
+    UNREACHABLE; // Todo: union
   }
   else if(tmp_type.id()==ID_struct)
   {
@@ -301,7 +301,7 @@ codet cpp_typecheckt::cpp_constructor(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   codet nil;
   nil.make_nil();
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index b98845964e0..ae5853d07b3 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/src/cpp/cpp_convert_type.cpp
@@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <cassert>
 
-#include <util/config.h>
 #include <util/arith_tools.h>
-#include <util/std_types.h>
-
 #include <util/c_types.h>
+#include <util/config.h>
+#include <util/invariant.h>
+#include <util/std_types.h>
 
 #include "cpp_declaration.h"
 #include "cpp_name.h"
@@ -285,7 +285,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
       throw "ellipsis only allowed as last parameter";
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   // if we just have one parameter of type void, remove it
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 9d7ee9b3121..e01b7bacaf3 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -91,7 +91,7 @@ symbolt &cpp_declarator_convertert::convert(
     // adjust template type
     if(final_type.id()==ID_template)
     {
-      assert(0);
+      UNREACHABLE;
       typet tmp;
       tmp.swap(final_type.subtype());
       final_type.swap(tmp);
diff --git a/src/cpp/cpp_scope.cpp b/src/cpp/cpp_scope.cpp
index c3849384d67..1521472ccd3 100644
--- a/src/cpp/cpp_scope.cpp
+++ b/src/cpp/cpp_scope.cpp
@@ -20,7 +20,7 @@ std::ostream &operator << (std::ostream &out, cpp_scopet::lookup_kindt kind)
   case cpp_scopet::QUALIFIED: return out << "QUALIFIED";
   case cpp_scopet::SCOPE_ONLY: return out << "SCOPE_ONLY";
   case cpp_scopet::RECURSIVE: return out << "RECURSIVE";
-  default: assert(false);
+  default: UNREACHABLE;
   }
 
   return out;
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index e87efb885fb..b1be4281d3b 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -250,7 +250,7 @@ void cpp_typecheckt::do_not_typechecked()
           cont=true;
         }
         else
-          assert(0); // Don't know what to do!
+          UNREACHABLE; // Don't know what to do!
       }
     }
   }
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 5c0a6afe285..29a2a7e0efc 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -380,7 +380,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void put_compound_into_scope(const struct_union_typet::componentt &component);
   void typecheck_compound_body(symbolt &symbol);
-  void typecheck_compound_body(struct_union_typet &type) { assert(false); }
+  void typecheck_compound_body(struct_union_typet &type) { UNREACHABLE; }
   void typecheck_enum_body(symbolt &symbol);
   void typecheck_method_bodies(method_bodiest &);
   void typecheck_compound_bases(struct_typet &type);
diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp
index c076d1e131b..26d2efb210e 100644
--- a/src/cpp/cpp_typecheck_bases.cpp
+++ b/src/cpp/cpp_typecheck_bases.cpp
@@ -209,7 +209,7 @@ void cpp_typecheckt::add_base_components(
         component.set_access(ID_private);
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     // put into scope
   }
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index f2c5d04f36f..e3d314f44aa 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -1750,7 +1750,7 @@ bool cpp_typecheckt::dynamic_typecast(
     {
       if(!e.get_bool(ID_C_lvalue))
         return false;
-      assert(0); // currently not supported
+      UNREACHABLE; // currently not supported
     }
     else if(follow(type.subtype()).id()==ID_struct)
     {
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 88b26461482..cac26bd5dc3 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -1021,7 +1021,7 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr)
   {
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   typet pointer_type=follow(expr.op0().type());
 
@@ -1065,7 +1065,7 @@ void cpp_typecheckt::typecheck_expr_typecast(exprt &expr)
   // should not be called
   #if 0
   std::cout << "E: " << expr.pretty() << '\n';
-  assert(0);
+  UNREACHABLE;
   #endif
 }
 
@@ -1392,7 +1392,7 @@ void cpp_typecheckt::typecheck_cast_expr(exprt &expr)
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   expr.swap(new_expr);
 }
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index e492a170cbf..7795b71e4c0 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -121,7 +121,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
         symbol.value.type().add("to-member") = resolved_expr.op0().type();
       }
       else
-        assert(false);
+        UNREACHABLE;
 
       if(symbol.type != symbol.value.type())
       {
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 0b49853f5fd..c323794f10b 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -405,7 +405,7 @@ void cpp_typecheck_resolvet::filter(
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
 
     if(match)
@@ -2078,7 +2078,7 @@ void cpp_typecheck_resolvet::apply_template_args(
 
   // We never try 'unassigned' template arguments.
   if(template_args_tc.has_unassigned())
-    assert(false);
+    UNREACHABLE;
 
   // a template is always a declaration
   const cpp_declarationt &cpp_declaration=
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 494f9e48ff5..bcdc444de36 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -1026,7 +1026,7 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
     break;
 
    default:
-    assert(0);
+    UNREACHABLE;
     break;
   }
 
@@ -1941,7 +1941,7 @@ bool Parser::optMemberSpec(cpp_member_spect &member_spec)
     case TOK_VIRTUAL:  member_spec.set_virtual(true); break;
     case TOK_FRIEND:   member_spec.set_friend(true); break;
     case TOK_EXPLICIT: member_spec.set_explicit(true); break;
-    default: assert(false);
+    default: UNREACHABLE;
     }
 
     t=lex.LookAhead(0);
@@ -1978,7 +1978,7 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
     case TOK_MUTABLE: storage_spec.set_mutable(); break;
     case TOK_GCC_ASM: storage_spec.set_asm(); break;
     case TOK_THREAD_LOCAL: storage_spec.set_thread_local(); break;
-    default: assert(false);
+    default: UNREACHABLE;
     }
 
     set_location(storage_spec, tk);
@@ -2048,7 +2048,7 @@ bool Parser::optCvQualify(typet &cv)
         break;
 
       default:
-        assert(false);
+        UNREACHABLE;
         break;
       }
     }
@@ -4205,7 +4205,7 @@ bool Parser::rClassSpec(typet &spec)
   else if(t==TOK_UNION)
     spec=typet(ID_union);
   else
-    assert(false);
+    UNREACHABLE;
 
   set_location(spec, tk);
 
@@ -4314,7 +4314,7 @@ bool Parser::rBaseSpecifiers(irept &bases)
         break;
 
        default:
-        assert(0);
+        UNREACHABLE;
       }
 
       t=lex.LookAhead(0);
@@ -4438,7 +4438,7 @@ bool Parser::rClassMember(cpp_itemt &member)
       break;
 
     default:
-      assert(0);
+      UNREACHABLE;
     }
 
     set_location(member, tk1);
@@ -5487,7 +5487,7 @@ bool Parser::rUnaryExpr(exprt &exp)
       break;
 
     default:
-      assert(0);
+      UNREACHABLE;
     }
 
     exp.move_to_operands(right);
@@ -6393,7 +6393,7 @@ bool Parser::rTypePredicate(exprt &expr)
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 
   return true;
diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp
index 4df80e3a089..16949d7aaa7 100644
--- a/src/cpp/template_map.cpp
+++ b/src/cpp/template_map.cpp
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <ostream>
 
+#include <util/invariant.h>
+
 void template_mapt::apply(typet &type) const
 {
   if(type.id()==ID_array)
@@ -190,7 +192,7 @@ void template_mapt::set(
   if(parameter.id()==ID_type)
   {
     if(parameter.id()!=ID_type)
-      assert(false); // typechecked before!
+      UNREACHABLE; // typechecked before!
 
     typet tmp=value.type();
 
@@ -202,7 +204,7 @@ void template_mapt::set(
     // must be non-type
 
     if(value.id()==ID_type)
-      assert(false); // typechecked before!
+      UNREACHABLE; // typechecked before!
 
     irep_idt identifier=parameter.get(ID_identifier);
     expr_map[identifier]=value;
diff --git a/src/goto-cc/goto_cc_cmdline.cpp b/src/goto-cc/goto_cc_cmdline.cpp
index 8691b9db770..ac86ee38551 100644
--- a/src/goto-cc/goto_cc_cmdline.cpp
+++ b/src/goto-cc/goto_cc_cmdline.cpp
@@ -18,6 +18,7 @@ Date:   April 2010
 #include <iostream>
 #include <cstdio>
 
+#include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/tempfile.h>
 
@@ -101,7 +102,7 @@ std::size_t goto_cc_cmdlinet::get_optnr(const std::string &opt_string)
   }
   else
   {
-    assert(false);
+    UNREACHABLE;
     return -1;
   }
 
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index 44946ab2f4c..cec37680a53 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -591,7 +591,7 @@ void change_impactt::output_change_impact(
     else if(mod_flags&DEL_CTRL_DEP)
       prefix='c';
     else
-      assert(false);
+      UNREACHABLE;
 
     output_instruction(prefix, goto_program, ns, function, target);
   }
@@ -653,12 +653,12 @@ void change_impactt::output_change_impact(
       else if(old_mod_flags&DEL_CTRL_DEP)
         prefix='c';
       else
-        assert(false);
+        UNREACHABLE;
 
       ++o_target;
     }
     else if(mod_flags&DELETED)
-      assert(false);
+      UNREACHABLE;
     else if(mod_flags&NEW)
       prefix='+';
     else if(mod_flags&NEW_DATA_DEP)
@@ -680,7 +680,7 @@ void change_impactt::output_change_impact(
       ++o_target;
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     output_instruction(prefix, goto_program, n_ns, function, target);
   }
@@ -697,17 +697,17 @@ void change_impactt::output_change_impact(
     // syntactic changes are preferred over data/control-dependence
     // modifications
     if(old_mod_flags==SAME)
-      assert(false);
+      UNREACHABLE;
     else if(old_mod_flags&DELETED)
       prefix='-';
     else if(old_mod_flags&NEW)
-      assert(false);
+      UNREACHABLE;
     else if(old_mod_flags&DEL_DATA_DEP)
       prefix='d';
     else if(old_mod_flags&DEL_CTRL_DEP)
       prefix='c';
     else
-      assert(false);
+      UNREACHABLE;
 
     output_instruction(prefix, goto_program, o_ns, function, o_target);
   }
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 1a96eb4ee34..e773b91cd02 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -88,7 +88,7 @@ void goto_program2codet::build_loop_map()
       }
 
     if(!loop_map.insert(std::make_pair(loop_start, loop_end)).second)
-      assert(false);
+      UNREACHABLE;
   }
 }
 
@@ -249,11 +249,11 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return convert_catch(target, upper_bound, dest);
 
     case NO_INSTRUCTION_TYPE:
-      assert(false);
+      UNREACHABLE;
   }
 
   // not reached
-  assert(false);
+  UNREACHABLE;
   return target;
 }
 
@@ -817,7 +817,7 @@ bool goto_program2codet::set_block_end_points(
         break;
 
       if(!processed_locations.insert(case_end->location_number).second)
-        assert(false);
+        UNREACHABLE;
 
       it->case_last=case_end;
     }
@@ -1022,7 +1022,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
       // this improves convergence
       if(it->case_start!=(--cases.end())->case_start)
       {
-        assert(false);
+        UNREACHABLE;
         goto_programt::instructiont i=*(it->case_selector);
         i.guard=true_exprt();
         goto_programt tmp;
@@ -1416,7 +1416,7 @@ goto_programt::const_targett goto_program2codet::convert_throw(
     codet &dest)
 {
   // this isn't really clear as throw is not supported in expr2cpp either
-  assert(false);
+  UNREACHABLE;
   return target;
 }
 
@@ -1426,7 +1426,7 @@ goto_programt::const_targett goto_program2codet::convert_catch(
     codet &dest)
 {
   // this isn't really clear as catch is not supported in expr2cpp either
-  assert(false);
+  UNREACHABLE;
   return target;
 }
 
diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp
index 7e01d66e62a..319acf8674c 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -136,7 +136,7 @@ bool model_argc_argv(
     else if(has_prefix(id2string(it->first),
                        CPROVER_PREFIX "initialize::") &&
             symbol_table.add(it->second))
-      assert(false);
+      UNREACHABLE;
   }
 
   assert(value.is_not_nil());
diff --git a/src/goto-instrument/show_locations.cpp b/src/goto-instrument/show_locations.cpp
index b02dcb1b099..2b9580add2f 100644
--- a/src/goto-instrument/show_locations.cpp
+++ b/src/goto-instrument/show_locations.cpp
@@ -57,7 +57,7 @@ void show_locations(
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 }
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index 78015b22e6f..81f19d30c7a 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -177,7 +177,7 @@ void goto_unwindt::unwind(
     else if(unwind_strategy==unwind_strategyt::ASSUME)
       new_t->make_assumption(exit_cond);
     else
-      assert(false);
+      UNREACHABLE;
 
     new_t->source_location=loop_head->source_location;
     new_t->function=loop_head->function;
diff --git a/src/goto-programs/basic_blocks.cpp b/src/goto-programs/basic_blocks.cpp
index 44e1ff7bacb..75b91b82bd6 100644
--- a/src/goto-programs/basic_blocks.cpp
+++ b/src/goto-programs/basic_blocks.cpp
@@ -89,6 +89,6 @@ void basic_blocks(goto_programt &goto_program,
       }
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 }
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 911e25460cc..f1a103e2428 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -221,7 +221,7 @@ void goto_convertt::do_printf(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void goto_convertt::do_scanf(
@@ -326,7 +326,7 @@ void goto_convertt::do_scanf(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void goto_convertt::do_input(
@@ -833,7 +833,7 @@ void goto_convertt::cpp_new_initializer(
       convert(to_code(initializer), dest);
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 }
 
@@ -1396,7 +1396,7 @@ void goto_convertt::do_function_call_symbol(
   }
   else if(identifier=="__builtin_unreachable")
   {
-    // says something like assert(false);
+    // says something like UNREACHABLE;
   }
   else if(identifier==ID_gcc_builtin_va_arg)
   {
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index 2e1bd83598b..dcb6d7153cd 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -403,7 +403,7 @@ void cfg_baset<T, P, I>::compute_edges(
     break;
 
   case NO_INSTRUCTION_TYPE:
-    assert(false);
+    UNREACHABLE;
     break;
   }
 }
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index aa6ddd70d7a..710c90595cd 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -839,7 +839,7 @@ void goto_convertt::convert_cpp_delete(
   else if(code.get_statement()==ID_cpp_delete)
     delete_identifier="__delete";
   else
-    assert(false);
+    UNREACHABLE;
 
   if(destructor.is_not_nil())
   {
@@ -858,7 +858,7 @@ void goto_convertt::convert_cpp_delete(
       convert(tmp_code, dest);
     }
     else
-      assert(false);
+      UNREACHABLE;
   }
 
   // now do "free"
@@ -1810,7 +1810,7 @@ void goto_convertt::generate_ifthenelse(
      true_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
-    // if(some) { label: assert(0); }
+    // if(some) { label: assert(false); }
     true_case.instructions.back().guard=boolean_negate(guard);
     dest.destructive_append(true_case);
     true_case.instructions.clear();
@@ -1823,7 +1823,7 @@ void goto_convertt::generate_ifthenelse(
      false_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
-    // if(some) ... else { label: assert(0); }
+    // if(some) ... else { label: assert(false); }
     false_case.instructions.back().guard=guard;
     dest.destructive_append(false_case);
     false_case.instructions.clear();
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 2fc795254d2..ac12c64be41 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -123,7 +123,7 @@ void goto_convertt::remove_assignment(
     convert(assignment, dest);
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   // revert assignment in the expression to its LHS
   if(result_is_used)
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index d832412509c..15749d2012d 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -56,7 +56,7 @@ void goto_trace_stept::output(
     out << "FUNCTION RETURN"; break;
   default:
     out << "unknown type: " << static_cast<int>(type) << std::endl;
-    assert(false);
+    UNREACHABLE;
   }
 
   if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO)
@@ -386,16 +386,16 @@ void show_goto_trace(
       break;
 
     case goto_trace_stept::typet::CONSTRAINT:
-      assert(false);
+      UNREACHABLE;
       break;
 
     case goto_trace_stept::typet::SHARED_READ:
     case goto_trace_stept::typet::SHARED_WRITE:
-      assert(false);
+      UNREACHABLE;
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 }
diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp
index 5f4c560a0bd..86deb73eb43 100644
--- a/src/goto-programs/loop_ids.cpp
+++ b/src/goto-programs/loop_ids.cpp
@@ -67,7 +67,7 @@ void show_loop_ids(
       break;
     }
     case ui_message_handlert::uit::JSON_UI:
-      assert(false); // use function below
+      UNREACHABLE; // use function below
   }
 }
 
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index ebfaf6a75d1..466d6cef4ab 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -114,7 +114,7 @@ bool read_bin_goto_object_v3(
          rev_target_map.insert(
            rev_target_map.end(),
            std::make_pair(instruction.target_number, itarget))->second!=itarget)
-        assert(false);
+        UNREACHABLE;
 
       std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
       for(std::size_t i=0; i<t_count; i++)
diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp
index 13ff90f908b..78b655e4108 100644
--- a/src/goto-programs/remove_complex.cpp
+++ b/src/goto-programs/remove_complex.cpp
@@ -24,7 +24,7 @@ static exprt complex_member(const exprt &expr, irep_idt id)
     else if(id==ID_imag)
       return expr.op1();
     else
-      assert(false);
+      UNREACHABLE;
   }
   else
   {
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index 0ea5f16fad6..7f0be70cc64 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -64,7 +64,7 @@ void show_properties(
       break;
 
     case ui_message_handlert::uit::JSON_UI:
-      assert(false);
+      UNREACHABLE;
       break;
 
     case ui_message_handlert::uit::PLAIN:
@@ -79,7 +79,7 @@ void show_properties(
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 }
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index fbb8aa32316..f7599e16578 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -481,7 +481,7 @@ goto_programt::targett string_abstractiont::abstract(
 
   case RETURN:
     // use remove_returns
-    assert(false);
+    UNREACHABLE;
     break;
 
   case END_FUNCTION:
@@ -498,7 +498,7 @@ goto_programt::targett string_abstractiont::abstract(
   case LOCATION:
     break;
   case NO_INSTRUCTION_TYPE:
-    assert(false);
+    UNREACHABLE;
     break;
   }
 
@@ -647,7 +647,7 @@ exprt string_abstractiont::build(
 
   exprt str_struct;
   if(build_wrap(pointer, str_struct, write))
-    assert(false);
+    UNREACHABLE;
 
   exprt result=member(str_struct, what);
 
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index bd13a853605..9616a3daa20 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -304,7 +304,7 @@ static void assert_l1_renaming(const exprt &expr)
   if(check_renaming_l1(expr))
   {
     std::cerr << expr.pretty() << '\n';
-    assert(false);
+    UNREACHABLE;
   }
   #else
   (void)expr;
@@ -317,7 +317,7 @@ static void assert_l2_renaming(const exprt &expr)
   if(check_renaming(expr))
   {
     std::cerr << expr.pretty() << '\n';
-    assert(false);
+    UNREACHABLE;
   }
   #else
   (void)expr;
@@ -439,7 +439,7 @@ void goto_symex_statet::set_ssa_indices(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index e0f82ba6af2..e79c6f3d90d 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -133,7 +133,7 @@ irep_idt partial_order_concurrencyt::rw_clock_id(
   else if(event->is_shared_read())
     return id2string(id(event))+"$rclk$"+std::to_string(axiom);
   else
-    assert(false);
+    UNREACHABLE;
 
   return "";
 }
@@ -156,7 +156,7 @@ symbol_exprt partial_order_concurrencyt::clock(
       std::to_string(numbering[event])+"$spwnclk$"+std::to_string(axiom);
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   return symbol_exprt(identifier, clock_type);
 }
diff --git a/src/goto-symex/partial_order_concurrency.h b/src/goto-symex/partial_order_concurrency.h
index 5163451e210..adb82366cbd 100644
--- a/src/goto-symex/partial_order_concurrency.h
+++ b/src/goto-symex/partial_order_concurrency.h
@@ -116,7 +116,7 @@ class numbered_evtst
     const ordered_evtst::size_type offset=ordered_evts.size();
     ordered_evts.push_back(&evt);
     if(!ordered_evts_map.insert(std::make_pair(&evt, offset)).second)
-      assert(false);
+      UNREACHABLE;
     assert(ordered_evts.size()==ordered_evts_map.size());
 
     if(evt.direction==evtt::D_SYNC ||
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 0a59b7befea..67795005c37 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -105,7 +105,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -196,7 +196,7 @@ void symex_slicet::collect_open_variables(
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 01c09f400bd..518df75b954 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -472,7 +472,7 @@ void goto_symext::symex_assign_byte_extract(
   else if(lhs.id()==ID_byte_extract_big_endian)
     new_rhs.id(ID_byte_update_big_endian);
   else
-    assert(false);
+    UNREACHABLE;
 
   new_rhs.copy_to_operands(lhs.op(), lhs.offset(), rhs);
   new_rhs.type()=lhs.op().type();
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index f066ee1065f..1349233d45e 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -297,7 +297,7 @@ void goto_symext::dereference_rec(
           to_index_expr(expr).array().type().id()==ID_pointer)
   {
     // old stuff, will go away
-    assert(false);
+    UNREACHABLE;
   }
   else if(expr.id()==ID_address_of)
   {
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index d5b30fa4b05..e98480e98a9 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -66,7 +66,7 @@ void goto_symext::symex_other(
   }
   else if(statement==ID_decl)
   {
-    assert(false); // see symex_decl.cpp
+    UNREACHABLE; // see symex_decl.cpp
   }
   else if(statement==ID_nondet)
   {
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 8ebed5216c1..d1ec5fc4d4b 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -71,7 +71,7 @@ void goto_symext::symex_start_thread(statet &state)
     if(!state.level1.current_names.insert(
         std::make_pair(lhs.get_l1_object_identifier(),
                        std::make_pair(lhs, 0))).second)
-      assert(false);
+      UNREACHABLE;
     state.rename(lhs, ns, goto_symex_statet::L1);
     const irep_idt l1_name=lhs.get_l1_object_identifier();
     // store it
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 6627e198b71..76a6bae061a 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -511,7 +511,7 @@ void symex_target_equationt::convert_assertions(
         prop_conv.set_to_true(step.cond_expr);
     }
 
-    assert(false); // unreachable
+    UNREACHABLE; // unreachable
   }
 
   // We do (NOT a1) OR (NOT a2) ...
@@ -695,7 +695,7 @@ void symex_target_equationt::SSA_stept::output(
   case goto_trace_stept::typet::GOTO:
     out << "IF " << from_expr(ns, "", cond_expr) << " GOTO\n"; break;
 
-  default: assert(false);
+  default: UNREACHABLE;
   }
 
   if(is_assert() || is_assume() || is_assignment() || is_constraint())
diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp
index 36a1213ef1c..d39b56145d2 100644
--- a/src/java_bytecode/expr2java.cpp
+++ b/src/java_bytecode/expr2java.cpp
@@ -189,7 +189,7 @@ std::string expr2javat::convert_constant(
 
     mp_integer int_value;
     if(to_integer(src, int_value))
-      assert(false);
+      UNREACHABLE;
 
     dest+="(char)'";
 
@@ -212,7 +212,7 @@ std::string expr2javat::convert_constant(
     // No byte-literals in Java, so just cast:
     mp_integer int_value;
     if(to_integer(src, int_value))
-      assert(false);
+      UNREACHABLE;
     std::string dest="(byte)";
     dest+=integer2string(int_value);
     return dest;
@@ -222,7 +222,7 @@ std::string expr2javat::convert_constant(
     // No short-literals in Java, so just cast:
     mp_integer int_value;
     if(to_integer(src, int_value))
-      assert(false);
+      UNREACHABLE;
     std::string dest="(short)";
     dest+=integer2string(int_value);
     return dest;
@@ -232,7 +232,7 @@ std::string expr2javat::convert_constant(
     // long integer literals must have 'L' at the end
     mp_integer int_value;
     if(to_integer(src, int_value))
-      assert(false);
+      UNREACHABLE;
     std::string dest=integer2string(int_value);
     dest+='L';
     return dest;
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index ef3c16a20e1..7025bca1f57 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1793,7 +1793,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
         statement=="ifge"?ID_ge:
         statement=="ifgt"?ID_gt:
         statement=="ifle"?ID_le:
-        (assert(false), "");
+        irep_idt();
+
+      INVARIANT(!id.empty(), "unexpected bytecode-if");
 
       assert(op.size()==1 && results.empty());
       mp_integer number;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 73953905875..7711940b781 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -161,7 +161,7 @@ bool java_bytecode_languaget::parse(
       java_class_loader.add_jar_file(path);
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   if(!main_class.empty())
   {
diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp
index 14dd365b0bc..22d59cf95e0 100644
--- a/src/java_bytecode/java_types.cpp
+++ b/src/java_bytecode/java_types.cpp
@@ -92,7 +92,7 @@ reference_typet java_array_type(const char subtype)
   case 'j': subtype_str="long"; break;
   case 'l': subtype_str="long"; break;
   case 'a': subtype_str="reference"; break;
-  default: assert(false);
+  default: UNREACHABLE;
   }
 
   irep_idt class_name="array["+subtype_str+"]";
@@ -131,7 +131,7 @@ typet java_type_from_char(char t)
   case 'd': return java_double_type();
   case 'z': return java_boolean_type();
   case 'a': return java_reference_type(void_typet());
-  default: assert(false); return nil_typet();
+  default: UNREACHABLE; return nil_typet();
   }
 }
 
diff --git a/src/musketeer/fence_inserter.cpp b/src/musketeer/fence_inserter.cpp
index cd1aaa910f5..10de10049eb 100644
--- a/src/musketeer/fence_inserter.cpp
+++ b/src/musketeer/fence_inserter.cpp
@@ -40,7 +40,7 @@ unsigned fence_insertert::fence_cost(fence_typet f) const
     case Ctlfence:
       return 1;
   }
-  assert(false);
+  UNREACHABLE;
   return 0;
 }
 
@@ -769,7 +769,7 @@ void fence_insertert::solve()
       break;
     case GLP_UNDEF:
       instrumenter.message.result() << "Solution undefined" << messaget::eom;
-      assert(0);
+      UNREACHABLE;
     case GLP_FEAS:
       instrumenter.message.result() << "Solution feasible, "
                                     << "yet not proven optimal, "
@@ -779,7 +779,7 @@ void fence_insertert::solve()
     case GLP_NOFEAS:
       instrumenter.message.result()
         << "No feasible solution, the system is UNSAT" << messaget::eom;
-      assert(0);
+      UNREACHABLE;
   }
 
   event_grapht &egraph=instrumenter.egraph;
@@ -964,7 +964,7 @@ std::string fence_insertert::to_string(fence_typet f) const
     case Branching: return "branching";
     case Ctlfence: return "ctlfence";
   }
-  assert(0);
+  UNREACHABLE;
 }
 
 inline unsigned fence_insertert::col_to_var(unsigned u) const
@@ -983,7 +983,7 @@ inline fence_insertert::fence_typet fence_insertert::col_to_fence(unsigned u)
     case 3: return Branching;
     case 4: return Ctlfence;
   }
-  assert(0);
+  UNREACHABLE;
 }
 
 inline unsigned fence_insertert::var_fence_to_col(fence_typet f, unsigned var)
@@ -997,7 +997,7 @@ inline unsigned fence_insertert::var_fence_to_col(fence_typet f, unsigned var)
     case Branching: return (var-1)*fence_options+3;
     case Ctlfence: return (var-1)*fence_options+4;
   }
-  assert(0);
+  UNREACHABLE;
 }
 
 void fence_insertert::compute_fence_options()
@@ -1103,5 +1103,5 @@ typet fence_insertert::type_component(
     return type;
   }
 
-  assert(0);
+  UNREACHABLE;
 }
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index 043ac0fb05c..0d8db5f979a 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -524,7 +524,7 @@ void path_symext::assign_rec(
     else if(ssa_lhs.id()==ID_byte_extract_big_endian)
       new_id=ID_byte_update_big_endian;
     else
-      assert(false);
+      UNREACHABLE;
 
     byte_update_exprt new_rhs(new_id);
 
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 28b5bf360a0..f28b51a12c5 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1492,7 +1492,7 @@ void value_sett::apply_code(
   else if(statement==ID_function_call)
   {
     // shouldn't be here
-    assert(false);
+    UNREACHABLE;
   }
   else if(statement==ID_assign ||
           statement==ID_init)
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index d08694b82da..3d5cb1b64ef 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -244,7 +244,7 @@ exprt value_set_fit::to_expr(object_map_dt::const_iterator it) const
 
 bool value_set_fit::make_union(const value_set_fit::valuest &new_values)
 {
-  assert(0);
+  UNREACHABLE;
   bool result=false;
 
   for(valuest::const_iterator
@@ -1428,7 +1428,7 @@ void value_set_fit::apply_code(
   else if(statement==ID_function_call)
   {
     // shouldn't be here
-    assert(false);
+    UNREACHABLE;
   }
   else if(statement==ID_assign ||
           statement==ID_init)
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 3ea5ef1aa8e..c45c999b507 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -1586,7 +1586,7 @@ void value_set_fivrt::apply_code(
   else if(statement==ID_function_call)
   {
     // shouldn't be here
-    assert(false);
+    UNREACHABLE;
   }
   else if(statement==ID_assign ||
           statement==ID_init)
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 015a97271e1..322b2ea2fc9 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mp_arith.h>
 #include <util/namespace.h>
 #include <util/reference_counting.h>
+#include <util/invariant.h>
 
 #include "object_numbering.h"
 
@@ -100,11 +101,11 @@ class value_set_fivrt
     // operator[] is the only way to insert something!
     std::pair<iterator, bool> insert(const std::pair<unsigned, objectt>&)
     {
-      assert(false);
+      UNREACHABLE;
     }
     iterator insert(iterator, const std::pair<unsigned, objectt>&)
     {
-      assert(false);
+      UNREACHABLE;
     }
 
     class validity_ranget
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 3b5ce55a3aa..8e4078ded41 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -1239,7 +1239,7 @@ void value_set_fivrnst::apply_code(
   else if(statement==ID_function_call)
   {
     // shouldn't be here
-    assert(false);
+    UNREACHABLE;
   }
   else if(statement==ID_assign ||
           statement==ID_init)
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index db735cfe2d1..d3b452c0408 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mp_arith.h>
 #include <util/namespace.h>
 #include <util/reference_counting.h>
+#include <util/invariant.h>
 
 #include "object_numbering.h"
 
@@ -101,11 +102,11 @@ class value_set_fivrnst
     // operator[] is the only way to insert something!
     std::pair<iterator, bool> insert(const std::pair<unsigned, objectt>&)
     {
-      assert(false);
+      UNREACHABLE;
     }
     iterator insert(iterator, const std::pair<unsigned, objectt>&)
     {
-      assert(false);
+      UNREACHABLE;
     }
 
     class validity_ranget
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index f2da45da76c..2361f3c494c 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -499,7 +499,7 @@ void symex_parse_optionst::report_success()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -524,7 +524,7 @@ void symex_parse_optionst::show_counterexample(
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -547,7 +547,7 @@ void symex_parse_optionst::report_failure()
     break;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 5b94a141dfa..680b5309775 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -199,7 +199,7 @@ constant_exprt from_integer(
   }
 
   {
-    assert(false);
+    PRECONDITION(false);
     constant_exprt r;
     r.make_nil();
     return r;
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
index e9691db7322..ebb243952f4 100644
--- a/src/util/arith_tools.h
+++ b/src/util/arith_tools.h
@@ -26,7 +26,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value);
 // returns 'true' on error
 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);
 
-// assert(false) in case of unsupported type
+// PRECONDITION(false) in case of unsupported type
 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
 
 // ceil(log2(size))
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
index 4287e04adf1..b04dee98aa0 100644
--- a/src/util/bv_arithmetic.cpp
+++ b/src/util/bv_arithmetic.cpp
@@ -42,7 +42,7 @@ void bv_spect::from_type(const typet &type)
   else if(type.id()==ID_signedbv)
     is_signed=true;
   else
-    assert(0);
+    UNREACHABLE;
 
   width=unsafe_string2unsigned(type.get_string(ID_width));
 }
diff --git a/src/util/byte_operators.cpp b/src/util/byte_operators.cpp
index 9ebc340d9cb..74aa67e53d7 100644
--- a/src/util/byte_operators.cpp
+++ b/src/util/byte_operators.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include "invariant.h"
 #include "config.h"
 
 irep_idt byte_extract_id()
@@ -23,7 +24,7 @@ irep_idt byte_extract_id()
     return ID_byte_extract_big_endian;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -38,6 +39,6 @@ irep_idt byte_update_id()
     return ID_byte_update_big_endian;
 
   default:
-    assert(false);
+    UNREACHABLE;
   }
 }
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index cc2880cb577..6c553f5adbc 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_types.h"
 #include "config.h"
+#include "invariant.h"
 
 #include "c_types.h"
 
@@ -67,7 +68,7 @@ unsignedbv_typet size_type()
   else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
     return unsigned_long_long_int_type();
   else
-    assert(false); // aaah!
+    INVARIANT(false, "width of size type"); // aaah!
 }
 
 signedbv_typet signed_size_type()
@@ -249,7 +250,7 @@ bitvector_typet long_double_type()
       // not quite right. The extra bits beyond 80 are usually padded.
     }
     else
-      assert(false);
+      INVARIANT(false, "width of long double");
 
     result.set(ID_C_c_type, ID_long_double);
 
@@ -290,7 +291,7 @@ signedbv_typet pointer_diff_type()
   else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
     return signed_long_long_int_type();
   else
-    assert(false); // aaah!
+    INVARIANT(false, "width of pointer difference");
 }
 
 pointer_typet pointer_type(const typet &subtype)
diff --git a/src/util/config.cpp b/src/util/config.cpp
index c2a6afd60be..4048cfd417a 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -172,7 +172,7 @@ void configt::ansi_ct::set_arch_spec_i386()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -209,7 +209,7 @@ void configt::ansi_ct::set_arch_spec_x86_64()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -270,7 +270,7 @@ void configt::ansi_ct::set_arch_spec_power(const irep_idt &subarch)
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -313,7 +313,7 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -342,7 +342,7 @@ void configt::ansi_ct::set_arch_spec_alpha()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -382,7 +382,7 @@ void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch)
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -392,7 +392,7 @@ void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch)
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -411,7 +411,7 @@ void configt::ansi_ct::set_arch_spec_s390()
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -421,7 +421,7 @@ void configt::ansi_ct::set_arch_spec_s390()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -439,7 +439,7 @@ void configt::ansi_ct::set_arch_spec_s390x()
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -449,7 +449,7 @@ void configt::ansi_ct::set_arch_spec_s390x()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -479,7 +479,7 @@ void configt::ansi_ct::set_arch_spec_sparc(const irep_idt &subarch)
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -489,7 +489,7 @@ void configt::ansi_ct::set_arch_spec_sparc(const irep_idt &subarch)
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -520,7 +520,7 @@ void configt::ansi_ct::set_arch_spec_ia64()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -545,7 +545,7 @@ void configt::ansi_ct::set_arch_spec_x32()
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -555,7 +555,7 @@ void configt::ansi_ct::set_arch_spec_x32()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -599,7 +599,7 @@ void configt::ansi_ct::set_arch_spec_hppa()
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -609,7 +609,7 @@ void configt::ansi_ct::set_arch_spec_hppa()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
@@ -629,7 +629,7 @@ void configt::ansi_ct::set_arch_spec_sh4()
     break;
 
   case flavourt::VISUAL_STUDIO:
-    assert(false); // not supported by Visual Studio
+    UNREACHABLE; // not supported by Visual Studio
     break;
 
   case flavourt::APPLE:
@@ -639,7 +639,7 @@ void configt::ansi_ct::set_arch_spec_sh4()
     break;
 
   case flavourt::NONE:
-    assert(false);
+    UNREACHABLE;
   }
 }
 
diff --git a/src/util/decision_procedure.cpp b/src/util/decision_procedure.cpp
index 85f52acdba2..61f30f626b4 100644
--- a/src/util/decision_procedure.cpp
+++ b/src/util/decision_procedure.cpp
@@ -15,6 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool decision_proceduret::in_core(const exprt &expr)
 {
-  assert(false);
+  UNREACHABLE;
   return true;
 }
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 913bc8ad5df..677f7b6b81e 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "endianness_map.h"
 
 #include <ostream>
-#include <cassert>
 
+#include "invariant.h"
 #include "std_types.h"
 #include "pointer_offset_size.h"
 #include "arith_tools.h"
@@ -64,7 +64,7 @@ void endianness_mapt::build_big_endian(const typet &src)
   {
     // these do get re-ordered!
     mp_integer bits=pointer_offset_bits(src, ns); // error is -1
-    assert(bits>=0);
+    CHECK_RETURN(bits>=0);
 
     size_t bits_int=integer2size_t(bits), base=map.size();
 
@@ -107,7 +107,7 @@ void endianness_mapt::build_big_endian(const typet &src)
 
     mp_integer s;
     if(to_integer(vector_type.size(), s))
-      assert(false);
+      CHECK_RETURN(false);
 
     while(s>0)
     {
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index ba9fb9ac857..c5fdb82de38 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -678,7 +678,7 @@ void ieee_floatt::divide_and_round(
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 }
diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h
index 8cbfcce4002..a558ec42901 100644
--- a/src/util/sharing_map.h
+++ b/src/util/sharing_map.h
@@ -386,7 +386,7 @@ SHARING_MAPT(void)::get_delta_view(
     }
     else
     {
-      assert(false);
+      UNREACHABLE;
     }
   }
   while(!stack.empty());
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index c2501f7f345..19b41712649 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -17,6 +17,8 @@ Author: Daniel Poetzl
 #include <memory>
 #include <cassert>
 
+#include "invariant.h"
+
 #define _sn_assert(b) assert(b)
 //#define _sn_assert(b)
 
@@ -235,7 +237,7 @@ class sharing_nodet
       }
     }
 
-    assert(false);
+    UNREACHABLE;
   }
 
   // misc
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index d7a72c455bc..5d0e00b4b2e 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1538,7 +1538,7 @@ exprt simplify_exprt::bits2expr(
 
     mp_integer size;
     if(to_integer(array_type.size(), size))
-      assert(false);
+      UNREACHABLE;
     std::size_t n_el=integer2size_t(size);
 
     std::size_t el_size=
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index cff452cfcbd..41f92a4a514 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -310,7 +310,7 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
       else if(expr.id()==ID_floatbv_div)
         result/=v1;
       else
-        assert(false);
+        UNREACHABLE;
 
       expr=result.to_expr();
       return false;
@@ -363,7 +363,7 @@ bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
     else if(expr.id()==ID_ieee_float_equal)
       expr.make_bool(f0.ieee_equal(f1));
     else
-      assert(false);
+      UNREACHABLE;
 
     return false;
   }
@@ -380,7 +380,7 @@ bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
     else if(expr.id()==ID_ieee_float_equal)
       isnan.make_not();
     else
-      assert(false);
+      UNREACHABLE;
 
     expr.swap(isnan);
     return false;
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index a94674c3fd9..995447c1c7e 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -581,7 +581,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
       else if(expr.id()==ID_bitxor)
         new_expr.id(ID_xor);
       else
-        assert(false);
+        UNREACHABLE;
 
       Forall_operands(it, new_expr)
       {
@@ -1266,7 +1266,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       else if(expr.id()==ID_lt)
         expr.make_bool(f0<f1);
       else
-        assert(false);
+        UNREACHABLE;
 
       return false;
     }
@@ -1288,7 +1288,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       else if(expr.id()==ID_lt)
         expr.make_bool(f0<f1);
       else
-        assert(false);
+        UNREACHABLE;
 
       return false;
     }
@@ -1315,7 +1315,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       else if(expr.id()==ID_lt)
         expr.make_bool(r0<r1);
       else
-        assert(false);
+        UNREACHABLE;
 
       return false;
     }
@@ -1342,7 +1342,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       else if(expr.id()==ID_lt)
         expr.make_bool(v0<v1);
       else
-        assert(false);
+        UNREACHABLE;
 
       return false;
     }
@@ -1377,7 +1377,7 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     return simplify_inequality_not_constant(expr);
   }
 
-  assert(false);
+  UNREACHABLE;
   return false;
 }
 
@@ -1516,7 +1516,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
         else
         {
           tmp=false;
-          assert(0);
+          UNREACHABLE;
         }
 
         if(first)
diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp
index 370b9d07a59..3e687b2bb55 100644
--- a/src/util/ssa_expr.cpp
+++ b/src/util/ssa_expr.cpp
@@ -37,7 +37,7 @@ static void build_ssa_identifier_rec(
 
     mp_integer idx;
     if(to_integer(to_constant_expr(index.index()), idx))
-      assert(false);
+      UNREACHABLE;
 
     os << '[' << idx << ']';
   }
@@ -68,7 +68,7 @@ static void build_ssa_identifier_rec(
     }
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 /* Used to determine whether or not an identifier can be built
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index b2d0c4f36d5..1b074b9522f 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -44,7 +44,7 @@ std::size_t struct_union_typet::component_number(
     number++;
   }
 
-  assert(false);
+  UNREACHABLE;
   return 0;
 }
 
diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp
index b796befa707..7a2f9a460a2 100644
--- a/src/util/tempdir.cpp
+++ b/src/util/tempdir.cpp
@@ -14,7 +14,6 @@ Author: CM Wintersteiger
 #include <direct.h>
 #endif
 
-#include <cassert>
 #include <cstdlib>
 #include <cstring>
 
@@ -27,6 +26,7 @@ Author: CM Wintersteiger
 #include <unistd.h>
 #endif
 
+#include "invariant.h"
 #include "file_util.h"
 
 std::string get_temporary_directory(const std::string &name_template)
@@ -100,11 +100,11 @@ temp_working_dirt::temp_working_dirt(const std::string &name_template):
 {
   old_working_directory=get_current_working_directory();
   if(chdir(path.c_str())!=0)
-    assert(false);
+    CHECK_RETURN(false);
 }
 
 temp_working_dirt::~temp_working_dirt()
 {
   if(chdir(old_working_directory.c_str())!=0)
-    assert(false);
+    CHECK_RETURN(false);
 }
diff --git a/src/util/union_find.cpp b/src/util/union_find.cpp
index e7b3230f305..e30744c7c24 100644
--- a/src/util/union_find.cpp
+++ b/src/util/union_find.cpp
@@ -117,7 +117,7 @@ unsigned_union_find::size_type unsigned_union_find::get_other(size_type a)
     if(find(i)==a && i!=a)
       return i;
 
-//  assert(false);
+//  UNREACHABLE;
   return 0;
 }
 
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index d76f5b1f956..84df9d7a3ad 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -140,7 +140,7 @@ static bool build_graph_rec(
   }
   else
   {
-    assert(false);
+    UNREACHABLE;
     return true;
   }