diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md
index 0ae4eab3fc7..ad792cb2c1b 100644
--- a/doc/architectural/folder-walkthrough.md
+++ b/doc/architectural/folder-walkthrough.md
@@ -14,6 +14,7 @@ containing the code for a different part of the system.
   * \ref linking
 
 - Symbolic Execution
+  * \ref goto-checker
   * \ref goto-symex
 
 - Static Analyses
@@ -36,9 +37,10 @@ containing the code for a different part of the system.
 
   * \ref cbmc
   * \ref goto-analyzer
-  * \ref goto-instrument
-  * \ref goto-diff
   * \ref goto-cc
+  * \ref goto-diff
+  * \ref goto-harness
+  * \ref goto-instrument
   * \ref jbmc
 
 - Utilities
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 91853a8b29c..993c7170c3c 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/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);
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 22e3a67aaac..74790aeee2a 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/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);
 
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 335a831e015..4d2b1fdae5f 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/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 "
diff --git a/src/goto-checker/goto_trace_provider.h b/src/goto-checker/goto_trace_provider.h
index cab2138e4bd..e56902c3d3f 100644
--- a/src/goto-checker/goto_trace_provider.h
+++ b/src/goto-checker/goto_trace_provider.h
@@ -23,6 +23,8 @@ class goto_trace_providert
 {
 public:
   /// Builds and returns the complete trace
+  /// \note If slicing is used then the trace will not be complete.
+  ///   E.g. with simple-slice it will end at the last assertion.
   virtual goto_tracet build_full_trace() const = 0;
 
   /// Builds and returns the trace up to the first failed property
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index d9e7475ff18..b4d84258684 100644
--- a/src/goto-instrument/cover.cpp
+++ b/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"));