diff --git a/doc/architectural/restrict-function-pointer.md b/doc/architectural/restrict-function-pointer.md
index 5b63b2b0c1a..9ef90cb2547 100644
--- a/doc/architectural/restrict-function-pointer.md
+++ b/doc/architectural/restrict-function-pointer.md
@@ -73,9 +73,12 @@ function where function pointers are being called, to this pattern:
 ```
 <function-name>.function_pointer_call.<N>
 ```
-
 where `N` is referring to which function call it is - so the first call to a
-function pointer in a function will have `N=1`, the 5th `N=5` etc.
+function pointer in a function will have `N=1`, the 5th `N=5` etc, or
+```
+<function-name>.<label>
+```
+when the function call is labelled.
 
 We can call `goto-instrument --restrict-function-pointer
 call.function_pointer_call.1/f,g in.gb out.gb`. This can be read as
diff --git a/regression/cbmc/unwindset1/label.desc b/regression/cbmc/unwindset1/label.desc
new file mode 100644
index 00000000000..6515b21f9a7
--- /dev/null
+++ b/regression/cbmc/unwindset1/label.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwindset main.for_loop:2,main.1:6
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/unwindset1/main.c b/regression/cbmc/unwindset1/main.c
new file mode 100644
index 00000000000..61b696d9bec
--- /dev/null
+++ b/regression/cbmc/unwindset1/main.c
@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+for_loop:
+  for(int i = 0; i < x; ++i)
+    --x;
+  for(int j = 0; j < 5; ++j)
+    ++x;
+  __CPROVER_assert(0, "can be reached");
+}
diff --git a/regression/cbmc/unwindset1/test.desc b/regression/cbmc/unwindset1/test.desc
new file mode 100644
index 00000000000..bfb173f37d7
--- /dev/null
+++ b/regression/cbmc/unwindset1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwindset main.0:2,main.2:2
+^Invalid User Input$
+^Option: unwindset$
+^Reason: invalid loop identifier main\.2$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/restrict-function-pointer-by-label/test.c b/regression/goto-instrument/restrict-function-pointer-by-label/test.c
new file mode 100644
index 00000000000..cbb70aa7f46
--- /dev/null
+++ b/regression/goto-instrument/restrict-function-pointer-by-label/test.c
@@ -0,0 +1,29 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(int);
+
+void use_f(fptr_t fptr)
+{
+labelled_call:
+  assert(fptr(10) == 11);
+}
+
+int f(int x)
+{
+  return x + 1;
+}
+
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int one = 1;
+
+  // We take the address of f and g. In this case remove_function_pointers()
+  // would create a case distinction involving both f and g in the function
+  // use_f() above.
+  use_f(one ? f : g);
+}
diff --git a/regression/goto-instrument/restrict-function-pointer-by-label/test.desc b/regression/goto-instrument/restrict-function-pointer-by-label/test.desc
new file mode 100644
index 00000000000..7bf9b38bc03
--- /dev/null
+++ b/regression/goto-instrument/restrict-function-pointer-by-label/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--restrict-function-pointer use_f.labelled_call/f
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the function f is called for the first function pointer
+call in function use_f when using the label to refer to the call site.
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp
index c3f48c85b4b..11d03e18bcd 100644
--- a/src/goto-checker/multi_path_symex_only_checker.cpp
+++ b/src/goto-checker/multi_path_symex_only_checker.cpp
@@ -28,13 +28,15 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
       equation,
       options,
       path_storage,
-      guard_manager)
+      guard_manager,
+      unwindset)
 {
   setup_symex(symex, ns, options, ui_message_handler);
 }
diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h
index 32db628521d..0bd396eb4c1 100644
--- a/src/goto-checker/multi_path_symex_only_checker.h
+++ b/src/goto-checker/multi_path_symex_only_checker.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "symex_bmc.h"
 
 class multi_path_symex_only_checkert : public incremental_goto_checkert
@@ -35,6 +37,7 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symex_target_equationt equation;
   guard_managert guard_manager;
   path_fifot path_storage; // should go away
+  unwindsett unwindset;
   symex_bmct symex;
 
   /// Generates the equation by running goto-symex
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp
index 02755b3f022..6369847c30b 100644
--- a/src/goto-checker/single_loop_incremental_symex_checker.cpp
+++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp
@@ -30,6 +30,7 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
@@ -37,6 +38,7 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
       options,
       path_storage,
       guard_manager,
+      unwindset,
       ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.h b/src/goto-checker/single_loop_incremental_symex_checker.h
index ad76495d7e9..bcf469b70fe 100644
--- a/src/goto-checker/single_loop_incremental_symex_checker.h
+++ b/src/goto-checker/single_loop_incremental_symex_checker.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "incremental_goto_checker.h"
@@ -57,6 +59,7 @@ class single_loop_incremental_symex_checkert : public incremental_goto_checkert,
   symex_target_equationt equation;
   path_fifot path_storage; // should go away
   guard_managert guard_manager;
+  unwindsett unwindset;
   symex_bmc_incremental_one_loopt symex;
   bool initial_equation_generated = false;
   bool full_equation_generated = false;
diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp
index a9347ca5dcf..01a65fb5011 100644
--- a/src/goto-checker/single_path_symex_only_checker.cpp
+++ b/src/goto-checker/single_path_symex_only_checker.cpp
@@ -30,7 +30,8 @@ single_path_symex_only_checkert::single_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     worklist(get_path_strategy(options.get_option("exploration-strategy"))),
-    symex_runtime(0)
+    symex_runtime(0),
+    unwindset(goto_model)
 {
 }
 
@@ -70,7 +71,8 @@ void single_path_symex_only_checkert::initialize_worklist()
     equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.initialize_path_storage_from_entry_point_of(
@@ -95,7 +97,8 @@ bool single_path_symex_only_checkert::resume_path(path_storaget::patht &path)
     path.equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.resume_symex_from_saved_state(
diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h
index 8370b21b86f..1732a76881a 100644
--- a/src/goto-checker/single_path_symex_only_checker.h
+++ b/src/goto-checker/single_path_symex_only_checker.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include <chrono>
 
 class symex_bmct;
@@ -40,6 +42,7 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
   guard_managert guard_manager;
   std::unique_ptr<path_storaget> worklist;
   std::chrono::duration<double> symex_runtime;
+  unwindsett unwindset;
 
   void equation_output(
     const symex_bmct &symex,
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 9bbf129a0b4..0fdaa6766ea 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -16,13 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
   const optionst &options,
   path_storaget &path_storage,
-  guard_managert &guard_manager)
+  guard_managert &guard_manager,
+  unwindsett &unwindset)
   : goto_symext(
       mh,
       outer_symbol_table,
@@ -33,6 +36,7 @@ symex_bmct::symex_bmct(
     record_coverage(!options.get_option("symex-coverage-report").empty()),
     havoc_bodyless_functions(
       options.get_bool_option("havoc-undefined-functions")),
+    unwindset(unwindset),
     symex_coverage(ns)
 {
 }
diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h
index 4f7829dea03..5e0958c7e0f 100644
--- a/src/goto-checker/symex_bmc.h
+++ b/src/goto-checker/symex_bmc.h
@@ -16,10 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/goto_symex.h>
 
-#include <goto-instrument/unwindset.h>
-
 #include "symex_coverage.h"
 
+class unwindsett;
+
 class symex_bmct : public goto_symext
 {
 public:
@@ -29,7 +29,8 @@ class symex_bmct : public goto_symext
     symex_target_equationt &_target,
     const optionst &options,
     path_storaget &path_storage,
-    guard_managert &guard_manager);
+    guard_managert &guard_manager,
+    unwindsett &unwindset);
 
   // To show progress
   source_locationt last_source_location;
@@ -81,7 +82,7 @@ class symex_bmct : public goto_symext
   const bool record_coverage;
   const bool havoc_bodyless_functions;
 
-  unwindsett unwindset;
+  unwindsett &unwindset;
 
 protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop
diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp
index c1e12394578..f50264c703f 100644
--- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp
+++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp
@@ -12,6 +12,8 @@ Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
 
 #include <util/structured_data.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   message_handlert &message_handler,
   const symbol_tablet &outer_symbol_table,
@@ -19,6 +21,7 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   const optionst &options,
   path_storaget &path_storage,
   guard_managert &guard_manager,
+  unwindsett &unwindset,
   ui_message_handlert::uit output_ui)
   : symex_bmct(
       message_handler,
@@ -26,7 +29,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
       target,
       options,
       path_storage,
-      guard_manager),
+      guard_manager,
+      unwindset),
     incr_loop_id(options.get_option("incremental-loop")),
     incr_max_unwind(
       options.is_set("unwind-max") ? options.get_signed_int_option("unwind-max")
diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.h b/src/goto-checker/symex_bmc_incremental_one_loop.h
index 9c3bc7ed14e..b5081081617 100644
--- a/src/goto-checker/symex_bmc_incremental_one_loop.h
+++ b/src/goto-checker/symex_bmc_incremental_one_loop.h
@@ -22,6 +22,7 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const optionst &,
     path_storaget &,
     guard_managert &,
+    unwindsett &,
     ui_message_handlert::uit output_ui);
 
   /// Return true if symex can be resumed
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 44682fcf7fa..d1a8f011575 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -165,7 +165,7 @@ int goto_instrument_parse_optionst::doit()
 
       if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        unwindsett unwindset;
+        unwindsett unwindset{goto_model};
 
         if(unwind_given)
           unwindset.parse_unwind(cmdline.get_value("unwind"));
diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp
index 364f3688e7e..9ecc80d5da1 100644
--- a/src/goto-instrument/unwindset.cpp
+++ b/src/goto-instrument/unwindset.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "unwindset.h"
 
+#include <util/exception_utils.h>
 #include <util/string2int.h>
 #include <util/string_utils.h>
 
@@ -44,6 +45,91 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
   if(last_c_pos != std::string::npos)
   {
     std::string id = val.substr(0, last_c_pos);
+
+    // The loop id can take three forms:
+    // 1) Just a function name to limit recursion.
+    // 2) F.N where F is a function name and N is a loop number.
+    // 3) F.L where F is a function name and L is a label.
+    const symbol_tablet &symbol_table = goto_model.get_symbol_table();
+    const symbolt *maybe_fn = symbol_table.lookup(id);
+    if(maybe_fn && maybe_fn->type.id() == ID_code)
+    {
+      // ok, recursion limit
+    }
+    else
+    {
+      auto last_dot_pos = val.rfind('.');
+      if(last_dot_pos == std::string::npos)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "invalid loop identifier " + id, "unwindset"};
+      }
+
+      std::string function_id = id.substr(0, last_dot_pos);
+      std::string loop_nr_label = id.substr(last_dot_pos + 1);
+
+      if(loop_nr_label.empty() || !goto_model.can_produce_function(function_id))
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "invalid loop identifier " + id, "unwindset"};
+      }
+
+      const goto_functiont &goto_function =
+        goto_model.get_goto_function(function_id);
+      if(isdigit(loop_nr_label[0]))
+      {
+        auto nr = string2optional_unsigned(loop_nr_label);
+        if(!nr.has_value())
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "invalid loop identifier " + id, "unwindset"};
+        }
+
+        bool found = std::any_of(
+          goto_function.body.instructions.begin(),
+          goto_function.body.instructions.end(),
+          [&nr](const goto_programt::instructiont &instruction) {
+            return instruction.is_backwards_goto() &&
+                   instruction.loop_number == nr;
+          });
+        if(!found)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "invalid loop identifier " + id, "unwindset"};
+        }
+      }
+      else
+      {
+        optionalt<unsigned> nr;
+        optionalt<source_locationt> location;
+        for(const auto &instruction : goto_function.body.instructions)
+        {
+          if(
+            std::find(
+              instruction.labels.begin(),
+              instruction.labels.end(),
+              loop_nr_label) != instruction.labels.end())
+          {
+            location = instruction.source_location();
+          }
+          if(
+            location.has_value() && instruction.is_backwards_goto() &&
+            instruction.source_location() == *location)
+          {
+            nr = instruction.loop_number;
+            break;
+          }
+        }
+        if(!nr.has_value())
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "loop identifier " + id + " does not match any loop", "unwindset"};
+        }
+        else
+          id = function_id + "." + std::to_string(*nr);
+      }
+    }
+
     std::string uw_string = val.substr(last_c_pos + 1);
 
     // the below initialisation makes g++-5 happy
diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h
index 4a0b924a6c7..aecca17d132 100644
--- a/src/goto-instrument/unwindset.h
+++ b/src/goto-instrument/unwindset.h
@@ -12,13 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 
+#include <goto-programs/goto_model.h>
+
 #include <list>
 #include <map>
 #include <string>
 
-#include <util/irep.h>
-#include <util/optional.h>
-
 class unwindsett
 {
 public:
@@ -27,6 +26,9 @@ class unwindsett
   // 2) a limit per loop, all threads
   // 3) a limit for a particular thread.
   // We use the most specific of the above.
+  explicit unwindsett(abstract_goto_modelt &goto_model) : goto_model(goto_model)
+  {
+  }
 
   // global limit for all loops
   void parse_unwind(const std::string &unwind);
@@ -41,6 +43,8 @@ class unwindsett
   void parse_unwindset_file(const std::string &file_name);
 
 protected:
+  abstract_goto_modelt &goto_model;
+
   optionalt<unsigned> global_limit;
 
   // Limit for all instances of a loop.
diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
index 93de4bf8ea7..b51266f406e 100644
--- a/src/goto-programs/restrict_function_pointers.cpp
+++ b/src/goto-programs/restrict_function_pointers.cpp
@@ -238,7 +238,8 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
 function_pointer_restrictionst::restrictionst
 function_pointer_restrictionst::parse_function_pointer_restrictions(
   const std::list<std::string> &restriction_opts,
-  const std::string &option)
+  const std::string &option,
+  const goto_modelt &goto_model)
 {
   auto function_pointer_restrictions =
     function_pointer_restrictionst::restrictionst{};
@@ -246,7 +247,7 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
   for(const std::string &restriction_opt : restriction_opts)
   {
     const auto restriction =
-      parse_function_pointer_restriction(restriction_opt, option);
+      parse_function_pointer_restriction(restriction_opt, option, goto_model);
 
     const bool inserted = function_pointer_restrictions
                             .emplace(restriction.first, restriction.second)
@@ -265,10 +266,11 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
 
 function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
   parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts)
+    const std::list<std::string> &restriction_opts,
+    const goto_modelt &goto_model)
 {
   return parse_function_pointer_restrictions(
-    restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
+    restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT, goto_model);
 }
 
 function_pointer_restrictionst::restrictionst
@@ -292,7 +294,8 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
 function_pointer_restrictionst::restrictiont
 function_pointer_restrictionst::parse_function_pointer_restriction(
   const std::string &restriction_opt,
-  const std::string &option)
+  const std::string &option,
+  const goto_modelt &goto_model)
 {
   // the format for restrictions is <pointer_name>/<target[,more_targets]*>
   // exactly one pointer and at least one target
@@ -321,7 +324,52 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
       "couldn't find target name before '/' in `" + restriction_opt + "'"};
   }
 
-  auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
+  auto pointer_name = restriction_opt.substr(0, pointer_name_end);
+  const auto last_dot = pointer_name.rfind('.');
+  if(
+    last_dot != std::string::npos && last_dot + 1 != pointer_name.size() &&
+    !isdigit(pointer_name[last_dot + 1]))
+  {
+    const auto function_id = pointer_name.substr(0, last_dot);
+    const auto label = pointer_name.substr(last_dot + 1);
+
+    bool found = false;
+    const auto it = goto_model.goto_functions.function_map.find(function_id);
+    if(it != goto_model.goto_functions.function_map.end())
+    {
+      optionalt<source_locationt> location;
+      for(const auto &instruction : it->second.body.instructions)
+      {
+        if(
+          std::find(
+            instruction.labels.begin(), instruction.labels.end(), label) !=
+          instruction.labels.end())
+        {
+          location = instruction.source_location();
+        }
+
+        if(
+          instruction.is_function_call() &&
+          instruction.call_function().id() == ID_dereference &&
+          location.has_value() && instruction.source_location() == *location)
+        {
+          auto const &called_function_pointer =
+            to_dereference_expr(instruction.call_function()).pointer();
+          pointer_name =
+            id2string(to_symbol_expr(called_function_pointer).get_identifier());
+          found = true;
+          break;
+        }
+      }
+    }
+    if(!found)
+    {
+      throw invalid_restriction_exceptiont{"non-existent pointer name " +
+                                             pointer_name,
+                                           restriction_format_message};
+    }
+  }
+
   auto const target_names_substring =
     restriction_opt.substr(pointer_name_end + 1);
   auto const target_name_strings = split_string(target_names_substring, ',');
@@ -405,7 +453,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
   try
   {
     commandline_restrictions =
-      parse_function_pointer_restrictions_from_command_line(restriction_opts);
+      parse_function_pointer_restrictions_from_command_line(
+        restriction_opts, goto_model);
     typecheck_function_pointer_restrictions(
       goto_model, commandline_restrictions);
   }
@@ -549,7 +598,9 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
 {
   function_pointer_restrictionst::restrictionst by_name_restrictions =
     parse_function_pointer_restrictions(
-      restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
+      restriction_name_opts,
+      "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
+      goto_model);
 
   function_pointer_restrictionst::restrictionst restrictions;
   for(auto const &goto_function : goto_model.goto_functions.function_map)
diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h
index 5a44a96b9f6..33845ac3503 100644
--- a/src/goto-programs/restrict_function_pointers.h
+++ b/src/goto-programs/restrict_function_pointers.h
@@ -115,15 +115,18 @@ class function_pointer_restrictionst
     message_handlert &message_handler);
 
   static restrictionst parse_function_pointer_restrictions_from_command_line(
-    const std::list<std::string> &restriction_opts);
+    const std::list<std::string> &restriction_opts,
+    const goto_modelt &goto_model);
 
   static restrictionst parse_function_pointer_restrictions(
     const std::list<std::string> &restriction_opts,
-    const std::string &option);
+    const std::string &option,
+    const goto_modelt &goto_model);
 
   static restrictiont parse_function_pointer_restriction(
     const std::string &restriction_opt,
-    const std::string &option);
+    const std::string &option,
+    const goto_modelt &goto_model);
 
   static optionalt<restrictiont> get_by_name_restriction(
     const goto_functiont &goto_function,
diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp
index 8015b3bcbd6..807a047f70c 100644
--- a/unit/goto-programs/restrict_function_pointers.cpp
+++ b/unit/goto-programs/restrict_function_pointers.cpp
@@ -24,9 +24,11 @@ class fp_restrictionst : public function_pointer_restrictionst
 
 void restriction_parsing_test()
 {
+  goto_modelt goto_model;
+
   {
     const auto res = fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2", "test");
+      "func1/func2", "test", goto_model);
     REQUIRE(res.first == "func1");
     REQUIRE(res.second.size() == 1);
     REQUIRE(res.second.find("func2") != res.second.end());
@@ -34,7 +36,7 @@ void restriction_parsing_test()
 
   {
     const auto res = fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2,func3", "test");
+      "func1/func2,func3", "test", goto_model);
     REQUIRE(res.first == "func1");
     REQUIRE(res.second.size() == 2);
     REQUIRE(res.second.find("func2") != res.second.end());
@@ -42,29 +44,33 @@ void restriction_parsing_test()
   }
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("/func", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "/func", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func/", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func/", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
-    fp_restrictionst::parse_function_pointer_restriction("func/,", "test"),
+    fp_restrictionst::parse_function_pointer_restriction(
+      "func/,", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
-      "func1/func2,", "test"),
+      "func1/func2,", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 
   REQUIRE_THROWS_AS(
     fp_restrictionst::parse_function_pointer_restriction(
-      "func1/,func2", "test"),
+      "func1/,func2", "test", goto_model),
     fp_restrictionst::invalid_restriction_exceptiont);
 }
 
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 4720883bfb6..95b9d442b47 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -24,6 +24,8 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include <langapi/mode.h>
 
 #include <util/cmdline.h>
@@ -408,6 +410,7 @@ void _check_with_strategy(
   propertiest properties(initialize_properties(goto_model));
   std::unique_ptr<path_storaget> worklist = get_path_strategy(strategy);
   guard_managert guard_manager;
+  unwindsett unwindset{goto_model};
 
   {
     // Put initial state into the work list
@@ -418,7 +421,8 @@ void _check_with_strategy(
       equation,
       options,
       *worklist,
-      guard_manager);
+      guard_manager,
+      unwindset);
     setup_symex(symex, ns, options, ui_message_handler);
 
     symex.initialize_path_storage_from_entry_point_of(
@@ -438,7 +442,8 @@ void _check_with_strategy(
       resume.equation,
       options,
       *worklist,
-      guard_manager);
+      guard_manager,
+      unwindset);
     setup_symex(symex, ns, options, ui_message_handler);
 
     symex.resume_symex_from_saved_state(