diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index fd0d43313e2..c4d7245b455 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -227,7 +227,7 @@ bool bmc_covert::operator()()
   {
     if(it->is_assert())
     {
-      assert(it->source.pc->is_assert());
+      PRECONDITION(it->source.pc->is_assert());
       const and_exprt c(
         literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal));
       literalt l_c=solver.convert(c);
@@ -247,7 +247,8 @@ bool bmc_covert::operator()()
     cover_goals.add(l);
   }
 
-  assert(cover_goals.size()==goal_map.size());
+  INVARIANT(cover_goals.size()==goal_map.size(),
+    "We add coverage for each goal");
 
   status() << "Running " << solver.decision_procedure_text() << eom;
 
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 8b216839f92..4a4ed7e15ec 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -34,7 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \return An smt2_dect::solvert giving the solver to use.
 smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
 {
-  assert(options.get_bool_option("smt2"));
+  // we shouldn't get here if this option isn't set
+  PRECONDITION(options.get_bool_option("smt2"));
 
   smt2_dect::solvert s=smt2_dect::solvert::GENERIC;
 
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index 66df55eca87..5572d8d11c1 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -71,13 +71,13 @@ class cbmc_solverst:public messaget
 
     prop_convt &prop_conv() const
     {
-      assert(prop_conv_ptr!=nullptr);
+      PRECONDITION(prop_conv_ptr!=nullptr);
       return *prop_conv_ptr;
     }
 
     propt &prop() const
     {
-      assert(prop_ptr!=nullptr);
+      PRECONDITION(prop_ptr!=nullptr);
       return *prop_ptr;
     }
 
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index c150a962912..d97469bad18 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -81,7 +81,7 @@ fault_localizationt::get_failed_property()
 bool fault_localizationt::check(const lpointst &lpoints,
                                 const lpoints_valuet &value)
 {
-  assert(value.size()==lpoints.size());
+  PRECONDITION(value.size()==lpoints.size());
   bvt assumptions;
   lpoints_valuet::const_iterator v_it=value.begin();
   for(const auto &l : lpoints)
@@ -142,7 +142,7 @@ void fault_localizationt::run(irep_idt goal_id)
 {
   // find failed property
   failed=get_failed_property();
-  assert(failed!=bmc.equation.SSA_steps.end());
+  PRECONDITION(failed!=bmc.equation.SSA_steps.end());
 
   if(goal_id==ID_nil)
     goal_id=failed->source.pc->source_location.get_property_id();
diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index ddef86378d9..82d653d0cf4 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -139,15 +139,17 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   const symex_coveraget::coveraget &coverage):
   coverage_recordt("method")
 {
-  assert(gf_it->second.body_available());
+  PRECONDITION(gf_it->second.body_available());
 
   // identify the file name, inlined functions aren't properly
   // accounted for
   goto_programt::const_targett end_function=
     --gf_it->second.body.instructions.end();
-  assert(end_function->is_end_function());
+  INVARIANT(end_function->is_end_function(),
+    "Last instruction in a function body is end function");
   file_name=end_function->source_location.get_file();
-  assert(!file_name.empty());
+  INVARIANT(!file_name.empty(),
+    "Should have a valid source location");
 
   // compute the maximum coverage of individual source-code lines
   coverage_lines_mapt coverage_lines_map;
@@ -260,11 +262,14 @@ void goto_program_coverage_recordt::compute_coverage_lines(
         for(const auto &cov : c_entry->second)
           std::cerr << cov.second.succ->location_number << '\n';
       }
-      assert(c_entry->second.size()==1 || is_branch);
+      INVARIANT(c_entry->second.size()==1 || is_branch,
+        "Instructions other than branch instructions have exactly 1 successor");
 
       for(const auto &cov : c_entry->second)
       {
-        assert(cov.second.num_executions>0);
+        INVARIANT(cov.second.num_executions>0,
+          // FIXME I don't know what this means
+          "Number of executions most be positive");
 
         if(entry.first->second.hits==0)
           ++lines_covered;
@@ -275,7 +280,8 @@ void goto_program_coverage_recordt::compute_coverage_lines(
         if(is_branch)
         {
           auto cond_entry=entry.first->second.conditions.find(it);
-          assert(cond_entry!=entry.first->second.conditions.end());
+          INVARIANT(cond_entry!=entry.first->second.conditions.end(),
+            "Branch should have condition");
 
           if(it->get_target()==cov.second.succ)
           {
@@ -439,7 +445,7 @@ bool symex_coveraget::generate_report(
   const goto_functionst &goto_functions,
   const std::string &path) const
 {
-  assert(!path.empty());
+  PRECONDITION(!path.empty());
 
   if(path=="-")
     return output_report(goto_functions, std::cout);