diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
index eaf884db60e..1efad8a920b 100644
--- a/jbmc/src/jbmc/Makefile
+++ b/jbmc/src/jbmc/Makefile
@@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index d3ad7b6f9bd..b9f7201d2dd 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -1,6 +1,5 @@
 SRC = all_properties.cpp \
       bmc.cpp \
-      bmc_cover.cpp \
       c_test_input_generator.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index bf2129d367b..5e3360ee09a 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -131,12 +131,6 @@ safety_checkert::resultt bmct::execute(
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
-    if(!options.get_list_option("cover").empty())
-    {
-      return cover(goto_functions)?
-        safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
-    }
-
     // any properties to check at all?
     if(
       !options.get_bool_option("program-only") &&
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index f92f2ff86c3..851f2a6566d 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -191,12 +191,7 @@ class bmct:public safety_checkert
   virtual resultt all_properties(const goto_functionst &goto_functions);
   virtual resultt stop_on_fail();
 
-  bool cover(const goto_functionst &goto_functions);
-
   friend class bmc_all_propertiest;
-  friend class bmc_covert;
-  template <template <class goalt> class covert>
-  friend class bmc_goal_covert;
 
 private:
   /// \brief Class-specific symbolic execution
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
deleted file mode 100644
index d6c5537c20a..00000000000
--- a/src/cbmc/bmc_cover.cpp
+++ /dev/null
@@ -1,437 +0,0 @@
-/*******************************************************************\
-
-Module: Test-Suite Generation with BMC
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Test-Suite Generation with BMC
-
-#include "bmc.h"
-
-#include <chrono>
-#include <iomanip>
-
-#include <goto-checker/bmc_util.h>
-
-#include <util/json.h>
-#include <util/json_stream.h>
-#include <util/xml_irep.h>
-
-#include <solvers/prop/cover_goals.h>
-#include <solvers/prop/prop_conv.h>
-
-#include <goto-symex/build_goto_trace.h>
-
-#include <goto-programs/json_expr.h>
-#include <goto-programs/json_goto_trace.h>
-#include <goto-programs/xml_expr.h>
-#include <goto-programs/xml_goto_trace.h>
-
-#include <langapi/language_util.h>
-
-class bmc_covert:
-  public cover_goalst::observert,
-  public messaget
-{
-public:
-  bmc_covert(
-    const goto_functionst &_goto_functions,
-    bmct &_bmc):
-    goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc)
-  {
-  }
-
-  bool operator()();
-
-  // gets called by prop_covert
-  virtual void satisfying_assignment();
-
-  struct goalt
-  {
-    // a criterion is satisfied if _any_ instance is true
-    struct instancet
-    {
-      symex_target_equationt::SSA_stepst::iterator step;
-      literalt condition;
-    };
-
-    typedef std::vector<instancet> instancest;
-    instancest instances;
-
-    void add_instance(
-      symex_target_equationt::SSA_stepst::iterator step,
-      literalt condition)
-    {
-      instances.push_back(instancet());
-      instances.back().step=step;
-      instances.back().condition=condition;
-    }
-
-    std::string description;
-    source_locationt source_location;
-
-    // if satisfied, we compute a goto_trace
-    bool satisfied;
-
-    goalt(
-      const std::string &_description,
-      const source_locationt &_source_location):
-      description(_description),
-      source_location(_source_location),
-      satisfied(false)
-    {
-    }
-
-    goalt():source_location(source_locationt::nil()),
-            satisfied(false)
-    {
-    }
-
-    exprt as_expr() const
-    {
-      std::vector<exprt> tmp;
-
-      for(const auto &goal_inst : instances)
-        tmp.push_back(literal_exprt(goal_inst.condition));
-
-      return disjunction(tmp);
-    }
-  };
-
-  struct testt
-  {
-    goto_tracet goto_trace;
-    std::vector<irep_idt> covered_goals;
-  };
-
-  inline irep_idt id(goto_programt::const_targett loc)
-  {
-    return loc->source_location.get_property_id();
-  }
-
-  typedef std::map<irep_idt, goalt> goal_mapt;
-  goal_mapt goal_map;
-  typedef std::vector<testt> testst;
-  testst tests;
-
-  std::string get_test(const goto_tracet &goto_trace) const
-  {
-    bool first=true;
-    std::string test;
-    for(const auto &step : goto_trace.steps)
-    {
-      if(step.is_input())
-      {
-        if(first)
-          first=false;
-        else
-          test+=", ";
-
-        test+=id2string(step.io_id)+"=";
-
-        if(step.io_args.size()==1)
-          test+=from_expr(bmc.ns, "", step.io_args.front());
-      }
-    }
-    return test;
-  }
-
-protected:
-  const goto_functionst &goto_functions;
-  prop_convt &solver;
-  bmct &bmc;
-};
-
-static bool is_failed_assumption_step(
-  symex_target_equationt::SSA_stepst::const_iterator step,
-  const prop_convt &prop_conv)
-{
-  return step->is_assume() && prop_conv.l_get(step->cond_literal).is_false();
-}
-
-void bmc_covert::satisfying_assignment()
-{
-  tests.push_back(testt());
-  testt &test = tests.back();
-
-  for(auto &goal_pair : goal_map)
-  {
-    goalt &g=goal_pair.second;
-
-    // covered already?
-    if(g.satisfied)
-      continue;
-
-    // check whether satisfied
-    for(const auto &goal_inst : g.instances)
-    {
-      literalt cond=goal_inst.condition;
-
-      if(solver.l_get(cond).is_true())
-      {
-        status() << "Covered function " << g.source_location.get_function()
-                 << " " << g.description << messaget::eom;
-        g.satisfied=true;
-        test.covered_goals.push_back(goal_pair.first);
-        break;
-      }
-    }
-  }
-
-  build_goto_trace(
-    bmc.equation, is_failed_assumption_step, solver, bmc.ns, test.goto_trace);
-}
-
-bool bmc_covert::operator()()
-{
-  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
-
-  solver.set_message_handler(get_message_handler());
-
-  auto solver_start=std::chrono::steady_clock::now();
-
-  // Collect _all_ goals in `goal_map'.
-  // This maps property IDs to 'goalt'
-  forall_goto_functions(f_it, goto_functions)
-  {
-    forall_goto_program_instructions(i_it, f_it->second.body)
-    {
-      if(i_it->is_assert())
-        goal_map[id(i_it)]=
-          goalt(
-            id2string(i_it->source_location.get_comment()),
-            i_it->source_location);
-    }
-  }
-
-  for(auto &step : bmc.equation.SSA_steps)
-    step.cond_literal=literalt(0, 0);
-
-  // Do conversion to next solver layer
-
-  convert_symex_target_equation(
-    bmc.equation, bmc.prop_conv, get_message_handler());
-  bmc.freeze_program_variables();
-
-  // get the conditions for these goals from formula
-  // collect all 'instances' of the goals
-  for(auto it = bmc.equation.SSA_steps.begin();
-      it!=bmc.equation.SSA_steps.end();
-      it++)
-  {
-    if(it->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);
-      goal_map[id(it->source.pc)].add_instance(it, l_c);
-    }
-  }
-
-  status() << "Aiming to cover " << goal_map.size() << " goal(s)" << eom;
-
-  cover_goalst cover_goals(solver);
-
-  cover_goals.register_observer(*this);
-
-  for(const auto &g : goal_map)
-  {
-    literalt l=solver.convert(g.second.as_expr());
-    cover_goals.add(l);
-  }
-
-  INVARIANT(cover_goals.size() == goal_map.size(),
-    "we add coverage for each goal");
-
-
-  status() << "Running " << solver.decision_procedure_text() << eom;
-
-  cover_goals(get_message_handler());
-
-  {
-    auto solver_stop=std::chrono::steady_clock::now();
-    status() << "Runtime decision procedure: "
-             << std::chrono::duration<double>(solver_stop-solver_start).count()
-             << "s" << eom;
-  }
-
-  // report
-  unsigned goals_covered=0;
-
-  for(const auto &g : goal_map)
-    if(g.second.satisfied)
-      goals_covered++;
-
-  switch(bmc.ui_message_handler.get_ui())
-  {
-    case ui_message_handlert::uit::PLAIN:
-    {
-      result() << "\n** coverage results:" << eom;
-
-      for(const auto &g : goal_map)
-      {
-        const goalt &goal=g.second;
-
-        result() << "[" << g.first << "]";
-
-        if(goal.source_location.is_not_nil())
-          result() << ' ' << goal.source_location;
-
-        if(!goal.description.empty())
-          result() << ' ' << goal.description;
-
-        result() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
-                 << '\n';
-      }
-
-      result() << eom;
-      break;
-    }
-
-    case ui_message_handlert::uit::XML_UI:
-    {
-      for(const auto &goal_pair : goal_map)
-      {
-        const goalt &goal=goal_pair.second;
-
-        xmlt xml_result(
-          "goal",
-          {{"id", id2string(goal_pair.first)},
-           {"description", goal.description},
-           {"status", goal.satisfied ? "SATISFIED" : "FAILED"}},
-          {});
-
-        if(goal.source_location.is_not_nil())
-          xml_result.new_element()=xml(goal.source_location);
-
-        result() << xml_result;
-      }
-
-      for(const auto &test : tests)
-      {
-        xmlt xml_result("test");
-        if(bmc.options.get_bool_option("trace"))
-        {
-          convert(bmc.ns, test.goto_trace, xml_result.new_element());
-        }
-        else
-        {
-          xmlt &xml_test=xml_result.new_element("inputs");
-
-          for(const auto &step : test.goto_trace.steps)
-          {
-            if(step.is_input())
-            {
-              xmlt &xml_input=xml_test.new_element("input");
-              xml_input.set_attribute("id", id2string(step.io_id));
-              if(step.io_args.size()==1)
-                xml_input.new_element("value")=
-                  xml(step.io_args.front(), bmc.ns);
-            }
-          }
-        }
-
-        for(const auto &goal_id : test.covered_goals)
-        {
-          xmlt &xml_goal=xml_result.new_element("goal");
-          xml_goal.set_attribute("id", id2string(goal_id));
-        }
-
-        result() << xml_result;
-      }
-      break;
-    }
-
-    case ui_message_handlert::uit::JSON_UI:
-    {
-      if(status().tellp() > 0)
-        status() << eom; // force end of previous message
-      json_stream_objectt &json_result =
-        bmc.ui_message_handler.get_json_stream().push_back_stream_object();
-      for(const auto &goal_pair : goal_map)
-      {
-        const goalt &goal=goal_pair.second;
-
-        json_result["status"] =
-          json_stringt(goal.satisfied ? "satisfied" : "failed");
-        json_result["goal"] = json_stringt(goal_pair.first);
-        json_result["description"] = json_stringt(goal.description);
-
-        if(goal.source_location.is_not_nil())
-          json_result["sourceLocation"] = json(goal.source_location);
-      }
-      json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
-      json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
-
-      json_arrayt &tests_array=json_result["tests"].make_array();
-      for(const auto &test : tests)
-      {
-        if(bmc.options.get_bool_option("trace"))
-        {
-          json_arrayt &json_trace = json_result["trace"].make_array();
-          convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
-        }
-        else
-        {
-          json_arrayt &json_test = json_result["inputs"].make_array();
-
-          for(const auto &step : test.goto_trace.steps)
-          {
-            if(step.is_input())
-            {
-              json_objectt json_input{{"id", json_stringt(step.io_id)}};
-              if(step.io_args.size()==1)
-                json_input["value"]=
-                  json(step.io_args.front(), bmc.ns, ID_unknown);
-              json_test.push_back(std::move(json_input));
-            }
-          }
-        }
-        json_arrayt goal_refs;
-        for(const auto &goal_id : test.covered_goals)
-        {
-          goal_refs.push_back(json_stringt(goal_id));
-        }
-        tests_array.push_back(
-          json_objectt({{"coveredGoals", std::move(goal_refs)}}));
-      }
-
-      break;
-    }
-  }
-
-  status() << "** " << goals_covered
-           << " of " << goal_map.size() << " covered ("
-           << std::fixed << std::setw(1) << std::setprecision(1)
-           << (goal_map.empty()?100.0:100.0*goals_covered/goal_map.size())
-           << "%)" << eom;
-
-  statistics() << "** Used "
-               << cover_goals.iterations() << " iteration"
-               << (cover_goals.iterations()==1?"":"s")
-               << eom;
-
-  if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
-  {
-    result() << "Test suite:" << '\n';
-
-    for(const auto &test : tests)
-      result() << get_test(test.goto_trace) << '\n';
-
-    result() << eom;
-  }
-
-  return false;
-}
-
-/// Try to cover all goals
-bool bmct::cover(const goto_functionst &goto_functions)
-{
-  bmc_covert bmc_cover(goto_functions, *this);
-  bmc_cover.set_message_handler(get_message_handler());
-  return bmc_cover();
-}
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 964842fc180..1b868cdce13 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -46,24 +46,24 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/validate_goto_model.h>
 #include <goto-programs/write_goto_binary.h>
 
-#include <pointer-analysis/value_set_analysis.h>
-#include <pointer-analysis/goto_program_dereference.h>
 #include <pointer-analysis/add_failed_symbols.h>
+#include <pointer-analysis/goto_program_dereference.h>
 #include <pointer-analysis/show_value_sets.h>
+#include <pointer-analysis/value_set_analysis.h>
 
-#include <analyses/natural_loops.h>
-#include <analyses/global_may_alias.h>
-#include <analyses/local_bitvector_analysis.h>
+#include <analyses/call_graph.h>
+#include <analyses/constant_propagator.h>
 #include <analyses/custom_bitvector_analysis.h>
+#include <analyses/dependence_graph.h>
 #include <analyses/escape_analysis.h>
-#include <analyses/call_graph.h>
+#include <analyses/global_may_alias.h>
 #include <analyses/interval_analysis.h>
 #include <analyses/interval_domain.h>
-#include <analyses/reaching_definitions.h>
-#include <analyses/dependence_graph.h>
-#include <analyses/constant_propagator.h>
 #include <analyses/is_threaded.h>
+#include <analyses/local_bitvector_analysis.h>
 #include <analyses/local_safe_pointers.h>
+#include <analyses/natural_loops.h>
+#include <analyses/reaching_definitions.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
diff --git a/unit/Makefile b/unit/Makefile
index 88da640103e..19ed3d747ff 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -98,7 +98,6 @@ testing-utils-clean:
 # We need to link bmc.o to the unit test, so here's everything it depends on...
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
-          ../src/cbmc/bmc_cover$(OBJEXT) \
           ../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \