Make use of simple-slice explicit

Simple slicing was deactivated with --cover
inside a utility function.
Now, we activate simple-slice by default
and deliberately turn it off when --cover is present.

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -108,6 +108,7 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("propagation", true);
   options.set_option("refine-strings", true);
   options.set_option("sat-preprocessor", true);
+  options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
 

src/cbmc/cbmc_parse_options.cpp

@@ -114,6 +114,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("pretty-names", true);
   options.set_option("propagation", true);
   options.set_option("sat-preprocessor", true);
+  options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
 

src/goto-checker/bmc_util.cpp

@@ -233,7 +233,7 @@ void slice(
     }
     else
     {
-      if(options.get_list_option("cover").empty())
+      if(options.get_bool_option("simple-slice"))
       {
         simple_slice(symex_target_equation);
         msg.statistics() << "simple slicing removed "

src/goto-instrument/cover.cpp

@@ -165,6 +165,10 @@ parse_coverage_criterion(const std::string &criterion_string)
 void parse_cover_options(const cmdlinet &cmdline, optionst &options)
 {
   options.set_option("cover", cmdline.get_values("cover"));
+
+  // allow retrieving full traces
+  options.set_option("simple-slice", false);
+
   options.set_option(
     "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
   options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));