diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 60e1adc98a5..873d0c2c2e3 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -962,18 +962,24 @@ bool jbmc_parse_optionst::process_goto_functions(
     log.status() << "Performing a forwards-backwards reachability slice"
                  << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"), true);
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), true, ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model, true);
+      reachability_slicer(goto_model, true, ui_message_handler);
   }
 
   if(cmdline.isset("reachability-slice"))
   {
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   // full slice?
diff --git a/regression/goto-instrument/reachability-slice/main.c b/regression/goto-instrument/reachability-slice/main.c
new file mode 100644
index 00000000000..5fcd6a1ff7a
--- /dev/null
+++ b/regression/goto-instrument/reachability-slice/main.c
@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+void undefined_function();
+
+void a()
+{
+  undefined_function();
+}
+
+void b()
+{
+  int should_be_sliced_away;
+}
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  a();
+  __CPROVER_assert(0, "reach me");
+  b();
+}
diff --git a/regression/goto-instrument/reachability-slice/test.desc b/regression/goto-instrument/reachability-slice/test.desc
new file mode 100644
index 00000000000..d7e1a6fc705
--- /dev/null
+++ b/regression/goto-instrument/reachability-slice/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--reachability-slice
+Removing call to undefined_function, which has no body
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+should_be_sliced_away
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ba9d672de8a..f1315686b26 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -944,19 +944,29 @@ bool cbmc_parse_optionst::process_goto_program(
     log.status() << "Performing a forwards-backwards reachability slice"
                  << messaget::eom;
     if(options.is_set("property"))
+    {
       reachability_slicer(
-        goto_model, options.get_list_option("property"), true);
+        goto_model,
+        options.get_list_option("property"),
+        true,
+        log.get_message_handler());
+    }
     else
-      reachability_slicer(goto_model, true);
+      reachability_slicer(goto_model, true, log.get_message_handler());
   }
 
   if(options.get_bool_option("reachability-slice"))
   {
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(options.is_set("property"))
-      reachability_slicer(goto_model, options.get_list_option("property"));
+    {
+      reachability_slicer(
+        goto_model,
+        options.get_list_option("property"),
+        log.get_message_handler());
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, log.get_message_handler());
   }
 
   // full slice?
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index a99d5caa850..2413dcb6b23 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -841,7 +841,7 @@ int goto_instrument_parse_optionst::doit()
       log.status() << "Removing calls to functions without a body"
                    << messaget::eom;
       remove_calls_no_bodyt remove_calls_no_body;
-      remove_calls_no_body(goto_model.goto_functions);
+      remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
 
       log.status() << "Accelerating" << messaget::eom;
       guard_managert guard_manager;
@@ -1066,8 +1066,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // we add the library in some cases, as some analyses benefit
 
-  if(cmdline.isset("add-library") ||
-     cmdline.isset("mm"))
+  if(
+    cmdline.isset("add-library") || cmdline.isset("mm") ||
+    cmdline.isset("reachability-slice") ||
+    cmdline.isset("reachability-slice-fb") ||
+    cmdline.isset("fp-reachability-slice"))
   {
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -1245,7 +1248,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
                  << messaget::eom;
 
     remove_calls_no_bodyt remove_calls_no_body;
-    remove_calls_no_body(goto_model.goto_functions);
+    remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
 
     goto_model.goto_functions.update();
     goto_model.goto_functions.compute_loop_numbers();
@@ -1602,9 +1605,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
 
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   if(cmdline.isset("fp-reachability-slice"))
@@ -1614,7 +1620,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     log.status() << "Performing a function pointer reachability slice"
                  << messaget::eom;
     function_path_reachability_slicer(
-      goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
+      goto_model,
+      cmdline.get_comma_separated_values("fp-reachability-slice"),
+      ui_message_handler);
   }
 
   // full slice?
@@ -1687,9 +1695,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   if(cmdline.isset("ensure-one-backedge-per-target"))
diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp
index a62caafc101..ca594ec1819 100644
--- a/src/goto-instrument/reachability_slicer.cpp
+++ b/src/goto-instrument/reachability_slicer.cpp
@@ -13,17 +13,46 @@ Author: Daniel Kroening, kroening@kroening.com
 /// (and possibly, depending on the parameters, keep those that can be reached
 /// from the criterion).
 
-#include "reachability_slicer.h"
+#include "full_slicer_class.h"
+#include "reachability_slicer_class.h"
+
+#include <util/exception_utils.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 
-#include <util/exception_utils.h>
+#include <analyses/is_threaded.h>
 
-#include "full_slicer_class.h"
-#include "reachability_slicer_class.h"
+#include "reachability_slicer.h"
+
+void reachability_slicert::operator()(
+  goto_functionst &goto_functions,
+  const slicing_criteriont &criterion,
+  bool include_forward_reachability,
+  message_handlert &message_handler)
+{
+  // Replace function calls without body by non-deterministic return values to
+  // ensure the CFG does not consider instructions after such a call to be
+  // unreachable.
+  remove_calls_no_bodyt remove_calls_no_body;
+  remove_calls_no_body(goto_functions, message_handler);
+  goto_functions.update();
+
+  cfg(goto_functions);
+  for(const auto &gf_entry : goto_functions.function_map)
+  {
+    forall_goto_program_instructions(i_it, gf_entry.second.body)
+      cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
+  }
+
+  is_threadedt is_threaded(goto_functions);
+  fixedpoint_to_assertions(is_threaded, criterion);
+  if(include_forward_reachability)
+    fixedpoint_from_assertions(is_threaded, criterion);
+  slice(goto_functions);
+}
 
 /// 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
@@ -364,13 +393,18 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
 /// \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)
+/// \param message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
-  const bool include_forward_reachability)
+  const bool include_forward_reachability,
+  message_handlert &message_handler)
 {
   reachability_slicert s;
   assert_criteriont a;
-  s(goto_model.goto_functions, a, include_forward_reachability);
+  s(goto_model.goto_functions,
+    a,
+    include_forward_reachability,
+    message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected properties.
@@ -380,14 +414,19 @@ void reachability_slicer(
 /// \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)
+/// \param message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
   const std::list<std::string> &properties,
-  const bool include_forward_reachability)
+  const bool include_forward_reachability,
+  message_handlert &message_handler)
 {
   reachability_slicert s;
   properties_criteriont p(properties);
-  s(goto_model.goto_functions, p, include_forward_reachability);
+  s(goto_model.goto_functions,
+    p,
+    include_forward_reachability,
+    message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected functions.
@@ -395,19 +434,22 @@ void reachability_slicer(
 /// \param functions_list: The functions relevant for the slicing (i.e. starting
 ///   point for the search in the CFG). Anything that is reachable in the CFG
 ///   starting from these functions will be kept.
+/// \param message_handler: message handler
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &functions_list)
+  const std::list<std::string> &functions_list,
+  message_handlert &message_handler)
 {
   for(const auto &function : functions_list)
   {
     in_function_criteriont matching_criterion(function);
     reachability_slicert slicer;
-    slicer(goto_model.goto_functions, matching_criterion, true);
+    slicer(
+      goto_model.goto_functions, matching_criterion, true, message_handler);
   }
 
   remove_calls_no_bodyt remove_calls_no_body;
-  remove_calls_no_body(goto_model.goto_functions);
+  remove_calls_no_body(goto_model.goto_functions, message_handler);
 
   goto_model.goto_functions.update();
   goto_model.goto_functions.compute_loop_numbers();
@@ -417,9 +459,12 @@ void function_path_reachability_slicer(
 /// 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)
+/// \param message_handler: message handler
+void reachability_slicer(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
-  reachability_slicer(goto_model, false);
+  reachability_slicer(goto_model, false, message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected properties. Only
@@ -427,9 +472,11 @@ void reachability_slicer(goto_modelt &goto_model)
 /// \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 message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  message_handlert &message_handler)
 {
-  reachability_slicer(goto_model, properties, false);
+  reachability_slicer(goto_model, properties, false, message_handler);
 }
diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h
index 1d112084d60..36fe5a4fef8 100644
--- a/src/goto-instrument/reachability_slicer.h
+++ b/src/goto-instrument/reachability_slicer.h
@@ -16,25 +16,30 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 class goto_modelt;
+class message_handlert;
 
-void reachability_slicer(goto_modelt &);
+void reachability_slicer(goto_modelt &, message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
-  const std::list<std::string> &properties);
+  const std::list<std::string> &properties,
+  message_handlert &);
 
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &functions_list);
+  const std::list<std::string> &functions_list,
+  message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
-  const bool include_forward_reachability);
+  const bool include_forward_reachability,
+  message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
   const std::list<std::string> &properties,
-  const bool include_forward_reachability);
+  const bool include_forward_reachability,
+  message_handlert &);
 
 // clang-format off
 #define OPT_REACHABILITY_SLICER                                                \
diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h
index 5bf92eab263..f6831e71c5e 100644
--- a/src/goto-instrument/reachability_slicer_class.h
+++ b/src/goto-instrument/reachability_slicer_class.h
@@ -12,11 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
 
-#include <goto-programs/goto_functions.h>
-#include <goto-programs/cfg.h>
-
-#include <analyses/is_threaded.h>
+#include <goto-programs/goto_program.h>
 
+class goto_functionst;
+class message_handlert;
 class slicing_criteriont;
 
 class reachability_slicert
@@ -25,21 +24,8 @@ class reachability_slicert
   void operator()(
     goto_functionst &goto_functions,
     const slicing_criteriont &criterion,
-    bool include_forward_reachability)
-  {
-    cfg(goto_functions);
-    for(const auto &gf_entry : goto_functions.function_map)
-    {
-      forall_goto_program_instructions(i_it, gf_entry.second.body)
-        cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
-    }
-
-    is_threadedt is_threaded(goto_functions);
-    fixedpoint_to_assertions(is_threaded, criterion);
-    if(include_forward_reachability)
-      fixedpoint_from_assertions(is_threaded, criterion);
-    slice(goto_functions);
-  }
+    bool include_forward_reachability,
+    message_handlert &);
 
 protected:
   struct slicer_entryt
diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp
index 857d04d1f37..3384430a310 100644
--- a/src/goto-programs/remove_calls_no_body.cpp
+++ b/src/goto-programs/remove_calls_no_body.cpp
@@ -12,6 +12,7 @@ Author: Daniel Poetzl
 #include "remove_calls_no_body.h"
 
 #include <util/invariant.h>
+#include <util/message.h>
 #include <util/std_code.h>
 
 #include "goto_functions.h"
@@ -94,14 +95,21 @@ bool remove_calls_no_bodyt::is_opaque_function_call(
 /// \param goto_program: goto program to operate on
 /// \param goto_functions: all goto functions; for looking up functions which
 ///   the goto program may call
-void remove_calls_no_bodyt::
-operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
+/// \param message_handler: message handler
+void remove_calls_no_bodyt::operator()(
+  goto_programt &goto_program,
+  const goto_functionst &goto_functions,
+  message_handlert &message_handler)
 {
   for(goto_programt::targett it = goto_program.instructions.begin();
       it != goto_program.instructions.end();) // no it++
   {
     if(is_opaque_function_call(it, goto_functions))
     {
+      messaget log{message_handler};
+      log.status() << "Removing call to "
+                   << to_symbol_expr(it->call_function()).get_identifier()
+                   << ", which has no body" << messaget::eom;
       remove_call_no_body(
         goto_program, it, it->call_lhs(), it->call_arguments());
     }
@@ -116,10 +124,13 @@ operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
 /// of the arguments of the call and a nondet assignment to the variable taking
 /// the return value.
 /// \param goto_functions: goto functions to operate on
-void remove_calls_no_bodyt::operator()(goto_functionst &goto_functions)
+/// \param message_handler: message handler
+void remove_calls_no_bodyt::operator()(
+  goto_functionst &goto_functions,
+  message_handlert &message_handler)
 {
   for(auto &gf_entry : goto_functions.function_map)
   {
-    (*this)(gf_entry.second.body, goto_functions);
+    (*this)(gf_entry.second.body, goto_functions, message_handler);
   }
 }
diff --git a/src/goto-programs/remove_calls_no_body.h b/src/goto-programs/remove_calls_no_body.h
index 9b7382328ce..3a18adb66f9 100644
--- a/src/goto-programs/remove_calls_no_body.h
+++ b/src/goto-programs/remove_calls_no_body.h
@@ -15,6 +15,7 @@ Author: Daniel Poetzl
 #include "goto_program.h"
 
 class goto_functionst;
+class message_handlert;
 
 class remove_calls_no_bodyt
 {
@@ -32,9 +33,10 @@ class remove_calls_no_bodyt
 public:
   void operator()(
     goto_programt &goto_program,
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions,
+    message_handlert &);
 
-  void operator()(goto_functionst &goto_functions);
+  void operator()(goto_functionst &goto_functions, message_handlert &);
 };
 
 #define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)"