diff --git a/regression/cbmc/full_slice1/test.desc b/regression/cbmc/full_slice1/test.desc
index 77b2ad2d1a8..9a991639be9 100644
--- a/regression/cbmc/full_slice1/test.desc
+++ b/regression/cbmc/full_slice1/test.desc
@@ -1,8 +1,13 @@
 CORE
 main.c
---full-slice --property main.assertion.1 --unwind 1
+--full-slice --property main.assertion.1 --unwind 1 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED
 --
 ^warning: ignoring
+^Thread 0 file main.c line 16 function doit
+^Thread 0 file main.c line 19 function doit
+^Thread 0 file main.c line 21 function doit
+^Thread 0 file main.c line 41 function main
+^Thread 0 file main.c line 42 function main
diff --git a/regression/cbmc/full_slice2/test.desc b/regression/cbmc/full_slice2/test.desc
index ab7f16df02b..f53f38884bd 100644
--- a/regression/cbmc/full_slice2/test.desc
+++ b/regression/cbmc/full_slice2/test.desc
@@ -1,10 +1,14 @@
 CORE
 main.c
---full-slice --property main.assertion.2 --unwind 1
+--full-slice --property main.assertion.2 --unwind 1 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED
 --
 ^warning: ignoring
+^Thread 0 file main.c line 19 function doit
+^Thread 0 file main.c line 21 function doit
+^Thread 0 file main.c line 43 function main
+^Thread 0 file main.c line 44 function main
 --
 Tests whether properties are not relabelled after slicing.
\ No newline at end of file
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ad64f5e8a17..0fd7408aeef 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -134,6 +134,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("full-slice"))
+    options.set_option("full-slice", true);
+
   if(cmdline.isset("show-symex-strategies"))
   {
     std::cout << path_strategy_chooser.show_strategies();