diff --git a/regression/cbmc-java/reachability-slice/A.class b/regression/cbmc-java/reachability-slice/A.class
new file mode 100644
index 00000000000..7f527e5fa9a
Binary files /dev/null and b/regression/cbmc-java/reachability-slice/A.class differ
diff --git a/regression/cbmc-java/reachability-slice/A.java b/regression/cbmc-java/reachability-slice/A.java
new file mode 100644
index 00000000000..7680ebd172f
--- /dev/null
+++ b/regression/cbmc-java/reachability-slice/A.java
@@ -0,0 +1,14 @@
+public class A {
+
+    public void foo(int i ) {
+      // We use integer constants that we grep for later in a goto program.
+      int x = 1001 + i;
+      if (i > 0) {
+        x = 1002 + i; // property "java::A.foo:(I)V.coverage.3", see https://github.com/diffblue/cbmc/pull/1943#discussion_r175367063 for a discusison.
+        x = 1003 + i;
+      }
+      else
+        x = 1004 + i;
+      x = 1005 + i;  
+    }
+}
diff --git a/regression/cbmc-java/reachability-slice/test.desc b/regression/cbmc-java/reachability-slice/test.desc
new file mode 100644
index 00000000000..972f34bca71
--- /dev/null
+++ b/regression/cbmc-java/reachability-slice/test.desc
@@ -0,0 +1,11 @@
+CORE
+A.class
+--reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+1001
+--
+1003
+1004
+1005
+--
+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.
diff --git a/regression/cbmc-java/reachability-slice/test2.desc b/regression/cbmc-java/reachability-slice/test2.desc
new file mode 100644
index 00000000000..7bb351660bc
--- /dev/null
+++ b/regression/cbmc-java/reachability-slice/test2.desc
@@ -0,0 +1,9 @@
+CORE
+A.class
+--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+1001
+1002
+1003
+1005
+--
+1004
diff --git a/regression/cbmc-java/reachability-slice/test3.desc b/regression/cbmc-java/reachability-slice/test3.desc
new file mode 100644
index 00000000000..271adbc2f0b
--- /dev/null
+++ b/regression/cbmc-java/reachability-slice/test3.desc
@@ -0,0 +1,8 @@
+CORE
+A.class
+--reachability-slice --show-goto-functions --cover location
+1001
+1002
+1003
+1004
+1005
diff --git a/regression/cbmc/reachability-slice/test.c b/regression/cbmc/reachability-slice/test.c
new file mode 100644
index 00000000000..d40a8d10b36
--- /dev/null
+++ b/regression/cbmc/reachability-slice/test.c
@@ -0,0 +1,13 @@
+void foo(int i)
+{
+  // We use integer constants that we grep for later in a goto program.
+  int x = 1001 + i;
+  if(i > 0)
+  { //foo.coverage.2
+    x = 1002 + i;
+    x = 1003 + i;
+  }
+  else
+    x = 1004 + i;
+  x = 1005 + i;
+}
diff --git a/regression/cbmc/reachability-slice/test.desc b/regression/cbmc/reachability-slice/test.desc
new file mode 100644
index 00000000000..b43ba07552c
--- /dev/null
+++ b/regression/cbmc/reachability-slice/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--reachability-slice --show-goto-functions --cover location --property foo.coverage.2
+1001
+--
+1004
+1005
+--
+We do not include 1002 and 1003, whether this is hit depends on where assertion is put
diff --git a/regression/cbmc/reachability-slice/test2.desc b/regression/cbmc/reachability-slice/test2.desc
new file mode 100644
index 00000000000..6b9fb6d4d4f
--- /dev/null
+++ b/regression/cbmc/reachability-slice/test2.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
+1001
+1002
+1003
+1005
+--
+1004
diff --git a/regression/cbmc/reachability-slice/test3.desc b/regression/cbmc/reachability-slice/test3.desc
new file mode 100644
index 00000000000..87e694174d1
--- /dev/null
+++ b/regression/cbmc/reachability-slice/test3.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--reachability-slice --show-goto-functions --cover location
+1001
+1002
+1003
+1004
+--
+--
+We do not include 1005 since it might or might not be present based on where the assertion is in the block.
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index df1a5df8279..c1d88efa6be 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -31,6 +31,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/add_failed_symbols$(OBJEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e48e71b2d80..14a92fb6117 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -54,6 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
 
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
@@ -801,6 +802,32 @@ bool cbmc_parse_optionst::process_goto_program(
     // this would cause the property identifiers to change.
     label_properties(goto_model);
 
+    // reachability slice?
+    if(cmdline.isset("reachability-slice-fb"))
+    {
+      if(cmdline.isset("reachability-slice"))
+      {
+        error() << "--reachability-slice and --reachability-slice-fb "
+                << "must not be given together" << eom;
+        return true;
+      }
+
+      status() << "Performing a forwards-backwards reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"), true);
+      else
+        reachability_slicer(goto_model, true);
+    }
+
+    if(cmdline.isset("reachability-slice"))
+    {
+      status() << "Performing a reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"));
+      else
+        reachability_slicer(goto_model);
+    }
+
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -926,6 +953,8 @@ void cbmc_parse_optionst::help()
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
+    HELP_REACHABILITY_SLICER
+    " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     "\n"
     "Semantic transformations:\n"
     // NOLINTNEXTLINE(whitespace/line_length)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 4d5cc8ed943..9a47b4eed2c 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -36,6 +36,7 @@ class optionst;
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
+  OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
index 7773aa7a760..9658c218a83 100644
--- a/src/goto-instrument/reachability_slicer.cpp
+++ b/src/goto-instrument/reachability_slicer.cpp
@@ -7,7 +7,11 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 /// \file
-/// Slicer
+/// Reachability Slicer
+/// Consider the control flow graph of the goto program and a criterion, and
+/// remove the parts of the graph from which the criterion is not reachable
+/// (and possibly, depending on the parameters, keep those that can be reached
+/// from the criterion).
 
 #include "reachability_slicer.h"
 
@@ -20,41 +24,62 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "full_slicer_class.h"
 #include "reachability_slicer_class.h"
 
-void reachability_slicert::fixedpoint_assertions(
+/// Get the set of nodes that correspond to the given criterion, or that can
+/// appear in concurrent execution. None of these should be sliced away so
+/// they are used as a basis for the search.
+/// \param is_threaded Instructions that might be executed concurrently
+/// \param criterion The criterion we care about
+std::vector<reachability_slicert::cfgt::node_indext>
+reachability_slicert::get_sources(
   const is_threadedt &is_threaded,
   slicing_criteriont &criterion)
 {
-  queuet queue;
+  std::vector<cfgt::node_indext> sources;
+  for(const auto &e_it : cfg.entry_map)
+  {
+    if(criterion(e_it.first) || is_threaded(e_it.first))
+      sources.push_back(e_it.second);
+  }
 
-  for(cfgt::entry_mapt::iterator
-      e_it=cfg.entry_map.begin();
-      e_it!=cfg.entry_map.end();
-      e_it++)
-    if(criterion(e_it->first) ||
-       is_threaded(e_it->first))
-      queue.push(e_it->second);
+  return sources;
+}
 
-  while(!queue.empty())
-  {
-    cfgt::entryt e=queue.top();
-    cfgt::nodet &node=cfg[e];
-    queue.pop();
+/// Perform backwards depth-first search of the control-flow graph of the
+/// goto program, starting from the nodes corresponding to the criterion and
+/// the instructions that might be executed concurrently. Set reaches_assertion
+/// to true for every instruction visited.
+/// \param is_threaded Instructions that might be executed concurrently
+/// \param criterion the criterion we are trying to hit
+void reachability_slicert::fixedpoint_to_assertions(
+  const is_threadedt &is_threaded,
+  slicing_criteriont &criterion)
+{
+  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
 
-    if(node.reaches_assertion)
-      continue;
+  std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, false);
+  for(const auto index : reachable)
+    cfg[index].reaches_assertion = true;
+}
 
-    node.reaches_assertion=true;
+/// Perform forwards depth-first search of the control-flow graph of the
+/// goto program, starting from the nodes corresponding to the criterion and
+/// the instructions that might be executed concurrently. Set reaches_assertion
+/// to true for every instruction visited.
+/// \param is_threaded Instructions that might be executed concurrently
+/// \param criterion the criterion we are trying to hit
+void reachability_slicert::fixedpoint_from_assertions(
+  const is_threadedt &is_threaded,
+  slicing_criteriont &criterion)
+{
+  std::vector<cfgt::node_indext> src = get_sources(is_threaded, criterion);
 
-    for(cfgt::edgest::const_iterator
-        p_it=node.in.begin();
-        p_it!=node.in.end();
-        p_it++)
-    {
-      queue.push(p_it->first);
-    }
-  }
+  const std::vector<cfgt::node_indext> reachable = cfg.get_reachable(src, true);
+  for(const auto index : reachable)
+    cfg[index].reachable_from_assertion = true;
 }
 
+/// This function removes all instructions that have the flag
+/// reaches_assertion or reachable_from_assertion set to true;
 void reachability_slicert::slice(goto_functionst &goto_functions)
 {
   // now replace those instructions that do not reach any assertions
@@ -66,8 +91,9 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
       Forall_goto_program_instructions(i_it, f_it->second.body)
       {
         const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
-        if(!e.reaches_assertion &&
-           !i_it->is_end_function())
+        if(
+          !e.reaches_assertion && !e.reachable_from_assertion &&
+          !i_it->is_end_function())
           i_it->make_assumption(false_exprt());
       }
 
@@ -80,18 +106,55 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
   goto_functions.update();
 }
 
-void reachability_slicer(goto_modelt &goto_model)
+/// Perform reachability slicing on goto_model, with respect to the
+/// criterion given by all properties.
+/// \param goto_model Goto program to slice
+/// \param include_forward_reachability Determines if only instructions
+/// from which the criterion is reachable should be kept (false) or also
+/// those reachable from the criterion (true)
+void reachability_slicer(
+  goto_modelt &goto_model,
+  const bool include_forward_reachability)
 {
   reachability_slicert s;
   assert_criteriont a;
-  s(goto_model.goto_functions, a);
+  s(goto_model.goto_functions, a, include_forward_reachability);
 }
 
+/// Perform reachability slicing on goto_model for selected properties.
+/// \param goto_model Goto program to slice
+/// \param properties The properties relevant for the slicing (i.e. starting
+/// point for the search in the cfg)
+/// \param include_forward_reachability Determines if only instructions
+/// from which the criterion is reachable should be kept (false) or also
+/// those reachable from the criterion (true)
 void reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  const bool include_forward_reachability)
 {
   reachability_slicert s;
   properties_criteriont p(properties);
-  s(goto_model.goto_functions, p);
+  s(goto_model.goto_functions, p, include_forward_reachability);
+}
+
+/// Perform reachability slicing on goto_model, with respect to criterion
+/// comprising all properties. Only instructions from which the criterion
+/// is reachable will be kept.
+/// \param goto_model Goto program to slice
+void reachability_slicer(goto_modelt &goto_model)
+{
+  reachability_slicer(goto_model, false);
+}
+
+/// Perform reachability slicing on goto_model for selected properties. Only
+/// instructions from which the criterion is reachable will be kept.
+/// \param goto_model Goto program to slice
+/// \param properties The properties relevant for the slicing (i.e. starting
+/// point for the search in the cfg)
+void reachability_slicer(
+  goto_modelt &goto_model,
+  const std::list<std::string> &properties)
+{
+  reachability_slicer(goto_model, properties, false);
 }
diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h
index 25e6a19ba5b..976fbcc5923 100644
--- a/src/goto-instrument/reachability_slicer.h
+++ b/src/goto-instrument/reachability_slicer.h
@@ -23,4 +23,22 @@ void reachability_slicer(
   goto_modelt &,
   const std::list<std::string> &properties);
 
+void reachability_slicer(
+  goto_modelt &,
+  const bool include_forward_reachability);
+
+void reachability_slicer(
+  goto_modelt &,
+  const std::list<std::string> &properties,
+  const bool include_forward_reachability);
+
+#define OPT_REACHABILITY_SLICER                                                \
+  "(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
+
+#define HELP_REACHABILITY_SLICER                                               \
+  " --reachability-slice         remove instructions that cannot appear on a " \
+  "trace from entry point to a property\n"                                     \
+  " --reachability-slice-fb      remove instructions that cannot appear on a " \
+  "trace from entry point through a property\n" // NOLINT(*)
+
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H
diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h
index 4f21049892e..5f52a6d1795 100644
--- a/src/goto-instrument/reachability_slicer_class.h
+++ b/src/goto-instrument/reachability_slicer_class.h
@@ -24,22 +24,26 @@ class reachability_slicert
 public:
   void operator()(
     goto_functionst &goto_functions,
-    slicing_criteriont &criterion)
+    slicing_criteriont &criterion,
+    bool include_forward_reachability)
   {
     cfg(goto_functions);
     is_threadedt is_threaded(goto_functions);
-    fixedpoint_assertions(is_threaded, criterion);
+    fixedpoint_to_assertions(is_threaded, criterion);
+    if(include_forward_reachability)
+      fixedpoint_from_assertions(is_threaded, criterion);
     slice(goto_functions);
   }
 
 protected:
   struct slicer_entryt
   {
-    slicer_entryt():reaches_assertion(false)
+    slicer_entryt() : reaches_assertion(false), reachable_from_assertion(false)
     {
     }
 
     bool reaches_assertion;
+    bool reachable_from_assertion;
   };
 
   typedef cfg_baset<slicer_entryt> cfgt;
@@ -47,11 +51,19 @@ class reachability_slicert
 
   typedef std::stack<cfgt::entryt> queuet;
 
-  void fixedpoint_assertions(
+  void fixedpoint_to_assertions(
+    const is_threadedt &is_threaded,
+    slicing_criteriont &criterion);
+
+  void fixedpoint_from_assertions(
     const is_threadedt &is_threaded,
     slicing_criteriont &criterion);
 
   void slice(goto_functionst &goto_functions);
+
+private:
+  std::vector<cfgt::node_indext>
+  get_sources(const is_threadedt &is_threaded, slicing_criteriont &criterion);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile
index cbb784bce2d..8d649d27731 100644
--- a/src/jbmc/Makefile
+++ b/src/jbmc/Makefile
@@ -18,6 +18,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 2bf4bffba44..f70af74fdca 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -47,6 +47,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/full_slicer.h>
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
 
@@ -773,6 +774,32 @@ bool jbmc_parse_optionst::process_goto_functions(
     // this would cause the property identifiers to change.
     label_properties(goto_model);
 
+    // reachability slice?
+    if(cmdline.isset("reachability-slice-fb"))
+    {
+      if(cmdline.isset("reachability-slice"))
+      {
+        error() << "--reachability-slice and --reachability-slice-fb "
+                << "must not be given together" << eom;
+        return true;
+      }
+
+      status() << "Performing a forwards-backwards reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"), true);
+      else
+        reachability_slicer(goto_model, true);
+    }
+
+    if(cmdline.isset("reachability-slice"))
+    {
+      status() << "Performing a reachability slice" << eom;
+      if(cmdline.isset("property"))
+        reachability_slicer(goto_model, cmdline.get_values("property"));
+      else
+        reachability_slicer(goto_model);
+    }
+
     // full slice?
     if(cmdline.isset("full-slice"))
     {
@@ -857,6 +884,8 @@ void jbmc_parse_optionst::help()
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
+    HELP_REACHABILITY_SLICER
+    " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     "\n"
     "Java Bytecode frontend options:\n"
     " --classpath dir/jar          set the classpath\n"
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
index 10305b88d7d..4f4ee552029 100644
--- a/src/jbmc/jbmc_parse_options.h
+++ b/src/jbmc/jbmc_parse_options.h
@@ -38,6 +38,7 @@ class optionst;
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
+  OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):" \
   "(object-bits):" \
diff --git a/src/util/graph.h b/src/util/graph.h
index 60d56cf2600..ed67703cf9d 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -249,6 +249,9 @@ class grapht
 
   std::vector<node_indext> get_reachable(node_indext src, bool forwards) const;
 
+  std::vector<node_indext>
+  get_reachable(const std::vector<node_indext> &src, bool forwards) const;
+
   void make_chordal();
 
   // return value: number of connected subgraphs
@@ -458,15 +461,35 @@ void grapht<N>::visit_reachable(node_indext src)
     nodes[index].visited = true;
 }
 
+/// Run depth-first search on the graph, starting from a single source
+/// node.
+/// \param src The node to start the search from.
+/// \param forwards true (false) if the forward (backward) reachability
+/// should be performed.
 template<class N>
 std::vector<typename N::node_indext>
 grapht<N>::get_reachable(node_indext src, bool forwards) const
+{
+  std::vector<node_indext> src_vector;
+  src_vector.push_back(src);
+
+  return get_reachable(src_vector, forwards);
+}
+
+/// Run depth-first search on the graph, starting from multiple source
+/// nodes.
+/// \param src The nodes to start the search from.
+/// \param forwards true (false) if the forward (backward) reachability
+/// should be performed.
+template <class N>
+std::vector<typename N::node_indext> grapht<N>::get_reachable(
+  const std::vector<node_indext> &src,
+  bool forwards) const
 {
   std::vector<node_indext> result;
   std::vector<bool> visited(size(), false);
 
-  std::stack<node_indext, std::vector<node_indext>> s;
-  s.push(src);
+  std::stack<node_indext, std::vector<node_indext>> s(src);
 
   while(!s.empty())
   {