diff --git a/regression/cbmc-java/reachability-slice/test.desc b/regression/cbmc-java/reachability-slice/test.desc
index 972f34bca71..a5f7064d5f9 100644
--- a/regression/cbmc-java/reachability-slice/test.desc
+++ b/regression/cbmc-java/reachability-slice/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
 1001
@@ -9,3 +9,5 @@ A.class
 --
 Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
 At the time of writing of this test, 1002 is removed.
+
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/regression/cbmc-java/reachability-slice/test2.desc b/regression/cbmc-java/reachability-slice/test2.desc
index 7bb351660bc..d8eea80d626 100644
--- a/regression/cbmc-java/reachability-slice/test2.desc
+++ b/regression/cbmc-java/reachability-slice/test2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
 1001
@@ -7,3 +7,5 @@ A.class
 1005
 --
 1004
+--
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/regression/cbmc-java/reachability-slice/test3.desc b/regression/cbmc-java/reachability-slice/test3.desc
index 271adbc2f0b..8c84468ecc0 100644
--- a/regression/cbmc-java/reachability-slice/test3.desc
+++ b/regression/cbmc-java/reachability-slice/test3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --cover location
 1001
@@ -6,3 +6,6 @@ A.class
 1003
 1004
 1005
+--
+--
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 42ef9afee20..0cd241a8cad 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -385,7 +385,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     for(const char *opt :
       { "nondet-static",
         "full-slice",
-        "lazy-methods" })
+        "lazy-methods",
+        "reachability-slice",
+        "reachability-slice-fb" })
     {
       if(cmdline.isset(opt))
       {