diff --git a/.gitignore b/.gitignore
index c10ff2decde..7cbe1dcb4dd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -96,6 +96,8 @@ src/memory-models/mm_y.tab.h
 # binaries
 src/cbmc/cbmc
 src/cbmc/cbmc.exe
+src/ccover/ccover
+src/ccover/ccover.exe
 src/goto-analyzer/goto-analyzer
 src/goto-analyzer/goto-analyzer.exe
 src/goto-cc/goto-cc
diff --git a/CMakeLists.txt b/CMakeLists.txt
index fea650dbac1..8e844c398ce 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -52,6 +52,8 @@ set_target_properties(
     big-int
     cbmc
     cbmc-lib
+    ccover
+    ccover-lib
     cpp
     driver
     goto-analyzer
diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
index ab8c2c962aa..32a1b8d4681 100644
--- a/jbmc/src/jbmc/Makefile
+++ b/jbmc/src/jbmc/Makefile
@@ -40,7 +40,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) \
       ../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index a4474d1edd5..8173c707693 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -121,9 +121,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);
 
-  if(cmdline.isset("cover"))
-    parse_cover_options(cmdline, options);
-
   if(cmdline.isset("nondet-static"))
     options.set_option("nondet-static", true);
 
@@ -189,14 +186,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("assumptions", false);
 
   // generate unwinding assertions
-  if(cmdline.isset("cover"))
-    options.set_option("unwinding-assertions", false);
-  else
-  {
-    options.set_option(
-      "unwinding-assertions",
-      cmdline.isset("unwinding-assertions"));
-  }
+  options.set_option(
+    "unwinding-assertions",
+    cmdline.isset("unwinding-assertions"));
 
   // generate unwinding assumptions otherwise
   options.set_option(
@@ -916,17 +908,9 @@ bool jbmc_parse_optionst::process_goto_functions(
       remove_unused_functions(goto_model, get_message_handler());
     }
 
-    // remove skips such that trivial GOTOs are deleted and not considered
-    // for coverage annotation:
+    // remove skips such that trivial GOTOs are deleted
     remove_skip(goto_model);
 
-    // instrument cover goals
-    if(cmdline.isset("cover"))
-    {
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
-        return true;
-    }
-
     // label the assertions
     // This must be done after adding assertions and
     // before using the argument of the "property" option.
@@ -970,7 +954,7 @@ bool jbmc_parse_optionst::process_goto_functions(
         full_slicer(goto_model);
     }
 
-    // remove any skips introduced since coverage instrumentation
+    // remove any skips
     remove_skip(goto_model);
   }
 
@@ -1079,7 +1063,6 @@ void jbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile
index 486a8c750f7..f2c4e334c5a 100644
--- a/regression/cbmc-cover/Makefile
+++ b/regression/cbmc-cover/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/ccover/ccover
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc
+	@../test.pl -p -c ../../../src/ccover/ccover
 
 show:
 	@for dir in *; do \
diff --git a/regression/ccover/Makefile b/regression/ccover/Makefile
new file mode 100644
index 00000000000..6ecfb9d1c97
--- /dev/null
+++ b/regression/ccover/Makefile
@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/ccover/ccover -X smt-backend
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/ccover/ccover -X smt-backend
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/cbmc/pointer-function-parameters-2/main.c b/regression/ccover/pointer-function-parameters-2/main.c
similarity index 100%
rename from regression/cbmc/pointer-function-parameters-2/main.c
rename to regression/ccover/pointer-function-parameters-2/main.c
diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/ccover/pointer-function-parameters-2/test.desc
similarity index 100%
rename from regression/cbmc/pointer-function-parameters-2/test.desc
rename to regression/ccover/pointer-function-parameters-2/test.desc
diff --git a/regression/cbmc/pointer-function-parameters/main.c b/regression/ccover/pointer-function-parameters/main.c
similarity index 100%
rename from regression/cbmc/pointer-function-parameters/main.c
rename to regression/ccover/pointer-function-parameters/main.c
diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/ccover/pointer-function-parameters/test.desc
similarity index 100%
rename from regression/cbmc/pointer-function-parameters/test.desc
rename to regression/ccover/pointer-function-parameters/test.desc
diff --git a/regression/cbmc/reachability-slice/test.c b/regression/ccover/reachability-slice/test.c
similarity index 100%
rename from regression/cbmc/reachability-slice/test.c
rename to regression/ccover/reachability-slice/test.c
diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/ccover/reachability-slice/test.desc
similarity index 100%
rename from regression/cbmc/reachability-slice/test.desc
rename to regression/ccover/reachability-slice/test.desc
diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/ccover/reachability-slice/test2.desc
similarity index 100%
rename from regression/cbmc/reachability-slice/test2.desc
rename to regression/ccover/reachability-slice/test2.desc
diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/ccover/reachability-slice/test3.desc
similarity index 100%
rename from regression/cbmc/reachability-slice/test3.desc
rename to regression/ccover/reachability-slice/test3.desc
diff --git a/regression/cbmc/simple_assert/main.c b/regression/ccover/simple_assert/main.c
similarity index 100%
rename from regression/cbmc/simple_assert/main.c
rename to regression/ccover/simple_assert/main.c
diff --git a/regression/cbmc/simple_assert/test.desc b/regression/ccover/simple_assert/test.desc
similarity index 100%
rename from regression/cbmc/simple_assert/test.desc
rename to regression/ccover/simple_assert/test.desc
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4022889e456..6111649f6de 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -97,6 +97,7 @@ add_subdirectory(util)
 add_subdirectory(xmllang)
 
 add_subdirectory(cbmc)
+add_subdirectory(ccover)
 add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)
diff --git a/src/Makefile b/src/Makefile
index a75535d49bc..beffa777260 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -3,6 +3,7 @@ DIRS = analyses \
        assembler \
        big-int \
        cbmc \
+       ccover \
        cpp \
        goto-analyzer \
        goto-cc \
@@ -21,6 +22,7 @@ DIRS = analyses \
        # Empty last line
 
 all: cbmc.dir \
+     ccover.dir \
      goto-analyzer.dir \
      goto-cc.dir \
      goto-diff.dir \
@@ -53,6 +55,8 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
           goto-instrument.dir
 
+ccover.dir: cbmc.dir
+
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir
 
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index e1045b7bc9c..78d57081039 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -1,6 +1,5 @@
 SRC = all_properties.cpp \
       bmc.cpp \
-      bmc_cover.cpp \
       bv_cbmc.cpp \
       cbmc_dimacs.cpp \
       cbmc_languages.cpp \
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 0fbc50aaa15..2b096a33135 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -380,12 +380,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;
-    }
-
     if(options.get_option("localize-faults")!="")
     {
       fault_localizationt fault_localization(
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 8e812e8e1da..1068e5ff066 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -223,12 +223,7 @@ class bmct:public safety_checkert
   void slice();
   void show();
 
-  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;
   friend class fault_localizationt;
 
 private:
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 964b64410f2..e8c6d48d76b 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -57,7 +57,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
-#include <goto-instrument/cover.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -151,9 +150,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-vcc"))
     options.set_option("show-vcc", true);
 
-  if(cmdline.isset("cover"))
-    parse_cover_options(cmdline, options);
-
   if(cmdline.isset("mm"))
     options.set_option("mm", cmdline.get_value("mm"));
 
@@ -786,13 +782,6 @@ bool cbmc_parse_optionst::process_goto_program(
     // for coverage annotation:
     remove_skip(goto_model);
 
-    // instrument cover goals
-    if(options.is_set("cover"))
-    {
-      if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
-        return true;
-    }
-
     // label the assertions
     // This must be done after adding assertions and
     // before using the argument of the "property" option.
@@ -831,7 +820,7 @@ bool cbmc_parse_optionst::process_goto_program(
         full_slicer(goto_model);
     }
 
-    // remove any skips introduced since coverage instrumentation
+    // remove any skips
     remove_skip(goto_model);
   }
 
@@ -937,7 +926,6 @@ void cbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index d36f976573a..d5defff73cf 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -62,7 +62,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):(symex-coverage-report):" \
+  "(symex-coverage-report):" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
diff --git a/src/ccover/CMakeLists.txt b/src/ccover/CMakeLists.txt
new file mode 100644
index 00000000000..b77ceee6ae9
--- /dev/null
+++ b/src/ccover/CMakeLists.txt
@@ -0,0 +1,35 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/ccover_main.cpp
+)
+add_library(ccover-lib ${sources})
+
+generic_includes(ccover-lib)
+
+target_link_libraries(ccover-lib
+    analyses
+    ansi-c
+    assembler
+    big-int
+    cbmc-lib
+    cpp
+    goto-instrument-lib
+    goto-programs
+    goto-symex
+    java_bytecode
+    json
+    langapi
+    linking
+    pointer-analysis
+    solvers
+    util
+    xml
+)
+
+add_if_library(ccover-lib bv_refinement)
+add_if_library(ccover-lib jsil)
+
+# Executable
+add_executable(ccover ccover_main.cpp)
+target_link_libraries(ccover ccover-lib)
diff --git a/src/ccover/Makefile b/src/ccover/Makefile
new file mode 100644
index 00000000000..2c70274ca19
--- /dev/null
+++ b/src/ccover/Makefile
@@ -0,0 +1,76 @@
+SRC = ccover_bmc.cpp \
+      bmc_cover.cpp \
+      ccover_main.cpp \
+      ccover_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+       ../cpp/cpp$(LIBEXT) \
+       ../linking/linking$(LIBEXT) \
+       ../big-int/big-int$(LIBEXT) \
+       ../goto-programs/goto-programs$(LIBEXT) \
+       ../goto-symex/goto-symex$(LIBEXT) \
+       ../pointer-analysis/value_set$(OBJEXT) \
+       ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_domain_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_fi$(OBJEXT) \
+       ../pointer-analysis/value_set_dereference$(OBJEXT) \
+       ../pointer-analysis/dereference_callback$(OBJEXT) \
+       ../pointer-analysis/add_failed_symbols$(OBJEXT) \
+       ../pointer-analysis/rewrite_index$(OBJEXT) \
+       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+       ../goto-instrument/full_slicer$(OBJEXT) \
+       ../goto-instrument/nondet_static$(OBJEXT) \
+       ../goto-instrument/cover$(OBJEXT) \
+       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
+       ../goto-instrument/cover_filter$(OBJEXT) \
+       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
+       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
+       ../goto-instrument/cover_instrument_decision$(OBJEXT) \
+       ../goto-instrument/cover_instrument_location$(OBJEXT) \
+       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+       ../goto-instrument/cover_instrument_other$(OBJEXT) \
+       ../goto-instrument/cover_util$(OBJEXT) \
+       ../goto-instrument/unwindset$(OBJEXT) \
+       ../analyses/analyses$(LIBEXT) \
+       ../langapi/langapi$(LIBEXT) \
+       ../xmllang/xmllang$(LIBEXT) \
+       ../assembler/assembler$(LIBEXT) \
+       ../solvers/solvers$(LIBEXT) \
+       ../util/util$(LIBEXT) \
+       ../json/json$(LIBEXT) \
+       ../cbmc/bv_cbmc$(OBJEXT) \
+       ../cbmc/cbmc_dimacs$(OBJEXT) \
+       ../cbmc/cbmc_solvers$(OBJEXT) \
+       ../cbmc/symex_bmc$(OBJEXT)
+
+INCLUDES= -I ..
+
+LIBS =
+
+include ../config.inc
+include ../common
+
+CLEANFILES = ccover$(EXEEXT)
+
+all: ccover$(EXEEXT)
+
+ifneq ($(wildcard ../bv_refinement/Makefile),)
+  OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
+endif
+
+ifneq ($(wildcard ../jsil/Makefile),)
+  OBJ += ../jsil/jsil$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_JSIL
+endif
+
+###############################################################################
+
+ccover$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: ccover-mac-signed
+
+ccover-mac-signed: ccover$(EXEEXT)
+	strip ccover$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) ccover$(EXEEXT)
diff --git a/src/cbmc/bmc_cover.cpp b/src/ccover/bmc_cover.cpp
similarity index 98%
rename from src/cbmc/bmc_cover.cpp
rename to src/ccover/bmc_cover.cpp
index 12d9ef66bb6..e599ee0b684 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/ccover/bmc_cover.cpp
@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Test-Suite Generation with BMC
 
-#include "bmc.h"
+#include "ccover_bmc.h"
 
 #include <chrono>
 #include <iomanip>
@@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
-#include "bv_cbmc.h"
+#include <cbmc/bv_cbmc.h>
 
 class bmc_covert:
   public cover_goalst::observert,
@@ -38,7 +38,7 @@ class bmc_covert:
 public:
   bmc_covert(
     const goto_functionst &_goto_functions,
-    bmct &_bmc):
+    ccover_bmct &_bmc):
     goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc)
   {
   }
@@ -141,7 +141,7 @@ class bmc_covert:
 protected:
   const goto_functionst &goto_functions;
   prop_convt &solver;
-  bmct &bmc;
+  ccover_bmct &bmc;
 };
 
 static bool is_failed_assumption_step(
@@ -420,7 +420,7 @@ bool bmc_covert::operator()()
 }
 
 /// Try to cover all goals
-bool bmct::cover(const goto_functionst &goto_functions)
+bool ccover_bmct::cover(const goto_functionst &goto_functions)
 {
   bmc_covert bmc_cover(goto_functions, *this);
   bmc_cover.set_message_handler(get_message_handler());
diff --git a/src/ccover/ccover_bmc.cpp b/src/ccover/ccover_bmc.cpp
new file mode 100644
index 00000000000..6d9c0fc0b4d
--- /dev/null
+++ b/src/ccover/ccover_bmc.cpp
@@ -0,0 +1,199 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking for Test Suite Generation
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Bounded Model Checking for Test Suite Generation
+
+#include "ccover_bmc.h"
+
+#include <util/exit_codes.h>
+#include <util/string2int.h>
+#include <util/string_utils.h>
+
+#include <langapi/language_util.h>
+
+#include <goto-symex/memory_model_pso.h>
+#include <goto-symex/path_storage.h>
+#include <goto-symex/slice.h>
+#include <goto-symex/slice_by_trace.h>
+
+#include <cbmc/cbmc_solvers.h>
+
+#include <linking/static_lifetime_init.h>
+
+void ccover_bmct::do_conversion()
+{
+  status() << "converting SSA" << eom;
+
+  // convert SSA
+  equation.convert(prop_conv);
+}
+
+void ccover_bmct::get_memory_model()
+{
+  const std::string mm=options.get_option("mm");
+
+  if(mm.empty() || mm=="sc")
+    memory_model=util_make_unique<memory_model_sct>(ns);
+  else if(mm=="tso")
+    memory_model=util_make_unique<memory_model_tsot>(ns);
+  else if(mm=="pso")
+    memory_model=util_make_unique<memory_model_psot>(ns);
+  else
+  {
+    error() << "Invalid memory model " << mm
+            << " -- use one of sc, tso, pso" << eom;
+    throw "invalid memory model";
+  }
+}
+
+void ccover_bmct::setup()
+{
+  get_memory_model();
+
+  {
+    const symbolt *init_symbol;
+    if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
+      symex.language_mode=init_symbol->mode;
+  }
+
+  status() << "Starting Bounded Model Checking" << eom;
+
+  symex.last_source_location.make_nil();
+
+  symex.unwindset.parse_unwind(options.get_option("unwind"));
+  symex.unwindset.parse_unwindset(options.get_option("unwindset"));
+}
+
+void ccover_bmct::run(abstract_goto_modelt &goto_model)
+{
+  setup();
+
+  auto get_goto_function = [&goto_model](const irep_idt &id) ->
+    const goto_functionst::goto_functiont &
+  {
+    return goto_model.get_goto_function(id);
+  };
+
+  // perform symbolic execution
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+
+  // Borrow a reference to the goto functions map. This reference, or
+  // iterators pointing into it, must not be stored by this function or its
+  // callees, as goto_model.get_goto_function (as used by symex)
+  // will have side-effects on it.
+  const goto_functionst &goto_functions =
+    goto_model.get_goto_functions();
+
+  // add a partial ordering, if required
+  if(equation.has_threads())
+  {
+    memory_model->set_message_handler(get_message_handler());
+    (*memory_model)(equation);
+  }
+
+  statistics() << "size of program expression: "
+               << equation.SSA_steps.size()
+               << " steps" << eom;
+
+  slice();
+
+//  const optionst::value_listt criteria=
+//    options.get_list_option("cover");
+
+  cover(goto_functions);
+}
+
+void ccover_bmct::slice()
+{
+  // any properties to check at all?
+  if(equation.has_threads())
+  {
+    // we should build a thread-aware SSA slicer
+    statistics() << "no slicing due to threads" << eom;
+  }
+  else
+  {
+    if(options.get_bool_option("slice-formula"))
+    {
+      ::slice(equation);
+      statistics() << "slicing removed "
+                   << equation.count_ignored_SSA_steps()
+                   << " assignments" << eom;
+    }
+    else
+    {
+      if(options.get_list_option("cover").empty())
+      {
+        simple_slice(equation);
+        statistics() << "simple slicing removed "
+                     << equation.count_ignored_SSA_steps()
+                     << " assignments" << eom;
+      }
+    }
+  }
+
+  statistics() << "Generated "
+               << symex.total_vccs<<" VCC(s), "
+               << symex.remaining_vccs
+               << " remaining after simplification" << eom;
+}
+
+/// Perform core BMC, using an abstract model to supply GOTO function bodies
+/// (perhaps created on demand).
+/// \param opts: command-line options affecting BMC
+/// \param model: provides goto function bodies and the symbol table, perhaps
+//    creating those function bodies on demand.
+/// \param ui: user-interface mode (plain text, XML output, JSON output, ...)
+/// \param message_handler: used for logging
+int ccover_bmct::do_bmc(
+  const optionst &opts,
+  abstract_goto_modelt &model,
+  const ui_message_handlert::uit &ui,
+  message_handlert &message_handler)
+{
+  const symbol_tablet &symbol_table = model.get_symbol_table();
+   messaget message(message_handler);
+
+  path_strategy_choosert path_strategy_chooser;
+  std::unique_ptr<path_storaget> path_storage=
+    path_strategy_chooser.get("lifo");
+
+  try
+  {
+    cbmc_solverst solvers(opts, symbol_table, message_handler);
+    solvers.set_ui(ui);
+    std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+    cbmc_solver = solvers.get_solver();
+    prop_convt &pc = cbmc_solver->prop_conv();
+    ccover_bmct bmc(opts, symbol_table, message_handler, pc, *path_storage);
+    bmc.set_ui(ui);
+    bmc.run(model);
+    return CPROVER_EXIT_SUCCESS;
+  }
+  catch(const char *error_msg)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(const std::string &error_msg)
+  {
+    message.error() << error_msg << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+  catch(const std::bad_alloc &)
+  {
+    message.error() << "Out of memory" << eom;
+    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
+  }
+  catch(...)
+  {
+    message.error() << "unable to get solver" << message.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+}
diff --git a/src/ccover/ccover_bmc.h b/src/ccover/ccover_bmc.h
new file mode 100644
index 00000000000..194115908ec
--- /dev/null
+++ b/src/ccover/ccover_bmc.h
@@ -0,0 +1,100 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking for Test Suite Generation
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Bounded Model Checking for Test Suite Generation
+
+#ifndef CPROVER_CCOVER_CCOVER_BMC_H
+#define CPROVER_CCOVER_CCOVER_BMC_H
+
+#include <memory>
+
+#include <util/ui_message.h>
+
+#include <goto-programs/goto_trace.h>
+
+#include <goto-symex/symex_target_equation.h>
+#include <goto-programs/goto_model.h>
+#include <goto-symex/memory_model.h>
+
+#include <cbmc/symex_bmc.h>
+
+class optionst;
+
+class ccover_bmct:public messaget
+{
+public:
+  ccover_bmct(
+    const optionst &_options,
+    const symbol_tablet &outer_symbol_table,
+    message_handlert &_message_handler,
+    prop_convt &_prop_conv,
+    path_storaget &_path_storage)
+    : messaget(_message_handler),
+      options(_options),
+      outer_symbol_table(outer_symbol_table),
+      ns(outer_symbol_table, symex_symbol_table),
+      equation(),
+      path_storage(_path_storage),
+      symex(_message_handler, outer_symbol_table, equation, _options, path_storage),
+      prop_conv(_prop_conv),
+      ui(ui_message_handlert::uit::PLAIN)
+  {
+    symex.constant_propagation=options.get_bool_option("propagation");
+    symex.record_coverage=
+      !options.get_option("symex-coverage-report").empty();
+  }
+
+  void run(abstract_goto_modelt &);
+
+  virtual ~ccover_bmct() { }
+
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
+
+  static int do_bmc(
+    const optionst &opts,
+    abstract_goto_modelt &goto_model,
+    const ui_message_handlert::uit &ui,
+    message_handlert &);
+
+protected:
+  const optionst &options;
+  /// \brief symbol table for the goto-program that we will execute
+
+  const symbol_tablet &outer_symbol_table;
+  /// \brief symbol table generated during symbolic execution
+
+  symbol_tablet symex_symbol_table;
+  namespacet ns;
+  symex_target_equationt equation;
+  path_storaget &path_storage;
+  symex_bmct symex;
+  prop_convt &prop_conv;
+  std::unique_ptr<memory_model_baset> memory_model;
+  // use gui format
+  ui_message_handlert::uit ui;
+
+  // unwinding
+  void setup_unwind();
+  void do_conversion();
+
+  trace_optionst trace_options()
+  {
+    return trace_optionst(options);
+  }
+
+  void setup();
+  void get_memory_model();
+  void slice();
+
+  bool cover(const goto_functionst &);
+
+  friend class bmc_covert;
+};
+
+#endif // CPROVER_CCOVER_CCOVER_BMC_H
diff --git a/src/ccover/ccover_main.cpp b/src/ccover/ccover_main.cpp
new file mode 100644
index 00000000000..0190c23dd05
--- /dev/null
+++ b/src/ccover/ccover_main.cpp
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: ccover Main Module
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// ccover Main Module
+
+/*
+
+  ccover
+  Test suite generation for ANSI-C
+  Copyright (C) 2018 Daniel Kroening <kroening@kroening.com>
+
+*/
+
+#include "ccover_parse_options.h"
+
+#include <util/unicode.h>
+
+#ifdef _MSC_VER
+int wmain(int argc, const wchar_t **argv_wide)
+{
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
+#else
+int main(int argc, const char **argv)
+{
+#endif
+  ccover_parse_optionst parse_options(argc, argv);
+
+  int res=parse_options.main();
+
+  return res;
+}
diff --git a/src/ccover/ccover_parse_options.cpp b/src/ccover/ccover_parse_options.cpp
new file mode 100644
index 00000000000..279690b96e9
--- /dev/null
+++ b/src/ccover/ccover_parse_options.cpp
@@ -0,0 +1,752 @@
+/*******************************************************************\
+
+Module: CBMC Command Line Option Processing
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// CBMC Command Line Option Processing
+
+#include "ccover_parse_options.h"
+
+#include <fstream>
+#include <cstdlib> // exit()
+#include <iostream>
+#include <memory>
+
+#include <util/config.h>
+#include <util/exit_codes.h>
+#include <util/invariant.h>
+#include <util/string2int.h>
+#include <util/unicode.h>
+#include <util/version.h>
+
+#include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <ansi-c/c_preprocess.h>
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/cprover_library.h>
+
+#include <cpp/cpp_language.h>
+#include <cpp/cprover_library.h>
+
+#include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/instrument_preconditions.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
+#include <goto-programs/mm_io.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_returns.h>
+#include <goto-programs/remove_vector.h>
+#include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/set_properties.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_symbol_table.h>
+#include <goto-programs/show_properties.h>
+#include <goto-programs/string_abstraction.h>
+#include <goto-programs/string_instrumentation.h>
+
+#include <goto-symex/rewrite_union.h>
+
+#include <goto-instrument/full_slicer.h>
+#include <goto-instrument/nondet_static.h>
+#include <goto-instrument/cover.h>
+
+#include <pointer-analysis/add_failed_symbols.h>
+
+#include <langapi/mode.h>
+
+ccover_parse_optionst::ccover_parse_optionst(int argc, const char **argv):
+  parse_options_baset(CCOVER_OPTIONS, argc, argv),
+  messaget(ui_message_handler),
+  ui_message_handler(cmdline, std::string("ccover ") + CBMC_VERSION)
+{
+}
+
+void ccover_parse_optionst::eval_verbosity()
+{
+  // this is our default verbosity
+  unsigned int v=messaget::M_STATISTICS;
+
+  if(cmdline.isset("verbosity"))
+  {
+    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
+    if(v>10)
+      v=10;
+  }
+
+  ui_message_handler.set_verbosity(v);
+}
+
+void ccover_parse_optionst::get_command_line_options(optionst &options)
+{
+  if(config.set(cmdline))
+  {
+    usage_error();
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
+  if(cmdline.isset("paths"))
+    options.set_option("paths", true);
+
+  if(cmdline.isset("show-vcc"))
+    options.set_option("show-vcc", true);
+
+  if(cmdline.isset("cover"))
+    parse_cover_options(cmdline, options);
+  else // default criterion
+    options.set_option("cover", std::list<std::string>({"location"}));
+
+  if(cmdline.isset("mm"))
+    options.set_option("mm", cmdline.get_value("mm"));
+
+  if(cmdline.isset("c89"))
+    config.ansi_c.set_c89();
+
+  if(cmdline.isset("c99"))
+    config.ansi_c.set_c99();
+
+  if(cmdline.isset("c11"))
+    config.ansi_c.set_c11();
+
+  if(cmdline.isset("cpp98"))
+    config.cpp.set_cpp98();
+
+  if(cmdline.isset("cpp03"))
+    config.cpp.set_cpp03();
+
+  if(cmdline.isset("cpp11"))
+    config.cpp.set_cpp11();
+
+  if(cmdline.isset("no-simplify"))
+    options.set_option("simplify", false);
+  else
+    options.set_option("simplify", true);
+
+  if(cmdline.isset("trace"))
+    options.set_option("trace", true);
+
+  if(cmdline.isset("unwind"))
+    options.set_option("unwind", cmdline.get_value("unwind"));
+
+  if(cmdline.isset("depth"))
+    options.set_option("depth", cmdline.get_value("depth"));
+
+  if(cmdline.isset("debug-level"))
+    options.set_option("debug-level", cmdline.get_value("debug-level"));
+
+  if(cmdline.isset("unwindset"))
+    options.set_option("unwindset", cmdline.get_value("unwindset"));
+
+  // constant propagation
+  if(cmdline.isset("no-propagation"))
+    options.set_option("propagation", false);
+  else
+    options.set_option("propagation", true);
+
+  // use assumptions
+  if(cmdline.isset("no-assumptions"))
+    options.set_option("assumptions", false);
+  else
+    options.set_option("assumptions", true);
+
+  // remove unused equations
+  options.set_option(
+    "slice-formula",
+    cmdline.isset("slice-formula"));
+
+  // simplify if conditions and branches
+  if(cmdline.isset("no-simplify-if"))
+    options.set_option("simplify-if", false);
+  else
+    options.set_option("simplify-if", true);
+
+  if(cmdline.isset("arrays-uf-always"))
+    options.set_option("arrays-uf", "always");
+  else if(cmdline.isset("arrays-uf-never"))
+    options.set_option("arrays-uf", "never");
+  else
+    options.set_option("arrays-uf", "auto");
+
+  if(cmdline.isset("refine-arrays"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+  }
+
+  if(cmdline.isset("refine-arithmetic"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arithmetic", true);
+  }
+
+  if(cmdline.isset("refine"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+    options.set_option("refine-arithmetic", true);
+  }
+
+  if(cmdline.isset("refine-strings"))
+  {
+    options.set_option("refine-strings", true);
+    options.set_option("string-printable", cmdline.isset("string-printable"));
+    if(cmdline.isset("string-max-length"))
+      options.set_option(
+        "string-max-length", cmdline.get_value("string-max-length"));
+  }
+
+  if(cmdline.isset("max-node-refinement"))
+    options.set_option(
+      "max-node-refinement",
+      cmdline.get_value("max-node-refinement"));
+
+  if(cmdline.isset("aig"))
+    options.set_option("aig", true);
+
+  if(cmdline.isset("fpa"))
+    options.set_option("fpa", true);
+
+  if(cmdline.isset("boolector"))
+  {
+    options.set_option("boolector", true);
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("mathsat"))
+  {
+    options.set_option("mathsat", true);
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("cvc4"))
+  {
+    options.set_option("cvc4", true);
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("yices"))
+  {
+    options.set_option("yices", true);
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("z3"))
+  {
+    options.set_option("z3", true);
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("beautify"))
+    options.set_option("beautify", true);
+
+  if(cmdline.isset("no-sat-preprocessor"))
+    options.set_option("sat-preprocessor", false);
+  else
+    options.set_option("sat-preprocessor", true);
+
+  if(cmdline.isset("outfile"))
+    options.set_option("outfile", cmdline.get_value("outfile"));
+
+  PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
+}
+
+/// invoke main modules
+int ccover_parse_optionst::doit()
+{
+  if(cmdline.isset("version"))
+  {
+    std::cout << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  //
+  // command line options
+  //
+
+  optionst options;
+  try
+  {
+    get_command_line_options(options);
+  }
+
+  catch(const char *error_msg)
+  {
+    error() << error_msg << eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
+  catch(const std::string &error_msg)
+  {
+    error() << error_msg << eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
+  eval_verbosity();
+
+  //
+  // Print a banner
+  //
+  status() << "CBMC version " << CBMC_VERSION << ' '
+           << sizeof(void *)*8 << "-bit "
+           << config.this_architecture() << ' '
+           << config.this_operating_system() << eom;
+
+  //
+  // Unwinding of transition systems is done by hw-cbmc.
+  //
+
+  if(cmdline.isset("module") ||
+     cmdline.isset("gen-interface"))
+  {
+    error() << "This version of CBMC has no support for "
+               " hardware modules. Please use hw-cbmc." << eom;
+    return CPROVER_EXIT_USAGE_ERROR;
+  }
+
+  register_language(new_ansi_c_language);
+  register_language(new_cpp_language);
+
+  if(cmdline.isset("test-preprocessor"))
+    return test_c_preprocessor(get_message_handler())
+             ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
+             : CPROVER_EXIT_SUCCESS;
+
+  if(cmdline.isset("preprocess"))
+  {
+    preprocessing();
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  if(cmdline.isset("show-parse-tree"))
+  {
+    if(cmdline.args.size()!=1 ||
+       is_goto_binary(cmdline.args[0]))
+    {
+      error() << "Please give exactly one source file" << eom;
+      return CPROVER_EXIT_INCORRECT_TASK;
+    }
+
+    std::string filename=cmdline.args[0];
+
+    #ifdef _MSC_VER
+    std::ifstream infile(widen(filename));
+    #else
+    std::ifstream infile(filename);
+    #endif
+
+    if(!infile)
+    {
+      error() << "failed to open input file `"
+              << filename << "'" << eom;
+      return CPROVER_EXIT_INCORRECT_TASK;
+    }
+
+    std::unique_ptr<languaget> language=
+      get_language_from_filename(filename);
+
+    if(language==nullptr)
+    {
+      error() << "failed to figure out type of file `"
+              <<  filename << "'" << eom;
+      return CPROVER_EXIT_INCORRECT_TASK;
+    }
+
+    language->get_language_options(cmdline);
+    language->set_message_handler(get_message_handler());
+
+    status() << "Parsing " << filename << eom;
+
+    if(language->parse(infile, filename))
+    {
+      error() << "PARSING ERROR" << eom;
+      return CPROVER_EXIT_INCORRECT_TASK;
+    }
+
+    language->show_parse(std::cout);
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  int get_goto_program_ret=get_goto_program(options);
+
+  if(get_goto_program_ret!=-1)
+    return get_goto_program_ret;
+
+  return ccover_bmct::do_bmc(
+    options, goto_model, ui_message_handler.get_ui(), get_message_handler());
+}
+
+int ccover_parse_optionst::get_goto_program(
+  const optionst &options)
+{
+  if(cmdline.args.empty())
+  {
+    error() << "Please provide a program to test" << eom;
+    return CPROVER_EXIT_INCORRECT_TASK;
+  }
+
+  try
+  {
+    goto_model=initialize_goto_model(cmdline, get_message_handler());
+
+    if(cmdline.isset("show-symbol-table"))
+    {
+      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      return CPROVER_EXIT_SUCCESS;
+    }
+
+    if(process_goto_program(options))
+      return CPROVER_EXIT_INTERNAL_ERROR;
+
+    // show it?
+    if(cmdline.isset("show-loops"))
+    {
+      show_loop_ids(ui_message_handler.get_ui(), goto_model);
+      return CPROVER_EXIT_SUCCESS;
+    }
+
+    // show it?
+    if(
+      cmdline.isset("show-goto-functions") ||
+      cmdline.isset("list-goto-functions"))
+    {
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        cmdline.isset("list-goto-functions"));
+      return CPROVER_EXIT_SUCCESS;
+    }
+
+    status() << config.object_bits_info() << eom;
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
+  catch(const std::string &e)
+  {
+    error() << e << eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
+  catch(int e)
+  {
+    error() << "Numeric exception : " << e << eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
+  catch(const std::bad_alloc &)
+  {
+    error() << "Out of memory" << eom;
+    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
+  }
+
+  return -1; // no error, continue
+}
+
+void ccover_parse_optionst::preprocessing()
+{
+  try
+  {
+    if(cmdline.args.size()!=1)
+    {
+      error() << "Please provide one program to preprocess" << eom;
+      return;
+    }
+
+    std::string filename=cmdline.args[0];
+
+    std::ifstream infile(filename);
+
+    if(!infile)
+    {
+      error() << "failed to open input file" << eom;
+      return;
+    }
+
+    std::unique_ptr<languaget> language=get_language_from_filename(filename);
+    language->get_language_options(cmdline);
+
+    if(language==nullptr)
+    {
+      error() << "failed to figure out type of file" << eom;
+      return;
+    }
+
+    language->set_message_handler(get_message_handler());
+
+    if(language->preprocess(infile, filename, std::cout))
+      error() << "PREPROCESSING ERROR" << eom;
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+  }
+
+  catch(const std::string &e)
+  {
+    error() << e << eom;
+  }
+
+  catch(int e)
+  {
+    error() << "Numeric exception : " << e << eom;
+  }
+
+  catch(const std::bad_alloc &)
+  {
+    error() << "Out of memory" << eom;
+    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
+  }
+}
+
+bool ccover_parse_optionst::process_goto_program(
+  const optionst &options)
+{
+  try
+  {
+    // Remove inline assembler; this needs to happen before
+    // adding the library.
+    remove_asm(goto_model);
+
+    // add the library
+    link_to_library(
+      goto_model, get_message_handler(), cprover_cpp_library_factory);
+    link_to_library(
+      goto_model, get_message_handler(), cprover_c_library_factory);
+
+    if(cmdline.isset("string-abstraction"))
+      string_instrumentation(goto_model, get_message_handler());
+
+    // remove function pointers
+    status() << "Removal of function pointers and virtual functions" << eom;
+    remove_function_pointers(
+      get_message_handler(),
+      goto_model,
+      cmdline.isset("pointer-check"));
+
+    mm_io(goto_model);
+
+    // remove library preconditions
+    remove_preconditions(goto_model);
+
+    // remove returns, gcc vectors, complex
+    remove_returns(goto_model);
+    remove_vector(goto_model);
+    remove_complex(goto_model);
+    rewrite_union(goto_model);
+
+    // checks don't know about adjusted float expressions
+    adjust_float_expressions(goto_model);
+
+    // ignore default/user-specified initialization
+    // of variables with static lifetime
+    if(cmdline.isset("nondet-static"))
+    {
+      status() << "Adding nondeterministic initialization "
+                  "of static/global variables" << eom;
+      nondet_static(goto_model);
+    }
+
+    if(cmdline.isset("string-abstraction"))
+    {
+      status() << "String Abstraction" << eom;
+      string_abstraction(
+        goto_model,
+        get_message_handler());
+    }
+
+    // add failed symbols
+    // needs to be done before pointer analysis
+    add_failed_symbols(goto_model.symbol_table);
+
+    // recalculate numbers, etc.
+    goto_model.goto_functions.update();
+
+    // add loop ids
+    goto_model.goto_functions.compute_loop_numbers();
+
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_model, get_message_handler());
+    }
+
+    // remove skips such that trivial GOTOs are deleted and not considered
+    // for coverage annotation:
+    remove_skip(goto_model);
+
+    // instrument cover goals
+    if(cmdline.isset("cover"))
+    {
+      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+        return true;
+    }
+
+    // label the assertions
+    // This must be done after adding assertions and
+    // before using the argument of the "property" option.
+    // Do not re-label after using the property slicer because
+    // this would cause the property identifiers to change.
+    label_properties(goto_model);
+
+    // full slice?
+    if(cmdline.isset("full-slice"))
+    {
+      status() << "Performing a full slice" << eom;
+      if(cmdline.isset("property"))
+        property_slicer(goto_model, cmdline.get_values("property"));
+      else
+        full_slicer(goto_model);
+    }
+
+    // remove any skips introduced since coverage instrumentation
+    remove_skip(goto_model);
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+    return true;
+  }
+
+  catch(const std::string &e)
+  {
+    error() << e << eom;
+    return true;
+  }
+
+  catch(int e)
+  {
+    error() << "Numeric exception : " << e << eom;
+    return true;
+  }
+
+  catch(const std::bad_alloc &)
+  {
+    error() << "Out of memory" << eom;
+    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
+    return true;
+  }
+
+  return false;
+}
+
+/// display command line help
+void ccover_parse_optionst::help()
+{
+  // clang-format off
+  std::cout << '\n' << banner_string("ccover", CBMC_VERSION) << '\n';
+
+  std::cout <<
+    "* *                     Daniel Kroening                     * *\n"
+    "* *    University of Oxford Computer, Science Department    * *\n"
+    "* *                 kroening@kroening.com                   * *\n"
+    "\n"
+    "Usage:                       Purpose:\n"
+    "\n"
+    " ccover [-?] [-h] [--help]    show help\n"
+    " cccover file.c ...           source file names\n"
+    "\n"
+    "Test suite generation options:\n"
+    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    "                              criteria supported are location, branch,\n"
+    "                              condition, decision, mcdc\n"
+    "                              default: location\n"
+    "\n"    
+    "C/C++ frontend options:\n"
+    " -I path                      set include path (C/C++)\n"
+    " -D macro                     define preprocessor macro (C/C++)\n"
+    " --preprocess                 stop after preprocessing\n"
+    " --16, --32, --64             set width of int\n"
+    " --LP64, --ILP64, --LLP64,\n"
+    "   --ILP32, --LP32            set width of int, long and pointers\n"
+    " --little-endian              allow little-endian word-byte conversions\n"
+    " --big-endian                 allow big-endian word-byte conversions\n"
+    " --unsigned-char              make \"char\" unsigned by default\n"
+    " --mm model                   set memory model (default: sc)\n"
+    " --arch                       set architecture (default: "
+                                   << configt::this_architecture() << ")\n"
+    " --os                         set operating system (default: "
+                                   << configt::this_operating_system() << ")\n"
+    " --c89/99/11                  set C language standard (default: "
+                                   << (configt::ansi_ct::default_c_standard()==
+                                       configt::ansi_ct::c_standardt::C89?"c89":
+                                       configt::ansi_ct::default_c_standard()==
+                                       configt::ansi_ct::c_standardt::C99?"c99":
+                                       configt::ansi_ct::default_c_standard()==
+                                       configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
+    " --cpp98/03/11                set C++ language standard (default: "
+                                   << (configt::cppt::default_cpp_standard()==
+                                       configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
+                                       configt::cppt::default_cpp_standard()==
+                                       configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
+                                       configt::cppt::default_cpp_standard()==
+                                       configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
+    #ifdef _WIN32
+    " --gcc                        use GCC as preprocessor\n"
+    #endif
+    " --no-arch                    don't set up an architecture\n"
+    " --no-library                 disable built-in abstract C library\n"
+    " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
+    " --round-to-nearest           rounding towards nearest even (default)\n"
+    " --round-to-plus-inf          rounding towards plus infinity\n"
+    " --round-to-minus-inf         rounding towards minus infinity\n"
+    " --round-to-zero              rounding towards zero\n"
+    HELP_FUNCTIONS
+    "\n"
+    "Program instrumentation options:\n"
+    " --no-assumptions             ignore user assumptions\n"
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
+    "\n"
+    "Semantic transformations:\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    "\n"
+    "BMC options:\n"
+    HELP_BMC
+    "\n"
+    "Solver options:\n"
+    " --object-bits n              number of bits used for object addresses\n"
+    " --dimacs                     generate CNF in DIMACS format\n"
+    " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
+    " --boolector                  use Boolector\n"
+    " --mathsat                    use MathSAT\n"
+    " --cvc4                       use CVC4\n"
+    " --yices                      use Yices\n"
+    " --z3                         use Z3\n"
+    " --refine                     use refinement procedure (experimental)\n"
+    " --refine-strings             use string refinement (experimental)\n"
+    " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
+    " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
+    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
+    " --outfile filename           output formula to given file\n"
+    " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
+    " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
+    "\n"
+    "Other options:\n"
+    " --version                    show version and exit\n"
+    " --xml-ui                     use XML-formatted output\n"
+    " --json-ui                    use JSON-formatted output\n"
+    HELP_GOTO_TRACE
+    " --verbosity #                verbosity level\n"
+    HELP_TIMESTAMP
+    "\n";
+  // clang-format on
+}
diff --git a/src/ccover/ccover_parse_options.h b/src/ccover/ccover_parse_options.h
new file mode 100644
index 00000000000..f58461d6c11
--- /dev/null
+++ b/src/ccover/ccover_parse_options.h
@@ -0,0 +1,91 @@
+/*******************************************************************\
+
+Module: CBMC Command Line Option Processing
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// CBMC Command Line Option Processing
+
+#ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
+#define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
+
+#include <util/ui_message.h>
+#include <util/parse_options.h>
+
+#include <langapi/language.h>
+
+#include <goto-programs/goto_model.h>
+
+#include <cbmc/bmc.h>
+
+#include "ccover_bmc.h"
+
+class optionst;
+
+// clang-format off
+#define CCOVER_OPTIONS \
+  OPT_BMC \
+  "(preprocess)(slice-by-trace):" \
+  OPT_FUNCTIONS \
+  "(no-simplify)(full-slice)" \
+  "(debug-level):(no-propagation)(no-simplify-if)" \
+  "(document-subgoals)(outfile):(test-preprocessor)" \
+  "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
+  "(object-bits):" \
+  "(no-assumptions)" \
+  "(xml-ui)(xml-interface)(json-ui)" \
+  "(smt2)(fpa)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
+  "(no-sat-preprocessor)" \
+  "(beautify)" \
+  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
+  "(refine-strings)" \
+  "(string-printable)" \
+  "(string-max-length):" \
+  "(string-max-input-length):" \
+  "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
+  "(little-endian)(big-endian)" \
+  OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
+  "(show-symbol-table)(show-parse-tree)" \
+  "(drop-unused-functions)" \
+  "(verbosity):(no-library)" \
+  "(nondet-static)" \
+  "(version)" \
+  "(cover):" \
+  "(mm):" \
+  OPT_TIMESTAMP \
+  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
+  "(ppc-macos)(unsigned-char)" \
+  "(arrays-uf-always)(arrays-uf-never)" \
+  "(string-abstraction)(no-arch)(arch):" \
+  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
+  OPT_GOTO_TRACE \
+  "(fixedbv)"
+// clang-format on
+
+class ccover_parse_optionst:
+  public parse_options_baset,
+  public messaget
+{
+public:
+  virtual int doit() override;
+  virtual void help() override;
+
+  ccover_parse_optionst(int argc, const char **argv);
+
+protected:
+  goto_modelt goto_model;
+  ui_message_handlert ui_message_handler;
+
+  void eval_verbosity();
+  void register_languages();
+  void get_command_line_options(optionst &);
+  void preprocessing();
+  int get_goto_program(const optionst &);
+  bool process_goto_program(const optionst &);
+};
+
+#endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
diff --git a/unit/Makefile b/unit/Makefile
index eeff4e499fe..85485cc61ce 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -61,7 +61,6 @@ testing-utils.dir:
 # 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/bv_cbmc$(OBJEXT) \
           ../src/cbmc/cbmc_dimacs$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \