diff --git a/regression/goto-instrument/unwind-unwindset3/test.desc b/regression/goto-instrument/unwind-unwindset3/test.desc
index 01df8603ae6..58a253c1062 100644
--- a/regression/goto-instrument/unwind-unwindset3/test.desc
+++ b/regression/goto-instrument/unwind-unwindset3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 10 --unwindset main.0:-1
+--unwind 10 --unwindset main.0:
 ^Unwinding loop
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 9da2d96efc2..e1045b7bc9c 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -30,9 +30,6 @@ 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) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
@@ -43,6 +40,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
+      ../goto-instrument/nondet_static$(OBJEXT) \
+      ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/unwindset$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index ea7b3e17f30..40e552bca71 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 
 #include <util/exit_codes.h>
-#include <util/string2int.h>
-#include <util/string_utils.h>
 
 #include <langapi/language_util.h>
 
@@ -319,7 +317,8 @@ void bmct::setup()
 
   symex.last_source_location.make_nil();
 
-    setup_unwind();
+  symex.unwindset.parse_unwind(options.get_option("unwind"));
+  symex.unwindset.parse_unwindset(options.get_option("unwindset"));
 }
 
 safety_checkert::resultt bmct::execute(
@@ -549,43 +548,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
   }
 }
 
-void bmct::setup_unwind()
-{
-  const std::string &set=options.get_option("unwindset");
-  std::vector<std::string> unwindset_loops;
-  split_string(set, ',', unwindset_loops, true, true);
-
-  for(auto &val : unwindset_loops)
-  {
-    unsigned thread_nr=0;
-    bool thread_nr_set=false;
-
-    if(!val.empty() &&
-       isdigit(val[0]) &&
-       val.find(":")!=std::string::npos)
-    {
-      std::string nr=val.substr(0, val.find(":"));
-      thread_nr=unsafe_string2unsigned(nr);
-      thread_nr_set=true;
-      val.erase(0, nr.size()+1);
-    }
-
-    if(val.rfind(":")!=std::string::npos)
-    {
-      std::string id=val.substr(0, val.rfind(":"));
-      long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
-
-      if(thread_nr_set)
-        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
-      else
-        symex.set_unwind_loop_limit(id, uw);
-    }
-  }
-
-  if(options.get_option("unwind")!="")
-    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
-}
-
 /// Perform core BMC, using an abstract model to supply GOTO function bodies
 /// (perhaps created on demand).
 /// \param opts: command-line options affecting BMC
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 0e7efe46da9..a61ba9e3e6c 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -183,8 +183,6 @@ class bmct:public safety_checkert
     const goto_functionst &,
     prop_convt &);
 
-  // unwinding
-  virtual void setup_unwind();
   void do_conversion();
 
   virtual void freeze_program_variables();
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 986e368ea45..abdda442a5b 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -25,8 +25,6 @@ symex_bmct::symex_bmct(
   path_storaget &path_storage)
   : goto_symext(mh, outer_symbol_table, _target, path_storage),
     record_coverage(false),
-    max_unwind(0),
-    max_unwind_is_set(false),
     symex_coverage(ns)
 {
 }
@@ -131,25 +129,12 @@ bool symex_bmct::get_unwind(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    // We use the most specific limit we have,
-    // and 'infinity' when we have none.
+    auto limit=unwindset.get_limit(id, source.thread_nr);
 
-    loop_limitst &this_thread_limits=
-      thread_loop_limits[source.thread_nr];
-
-    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-    if(l_it!=this_thread_limits.end())
-      this_loop_limit=l_it->second;
+    if(!limit.has_value())
+      abort_unwind_decision = tvt(false);
     else
-    {
-      l_it=loop_limits.find(id);
-      if(l_it!=loop_limits.end())
-        this_loop_limit=l_it->second;
-      else if(max_unwind_is_set)
-        this_loop_limit=max_unwind;
-    }
-
-    abort_unwind_decision = tvt(unwind >= this_loop_limit);
+      abort_unwind_decision = tvt(unwind >= *limit);
   }
 
   INVARIANT(
@@ -187,25 +172,12 @@ bool symex_bmct::get_unwind_recursion(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    // We use the most specific limit we have,
-    // and 'infinity' when we have none.
-
-    loop_limitst &this_thread_limits=
-      thread_loop_limits[thread_nr];
+    auto limit=unwindset.get_limit(id, thread_nr);
 
-    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-    if(l_it!=this_thread_limits.end())
-      this_loop_limit=l_it->second;
+    if(!limit.has_value())
+      abort_unwind_decision = tvt(false);
     else
-    {
-      l_it=loop_limits.find(id);
-      if(l_it!=loop_limits.end())
-        this_loop_limit=l_it->second;
-      else if(max_unwind_is_set)
-        this_loop_limit=max_unwind;
-    }
-
-    abort_unwind_decision = tvt(unwind>this_loop_limit);
+      abort_unwind_decision = tvt(unwind > *limit);
   }
 
   INVARIANT(
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index bc43242037b..0808604118c 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/path_storage.h>
 #include <goto-symex/goto_symex.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "symex_coverage.h"
 
 class symex_bmct: public goto_symext
@@ -32,29 +34,6 @@ class symex_bmct: public goto_symext
   // To show progress
   source_locationt last_source_location;
 
-  // Control unwinding.
-
-  void set_unwind_limit(unsigned limit)
-  {
-    max_unwind=limit;
-    max_unwind_is_set=true;
-  }
-
-  void set_unwind_thread_loop_limit(
-    unsigned thread_nr,
-    const irep_idt &id,
-    unsigned limit)
-  {
-    thread_loop_limits[thread_nr][id]=limit;
-  }
-
-  void set_unwind_loop_limit(
-    const irep_idt &id,
-    unsigned limit)
-  {
-    loop_limits[id]=limit;
-  }
-
   /// Loop unwind handlers take the function ID and loop number, the unwind
   /// count so far, and an out-parameter specifying an advisory maximum, which
   /// they may set. If set the advisory maximum is set it is *only* used to
@@ -101,26 +80,12 @@ class symex_bmct: public goto_symext
 
   bool record_coverage;
 
-protected:
-  // We have
-  // 1) a global limit (max_unwind)
-  // 2) a limit per loop, all threads
-  // 3) a limit for a particular thread.
-  // 4) zero or more handler functions that can special-case particular
-  //    functions or loops
-  // We use the most specific of the above.
-
-  unsigned max_unwind;
-  bool max_unwind_is_set;
-
-  typedef std::unordered_map<irep_idt, unsigned> loop_limitst;
-  loop_limitst loop_limits;
-
-  typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
-  thread_loop_limitst thread_loop_limits;
+  unwindsett unwindset;
 
+protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop
   std::vector<loop_unwind_handlert> loop_unwind_handlers;
+
   /// Callbacks that may provide an unwind/do-not-unwind decision for a
   /// recursive call
   std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index bb4ff425daf..126151d9c03 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
+      unwindset.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index cdfa46f45d9..c8ddbf16a50 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -139,43 +139,26 @@ int goto_instrument_parse_optionst::doit()
     instrument_goto_program();
 
     {
-      bool unwind=cmdline.isset("unwind");
-      bool unwindset=cmdline.isset("unwindset");
-      bool unwindset_file=cmdline.isset("unwindset-file");
+      bool unwind_given=cmdline.isset("unwind");
+      bool unwindset_given=cmdline.isset("unwindset");
+      bool unwindset_file_given=cmdline.isset("unwindset-file");
 
-      if(unwindset && unwindset_file)
+      if(unwindset_given && unwindset_file_given)
         throw "only one of --unwindset and --unwindset-file supported at a "
               "time";
 
-      if(unwind || unwindset || unwindset_file)
+      if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        int k=-1;
+        unwindsett unwindset;
 
-        if(unwind)
-          k=std::stoi(cmdline.get_value("unwind"));
+        if(unwind_given)
+          unwindset.parse_unwind(cmdline.get_value("unwind"));
 
-        unwind_sett unwind_set;
+        if(unwindset_file_given)
+          unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
 
-        if(unwindset_file)
-        {
-          std::string us;
-          std::string fn=cmdline.get_value("unwindset-file");
-
-#ifdef _MSC_VER
-          std::ifstream file(widen(fn));
-#else
-          std::ifstream file(fn);
-#endif
-          if(!file)
-            throw "cannot open file "+fn;
-
-          std::stringstream buffer;
-          buffer << file.rdbuf();
-          us=buffer.str();
-          parse_unwindset(us, unwind_set);
-        }
-        else if(unwindset)
-          parse_unwindset(cmdline.get_value("unwindset"), unwind_set);
+        if(unwindset_given)
+          unwindset.parse_unwindset(cmdline.get_value("unwindset"));
 
         bool unwinding_assertions=cmdline.isset("unwinding-assertions");
         bool partial_loops=cmdline.isset("partial-loops");
@@ -202,7 +185,7 @@ int goto_instrument_parse_optionst::doit()
         }
 
         goto_unwindt goto_unwind;
-        goto_unwind(goto_model, unwind_set, k, unwind_strategy);
+        goto_unwind(goto_model, unwindset, unwind_strategy);
 
         goto_model.goto_functions.update();
         goto_model.goto_functions.compute_loop_numbers();
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index 01b0087c522..00beb99ddcb 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -22,40 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "loop_utils.h"
 
-void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
-{
-  assert(unwind_set.empty());
-
-  std::vector<std::string> result;
-  split_string(us, ',', result, true, true);
-  assert(!result.empty());
-
-  if(result.front().empty()) // allow empty string as unwindset
-    return;
-
-  for(std::vector<std::string>::const_iterator it=result.begin();
-      it!=result.end(); it++)
-  {
-    std::string loop;
-    std::string bound;
-
-    split_string(*it, ':', loop, bound, true);
-
-    std::string func;
-    std::string id;
-
-    split_string(loop, '.', func, id, true);
-
-    unsigned loop_id=std::stoi(id);
-    int loop_bound=std::stoi(bound);
-
-    if(loop_bound<-1)
-      throw "given unwind bound < -1";
-
-    unwind_set[func][loop_id]=loop_bound;
-  }
-}
-
 void goto_unwindt::copy_segment(
   const goto_programt::const_targett start,
   const goto_programt::const_targett end, // exclusive
@@ -290,37 +256,11 @@ void goto_unwindt::unwind(
   goto_program.destructive_insert(loop_exit, copies);
 }
 
-int goto_unwindt::get_k(
-  const irep_idt func,
-  const unsigned loop_id,
-  const int global_k,
-  const unwind_sett &unwind_set) const
-{
-  assert(global_k>=-1);
-
-  unwind_sett::const_iterator f_it=unwind_set.find(func);
-  if(f_it==unwind_set.end())
-    return global_k;
-
-  const std::map<unsigned, int> &m=f_it->second;
-  std::map<unsigned, int>::const_iterator l_it=m.find(loop_id);
-  if(l_it==m.end())
-    return global_k;
-
-  int k=l_it->second;
-  assert(k>=-1);
-
-  return k;
-}
-
 void goto_unwindt::unwind(
   goto_programt &goto_program,
-  const unwind_sett &unwind_set,
-  const int k,
+  const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
 {
-  assert(k>=-1);
-
   for(goto_programt::const_targett i_it=goto_program.instructions.begin();
       i_it!=goto_program.instructions.end();)
   {
@@ -340,12 +280,14 @@ void goto_unwindt::unwind(
     const irep_idt func=i_it->function;
     assert(!func.empty());
 
-    unsigned loop_number=i_it->loop_number;
+    const irep_idt loop_id=
+      id2string(func) + "." + std::to_string(i_it->loop_number);
 
-    int final_k=get_k(func, loop_number, k, unwind_set);
+    auto limit=unwindset.get_limit(loop_id, 0);
 
-    if(final_k==-1)
+    if(!limit.has_value())
     {
+      // no unwinding given
       i_it++;
       continue;
     }
@@ -355,7 +297,7 @@ void goto_unwindt::unwind(
     loop_exit++;
     assert(loop_exit!=goto_program.instructions.end());
 
-    unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy);
+    unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
 
     // necessary as we change the goto program in the previous line
     i_it=loop_exit;
@@ -364,12 +306,9 @@ void goto_unwindt::unwind(
 
 void goto_unwindt::operator()(
   goto_functionst &goto_functions,
-  const unwind_sett &unwind_set,
-  const int k,
+  const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
 {
-  assert(k>=-1);
-
   Forall_goto_functions(it, goto_functions)
   {
     goto_functionst::goto_functiont &goto_function=it->second;
@@ -383,7 +322,7 @@ void goto_unwindt::operator()(
 
     goto_programt &goto_program=goto_function.body;
 
-    unwind(goto_program, unwind_set, k, unwind_strategy);
+    unwind(goto_program, unwindset, unwind_strategy);
   }
 }
 
diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h
index 072c6f54267..89b8ea40c08 100644
--- a/src/goto-instrument/unwind.h
+++ b/src/goto-instrument/unwind.h
@@ -13,17 +13,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H
 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
 
+#include "unwindset.h"
+
 #include <util/json.h>
 #include <util/json_expr.h>
 #include <goto-programs/goto_model.h>
 
 class goto_modelt;
 
-// -1: do not unwind loop
-typedef std::map<irep_idt, std::map<unsigned, int>> unwind_sett;
-
-void parse_unwindset(const std::string &us, unwind_sett &unwind_set);
-
 class goto_unwindt
 {
 public:
@@ -50,44 +47,22 @@ class goto_unwindt
 
   void unwind(
     goto_programt &goto_program,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
 
   // unwind all functions
-
-  void operator()(
-    goto_functionst &goto_functions,
-    const unsigned k, // global bound
-    const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
-  {
-    const unwind_sett unwind_set;
-    operator()(goto_functions, unwind_set, k, unwind_strategy);
-  }
-
   void operator()(
     goto_functionst &,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
 
   void operator()(
     goto_modelt &goto_model,
-    const unsigned k, // global bound
-    const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
-  {
-    const unwind_sett unwind_set;
-    operator()(goto_model.goto_functions, unwind_set, k, unwind_strategy);
-  }
-
-  void operator()(
-    goto_modelt &goto_model,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
   {
     operator()(
-      goto_model.goto_functions, unwind_set, k, unwind_strategy);
+      goto_model.goto_functions, unwindset, unwind_strategy);
   }
 
   // unwind log
@@ -132,8 +107,7 @@ class goto_unwindt
   int get_k(
     const irep_idt func,
     const unsigned loop_id,
-    const int global_k,
-    const unwind_sett &unwind_set) const;
+    const unwindsett &unwindset) const;
 
   // copy goto program segment and redirect internal edges
   void copy_segment(
diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp
new file mode 100644
index 00000000000..5865494a6ed
--- /dev/null
+++ b/src/goto-instrument/unwindset.cpp
@@ -0,0 +1,99 @@
+/*******************************************************************\
+
+Module: Loop unwinding setup
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "unwindset.h"
+
+#include <util/string2int.h>
+#include <util/string_utils.h>
+#include <util/unicode.h>
+
+#include <fstream>
+#include <sstream>
+
+void unwindsett::parse_unwind(const std::string &unwind)
+{
+  if(!unwind.empty())
+    global_limit = unsafe_string2unsigned(unwind);
+}
+
+void unwindsett::parse_unwindset(const std::string &unwindset)
+{
+  std::vector<std::string> unwindset_loops;
+  split_string(unwindset, ',', unwindset_loops, true, true);
+
+  for(auto &val : unwindset_loops)
+  {
+    unsigned thread_nr = 0;
+    bool thread_nr_set = false;
+
+    if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
+    {
+      std::string nr = val.substr(0, val.find(":"));
+      thread_nr = unsafe_string2unsigned(nr);
+      thread_nr_set = true;
+      val.erase(0, nr.size() + 1);
+    }
+
+    if(val.rfind(":") != std::string::npos)
+    {
+      std::string id = val.substr(0, val.rfind(":"));
+      std::string uw_string = val.substr(val.rfind(":") + 1);
+
+      // the below initialisation makes g++-5 happy
+      optionalt<unsigned> uw(0);
+
+      if(uw_string.empty())
+        uw = { };
+      else
+        uw = unsafe_string2unsigned(uw_string);
+
+      if(thread_nr_set)
+        thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
+      else
+        loop_map[id] = uw;
+    }
+  }
+}
+
+optionalt<unsigned>
+unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
+{
+  // We use the most specific limit we have
+
+  // thread x loop
+  auto tl_it =
+    thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
+
+  if(tl_it != thread_loop_map.end())
+    return tl_it->second;
+
+  // loop
+  auto l_it = loop_map.find(loop_id);
+
+  if(l_it != loop_map.end())
+    return l_it->second;
+
+  // global, if any
+  return global_limit;
+}
+
+void unwindsett::parse_unwindset_file(const std::string &file_name)
+{
+  #ifdef _MSC_VER
+  std::ifstream file(widen(file_name));
+  #else
+  std::ifstream file(file_name);
+  #endif
+
+  if(!file)
+    throw "cannot open file "+file_name;
+
+  std::stringstream buffer;
+  buffer << file.rdbuf();
+  parse_unwindset(buffer.str());
+}
diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h
new file mode 100644
index 00000000000..3a20b2ac028
--- /dev/null
+++ b/src/goto-instrument/unwindset.h
@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+Module: Loop unwinding setup
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Loop unwinding
+
+#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
+#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
+
+#include <map>
+#include <string>
+
+#include <util/irep.h>
+#include <util/optional.h>
+
+class unwindsett
+{
+public:
+  // We have
+  // 1) a global limit
+  // 2) a limit per loop, all threads
+  // 3) a limit for a particular thread.
+  // We use the most specific of the above.
+
+  // global limit for all loops
+  void parse_unwind(const std::string &unwind);
+
+  // limit for instances of a loop
+  void parse_unwindset(const std::string &unwindset);
+
+  // queries
+  optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
+
+  // read unwindset directives from a file
+  void parse_unwindset_file(const std::string &file_name);
+
+protected:
+  optionalt<unsigned> global_limit;
+
+  // Limit for all instances of a loop.
+  // This may have 'no value'.
+  typedef std::map<irep_idt, optionalt<unsigned>> loop_mapt;
+  loop_mapt loop_map;
+
+  // separate limits per thread
+  using thread_loop_mapt =
+    std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
+  thread_loop_mapt thread_loop_map;
+};
+
+#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile
index 8d649d27731..6bdc5ad2685 100644
--- a/src/jbmc/Makefile
+++ b/src/jbmc/Makefile
@@ -17,9 +17,6 @@ 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/full_slicer$(OBJEXT) \
-      ../goto-instrument/reachability_slicer$(OBJEXT) \
-      ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
@@ -30,6 +27,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
+      ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/nondet_static$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
+      ../goto-instrument/unwindset$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \