diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 53f21aa5ab5..03c060372f0 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -236,7 +236,7 @@ exprt c_nondet_symbol_factory(
 
   symbolt *main_symbol_ptr;
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  assert(!moving_symbol_failed);
+  CHECK_RETURN(!moving_symbol_failed);
 
   std::vector<symbolt const *> symbols_created;
   symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 7d388cc68dd..4f2804e1521 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -33,10 +33,10 @@ void c_typecheck_baset::do_initializer(
 
   if(type.id()==ID_array)
   {
-    // any arrays must have a size
     const typet &result_type=follow(result.type());
-    assert(result_type.id()==ID_array &&
-           to_array_type(result_type).size().is_not_nil());
+    DATA_INVARIANT(result_type.id()==ID_array &&
+                   to_array_type(result_type).size().is_not_nil(),
+                   "any array must have a size");
 
     // we don't allow initialisation with symbols of array type
     if(result.id()!=ID_array)
@@ -436,9 +436,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         throw 0;
       }
 
-      assert(index<components.size());
-      assert(components[index].type().id()!=ID_code &&
-             !components[index].get_is_padding());
+      DATA_INVARIANT(index<components.size(),
+                     "member designator is bounded by components size");
+      DATA_INVARIANT(components[index].type().id()!=ID_code &&
+                     !components[index].get_is_padding(),
+                     "member designator points at data member");
 
       dest=&(dest->operands()[index]);
     }
@@ -449,7 +451,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       const union_typet::componentst &components=
         union_type.components();
 
-      assert(index<components.size());
+      DATA_INVARIANT(index<components.size(),
+                     "member designator is bounded by components size");
 
       const union_typet::componentt &component=union_type.components()[index];
 
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 4796f5e3d76..35f3454e30c 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -537,7 +537,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         vt_symb_type.is_type=true;
 
         const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
-        assert(!failed);
+        CHECK_RETURN(!failed);
 
         // add a virtual-table pointer
         struct_typet::componentt compo;
@@ -613,7 +613,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
           // add the parameter to the symbol table
           const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
-          assert(!failed);
+          CHECK_RETURN(!failed);
         }
 
         // do the body of the function
@@ -671,7 +671,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         // add the function to the symbol table
         {
           const bool failed=!symbol_table.insert(std::move(func_symb)).second;
-          assert(!failed);
+          CHECK_RETURN(!failed);
         }
 
         // next base
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index 2ec3a686c2d..813e2c76ef6 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -486,8 +486,8 @@ void cpp_typecheckt::default_assignop_value(
 
       mp_integer size;
       bool to_int=to_integer(size_expr, size);
-      assert(!to_int);
-      assert(size>=0);
+      CHECK_RETURN(!to_int);
+      CHECK_RETURN(size>=0);
 
       exprt::operandst empty_operands;
       for(mp_integer i=0; i < size; ++i)
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 013f861886d..dab7936f70b 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -215,8 +215,8 @@ void cpp_typecheckt::zero_initializer(
     mp_integer size;
 
     bool to_int=to_integer(size_expr, size);
-    assert(!to_int);
-    assert(size>=0);
+    CHECK_RETURN(!to_int);
+    CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;
     for(mp_integer i=0; i<size; ++i)
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index c323794f10b..97fd84135ee 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -2125,7 +2125,8 @@ void cpp_typecheck_resolvet::apply_template_args(
         const struct_typet &struct_type=
           to_struct_type(type_symb.type);
 
-        assert(struct_type.has_component(new_symbol.name));
+        DATA_INVARIANT(struct_type.has_component(new_symbol.name),
+                       "method should exist in struct");
         member_exprt member(code_type);
         member.set_component_name(new_symbol.name);
         member.struct_op()=*fargs.operands.begin();
diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp
index 328efabbcaf..a954500d5ac 100644
--- a/src/cpp/cpp_typecheck_virtual_table.cpp
+++ b/src/cpp/cpp_typecheck_virtual_table.cpp
@@ -96,6 +96,6 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     vt_symb_var.value=values;
 
     bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
-    assert(!failed);
+    CHECK_RETURN(!failed);
   }
 }
diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp
index df72550d5c0..505c6e65f84 100644
--- a/src/goto-instrument/accelerate/polynomial.cpp
+++ b/src/goto-instrument/accelerate/polynomial.cpp
@@ -409,7 +409,7 @@ int monomialt::compare(monomialt &other)
     return -1;
   }
 
-  assert(!"NOTREACHEDBITCHES");
+  UNREACHABLE;
 }
 
 int polynomialt::max_degree(const exprt &var)
diff --git a/src/goto-instrument/accelerate/util.cpp b/src/goto-instrument/accelerate/util.cpp
index 15563559adb..b67b062f8e6 100644
--- a/src/goto-instrument/accelerate/util.cpp
+++ b/src/goto-instrument/accelerate/util.cpp
@@ -117,5 +117,6 @@ typet join_types(const typet &t1, const typet &t2)
   std::cerr << "Tried to join types: "
             << t1.pretty() << " and " << t2.pretty()
             << '\n';
-  assert(!"Couldn't join types");
+
+  INVARIANT(false, "failed to join types");
 }
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 67994855cb6..f77bcec3298 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -185,7 +185,8 @@ void full_slicert::add_jumps(
         if(cfg[entry->second].node_required)
         {
           const irep_idt id2=goto_programt::get_function_id(*d_it);
-          assert(id==id2);
+          INVARIANT(id==id2,
+                    "goto/jump expected to be within a single function");
 
           cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
             pd.cfg.entry_map.find(*d_it);
diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h
index 6360fbaeb74..072c6f54267 100644
--- a/src/goto-instrument/unwind.h
+++ b/src/goto-instrument/unwind.h
@@ -119,7 +119,7 @@ class goto_unwindt
       const unsigned location_number)
     {
       auto r=location_map.insert(std::make_pair(target, location_number));
-      assert(r.second); // did not exist yet
+      INVARIANT(r.second, "target already exists");
     }
 
     typedef std::map<goto_programt::const_targett, unsigned> location_mapt;
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 69eb502760d..9d896a75255 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -406,9 +406,9 @@ class event_grapht
 
   event_idt add_node()
   {
-    const event_idt po_no = po_graph.add_node();
-    const event_idt com_no = com_graph.add_node();
-    assert(po_no == com_no);
+    const event_idt po_no=po_graph.add_node();
+    const event_idt com_no=com_graph.add_node();
+    INVARIANT(po_no==com_no, "node added with same id in both graphs");
     return po_no;
   }
 
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 1349233d45e..4fd3b0176a2 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -221,8 +221,9 @@ exprt goto_symext::address_arithmetic(
     throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
 
   const typet &expr_type=ns.follow(expr.type());
-  assert((expr_type.id()==ID_array && !keep_array) ||
-         base_type_eq(pointer_type(expr_type), result.type(), ns));
+  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
+            base_type_eq(pointer_type(expr_type), result.type(), ns),
+            "either non-persistent array or pointer to result");
 
   return result;
 }
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 00652d34618..cca06fdb375 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1320,8 +1320,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
             "java::org.cprover.CProver.assume:(Z)V")
     {
       const code_typet &code_type=to_code_type(arg0.type());
-      // sanity check: function has the right number of args
-      assert(code_type.parameters().size()==1);
+      INVARIANT(code_type.parameters().size()==1,
+                "function expected to have exactly one parameter");
 
       exprt operand = pop(1)[0];
       // we may need to adjust the type of the argument
@@ -1384,7 +1384,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(use_this)
       {
         const exprt &this_arg=call.arguments().front();
-        assert(this_arg.type().id()==ID_pointer);
+        INVARIANT(this_arg.type().id()==ID_pointer,
+                  "first argument must be a pointer");
       }
 
       // do some type adjustment for the arguments,
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index 1b424291a5c..3f330271ca2 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -635,7 +635,7 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
     size_t flags=(field.is_public?1:0)+
       (field.is_protected?1:0)+
       (field.is_private?1:0);
-    assert(flags<=1);
+    DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
 
     for(std::size_t j=0; j<attributes_count; j++)
       rfield_attribute(field);
@@ -1361,7 +1361,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
   size_t flags=(method.is_public?1:0)+
     (method.is_protected?1:0)+
     (method.is_private?1:0);
-  assert(flags<=1);
+  DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
   u2 attributes_count=read_u2();
 
   for(std::size_t j=0; j<attributes_count; j++)
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 58e0fa1312a..40dd0cd520b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -369,8 +369,9 @@ void value_sett::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
   }
@@ -380,10 +381,11 @@ void value_sett::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     const std::string &component_name=
       expr.get_string(ID_component_name);
@@ -1360,7 +1362,8 @@ void value_sett::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array || type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, true);
   }
@@ -1373,10 +1376,11 @@ void value_sett::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(
       lhs.op0(), values_rhs, "."+component_name+suffix, ns, add_to_sets);
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index c18ae55eb70..8b38d975d0d 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -412,9 +412,10 @@ void value_set_fit::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix,
                       original_type, ns, recursion_set);
@@ -429,10 +430,11 @@ void value_set_fit::get_value_set_rec(
     {
       const typet &type=ns.follow(expr.op0().type());
 
-      assert(type.id()==ID_struct ||
-             type.id()==ID_union ||
-             type.id()==ID_incomplete_struct ||
-             type.id()==ID_incomplete_union);
+      DATA_INVARIANT(type.id()==ID_struct ||
+                     type.id()==ID_union ||
+                     type.id()==ID_incomplete_struct ||
+                     type.id()==ID_incomplete_union,
+                     "operand 0 of member expression must be struct or union");
 
       const std::string &component_name=
         expr.get_string(ID_component_name);
@@ -1290,9 +1292,10 @@ void value_set_fit::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set);
   }
@@ -1308,10 +1311,11 @@ void value_set_fit::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
                ns, recursion_set);
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index cbe0a652fb8..b3c5a53726c 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -525,9 +525,10 @@ void value_set_fivrt::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix,
                       original_type, ns, recursion_set);
@@ -542,10 +543,11 @@ void value_set_fivrt::get_value_set_rec(
     {
       const typet &type=ns.follow(expr.op0().type());
 
-      assert(type.id()==ID_struct ||
-             type.id()==ID_union ||
-             type.id()==ID_incomplete_struct ||
-             type.id()==ID_incomplete_union);
+      DATA_INVARIANT(type.id()==ID_struct ||
+                     type.id()==ID_union ||
+                     type.id()==ID_incomplete_struct ||
+                     type.id()==ID_incomplete_union,
+                     "operand 0 of member expression must be struct or union");
 
       const std::string &component_name=
         expr.get_string(ID_component_name);
@@ -1427,9 +1429,10 @@ void value_set_fivrt::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     assign_rec(
       lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set, add_to_sets);
@@ -1446,10 +1449,11 @@ void value_set_fivrt::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
                ns, recursion_set, add_to_sets);
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 7f05d584fdc..ae7ec38a526 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -316,8 +316,9 @@ void value_set_fivrnst::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
 
@@ -331,10 +332,11 @@ void value_set_fivrnst::get_value_set_rec(
     {
       const typet &type=ns.follow(expr.op0().type());
 
-      assert(type.id()==ID_struct ||
-             type.id()==ID_union ||
-             type.id()==ID_incomplete_struct ||
-             type.id()==ID_incomplete_union);
+      DATA_INVARIANT(type.id()==ID_struct ||
+                     type.id()==ID_union ||
+                     type.id()==ID_incomplete_struct ||
+                     type.id()==ID_incomplete_union,
+                     "operand 0 of member expression must be struct or union");
 
       const std::string &component_name=
         expr.get_string(ID_component_name);
@@ -1081,7 +1083,8 @@ void value_set_fivrnst::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array || type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, add_to_sets);
   }
@@ -1097,10 +1100,11 @@ void value_set_fivrnst::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
                ns, add_to_sets);
diff --git a/src/solvers/cvc/cvc_dec.cpp b/src/solvers/cvc/cvc_dec.cpp
index cdb83e67afa..a5fecd8a991 100644
--- a/src/solvers/cvc/cvc_dec.cpp
+++ b/src/solvers/cvc/cvc_dec.cpp
@@ -63,7 +63,7 @@ decision_proceduret::resultt cvc_dect::dec_solve()
     "cvcl "+temp_out_filename+" > "+temp_result_filename+" 2>&1";
 
   int res=system(command.c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   status() << "Reading result from CVCL" << eom;
 
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 5446a0498cf..1ffcd8d91b7 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -31,7 +31,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   else if(expr.id()==ID_byte_update_big_endian)
     little_endian=false;
   else
-    assert(false);
+    UNREACHABLE;
 
   bvt bv=convert_bv(op);
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index cf5ebfdb243..d0c61e8ae86 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -581,7 +581,7 @@ exprt bv_pointerst::bv_get_rec(
        case tvt::tv_enumt::TV_FALSE: ch='0'; break;
        case tvt::tv_enumt::TV_TRUE:  ch='1'; break;
        case tvt::tv_enumt::TV_UNKNOWN: ch='0'; break;
-       default: assert(false);
+       default: UNREACHABLE;
       }
     }
 
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index cff775d6597..1d729070c12 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -385,7 +385,7 @@ literalt bv_utilst::overflow_add(
     return carry_out(op0, op1, const_literal(false));
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 literalt bv_utilst::overflow_sub(
@@ -410,7 +410,7 @@ literalt bv_utilst::overflow_sub(
     return !carry_out(op0, inverted(op1), const_literal(true));
   }
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 void bv_utilst::adder_no_overflow(
@@ -797,7 +797,7 @@ bvt bv_utilst::multiplier(
   {
   case representationt::SIGNED: return signed_multiplier(op0, op1);
   case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
-  default: assert(false);
+  default: UNREACHABLE;
   }
 }
 
@@ -812,7 +812,7 @@ bvt bv_utilst::multiplier_no_overflow(
     return signed_multiplier_no_overflow(op0, op1);
   case representationt::UNSIGNED:
     return unsigned_multiplier_no_overflow(op0, op1);
-  default: assert(false);
+  default: UNREACHABLE;
   }
 }
 
@@ -1278,7 +1278,7 @@ literalt bv_utilst::rel(
   else if(id==ID_gt)
     return lt_or_le(false, bv1, bv0, rep); // swapped
   else
-    assert(false);
+    UNREACHABLE;
 }
 
 bool bv_utilst::is_constant(const bvt &bv)
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index 1d431c083c4..34d166044e8 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -202,7 +202,7 @@ exprt flatten_byte_extract(
   else if(src.id()==ID_byte_extract_big_endian)
     little_endian=false;
   else
-    assert(false);
+    UNREACHABLE;
 
   // determine an upper bound of the number of bytes we might need
   exprt upper_bound=size_of_expr(src.type(), ns);
@@ -292,7 +292,8 @@ exprt flatten_byte_extract(
   const array_typet &array_type=to_array_type(root.type());
   const typet &subtype=array_type.subtype();
 
-  assert(pointer_offset_bits(subtype, ns)==8);
+  DATA_INVARIANT(pointer_offset_bits(subtype, ns)==8,
+                 "offset bits are byte aligned");
 
   mp_integer size_bits=pointer_offset_bits(unpacked.type(), ns);
   if(size_bits<0)
diff --git a/src/solvers/prop/minimize.cpp b/src/solvers/prop/minimize.cpp
index c28ab411bf3..8f5dfeff36e 100644
--- a/src/solvers/prop/minimize.cpp
+++ b/src/solvers/prop/minimize.cpp
@@ -54,7 +54,7 @@ void prop_minimizet::fix_objectives()
     }
   }
 
-  assert(found);
+  POSTCONDITION(found);
 }
 
 /// Build constraints that require us to improve on at least one goal, greedily.
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
index ab187e20ada..8f605c0b9f1 100644
--- a/src/solvers/qbf/qbf_quantor.cpp
+++ b/src/solvers/qbf/qbf_quantor.cpp
@@ -53,7 +53,7 @@ propt::resultt qbf_quantort::prop_solve()
   // solve it
   int res=system((
     "quantor "+qbf_tmp_file+" -o "+result_tmp_file).c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
index 9953fbc922b..37ad3374705 100644
--- a/src/solvers/qbf/qbf_qube.cpp
+++ b/src/solvers/qbf/qbf_qube.cpp
@@ -61,7 +61,7 @@ propt::resultt qbf_qubet::prop_solve()
   // solve it
   int res=system(
     ("QuBE "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index e14dda75f60..877a5a27a85 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -56,7 +56,7 @@ propt::resultt qbf_qube_coret::prop_solve()
   // solve it
   int res=system((
     "QuBE "+options+" "+qbf_tmp_file+" > "+result_tmp_file).c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
index 55813caf564..d8fb7e59f31 100644
--- a/src/solvers/qbf/qbf_skizzo.cpp
+++ b/src/solvers/qbf/qbf_skizzo.cpp
@@ -61,7 +61,7 @@ propt::resultt qbf_skizzot::prop_solve()
   // solve it
   int res=system((
     "sKizzo "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index c5cd3991c53..b439577c270 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -106,7 +106,7 @@ bool pbs_dimacs_cnft::pbs_solve()
   command += " -a > temp.out";
 
   int res=system(command.c_str());
-  assert(0==res);
+  CHECK_RETURN(0==res);
 
   std::ifstream file("temp.out");
   std::string line;
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index a362435e91a..745f6e57826 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4246,7 +4246,7 @@ void smt2_convt::find_symbols(const exprt &expr)
 bool smt2_convt::use_array_theory(const exprt &expr)
 {
   const typet &type=ns.follow(expr.type());
-  assert(type.id()==ID_array);
+  PRECONDITION(type.id()==ID_array);
   // const array_typet &array_type=to_array_type(ns.follow(expr.type()));
 
   if(use_datatypes)
diff --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp
index 50e0f537fa5..abded937922 100644
--- a/src/util/irep_ids.cpp
+++ b/src/util/irep_ids.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "irep_ids.h"
 
-#include <cassert>
+#include "invariant.h"
 
 #include "string_container.h"
 
@@ -51,6 +51,6 @@ void initialize_string_container()
   {
     unsigned x;
     x=string_container[irep_ids_table[i]];
-    assert(x==i); // sanity check
+    INVARIANT(x==i, "i-th element is inserted at position i"); // sanity check
   }
 }
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 84df9d7a3ad..17dc6fd9577 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -170,7 +170,7 @@ static bool build_graph(
   {
     const graphmlt::nodet &n=dest[i];
 
-    assert(!n.node_name.empty());
+    INVARIANT(!n.node_name.empty(), "node should be named");
   }
 
   assert(!entrynode.empty());