diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index c2d3e5851b3..41d176e8dd9 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -382,9 +382,7 @@ safety_checkert::resultt bmct::execute(
 
     if(!options.get_list_option("cover").empty())
     {
-      const optionst::value_listt criteria=
-        options.get_list_option("cover");
-      return cover(goto_functions, criteria)?
+      return cover(goto_functions)?
         safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
     }
 
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 68b0c9a940d..8e812e8e1da 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -223,9 +223,7 @@ class bmct:public safety_checkert
   void slice();
   void show();
 
-  bool cover(
-    const goto_functionst &goto_functions,
-    const optionst::value_listt &criteria);
+  bool cover(const goto_functionst &goto_functions);
 
   friend class bmc_all_propertiest;
   friend class bmc_covert;
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index 2382c7d8bfa..fd0d43313e2 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -426,9 +426,7 @@ bool bmc_covert::operator()()
 }
 
 /// Try to cover all goals
-bool bmct::cover(
-  const goto_functionst &goto_functions,
-  const optionst::value_listt &criteria)
+bool bmct::cover(const goto_functionst &goto_functions)
 {
   bmc_covert bmc_cover(goto_functions, *this);
   bmc_cover.set_message_handler(get_message_handler());