diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
index 1344b1beb4a..f87d8d3662d 100644
--- a/jbmc/src/jbmc/Makefile
+++ b/jbmc/src/jbmc/Makefile
@@ -32,7 +32,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
       ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
       ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
       ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index bbe89ee617c..bc16c2ca851 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -116,7 +116,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
-              $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
               $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index d78b9221461..cc5be488a55 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -36,7 +36,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../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/goto-checker/CMakeLists.txt b/src/goto-checker/CMakeLists.txt
index 9b9f9698bac..7f75ff54011 100644
--- a/src/goto-checker/CMakeLists.txt
+++ b/src/goto-checker/CMakeLists.txt
@@ -3,4 +3,4 @@ add_library(goto-checker ${sources})
 
 generic_includes(goto-checker)
 
-target_link_libraries(goto-checker goto-programs goto-symex solvers util xml goto-instrument-lib)
+target_link_libraries(goto-checker goto-programs goto-symex solvers util xml)
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 92e0e3a82de..292d9c14ddc 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
 #define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
 #include <goto-symex/build_goto_trace.h>
 
 #include "incremental_goto_checker.h"
diff --git a/src/goto-checker/module_dependencies.txt b/src/goto-checker/module_dependencies.txt
index fbac8e83b49..07af9cc962d 100644
--- a/src/goto-checker/module_dependencies.txt
+++ b/src/goto-checker/module_dependencies.txt
@@ -1,7 +1,6 @@
 assembler
 cbmc # symex_bmc will be moved next
 goto-checker
-goto-instrument
 goto-programs
 goto-symex
 langapi
diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h
index 0bd396eb4c1..b8e8b3ab116 100644
--- a/src/goto-checker/multi_path_symex_only_checker.h
+++ b/src/goto-checker/multi_path_symex_only_checker.h
@@ -12,12 +12,11 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
 #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H
 
-#include "incremental_goto_checker.h"
+#include <goto-programs/unwindset.h>
 
 #include <goto-symex/path_storage.h>
 
-#include <goto-instrument/unwindset.h>
-
+#include "incremental_goto_checker.h"
 #include "symex_bmc.h"
 
 class multi_path_symex_only_checkert : public incremental_goto_checkert
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.h b/src/goto-checker/single_loop_incremental_symex_checker.h
index bcf469b70fe..e5fd98bde13 100644
--- a/src/goto-checker/single_loop_incremental_symex_checker.h
+++ b/src/goto-checker/single_loop_incremental_symex_checker.h
@@ -14,9 +14,9 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H
 
-#include <goto-symex/path_storage.h>
+#include <goto-programs/unwindset.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-symex/path_storage.h>
 
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h
index 325459e919c..aee94cbbb68 100644
--- a/src/goto-checker/single_path_symex_only_checker.h
+++ b/src/goto-checker/single_path_symex_only_checker.h
@@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
 #include <goto-symex/path_storage.h>
 
 #include "incremental_goto_checker.h"
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 56bd0c198d6..de4ecdd28b4 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -11,12 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_bmc.h"
 
-#include <limits>
-
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
+#include <limits>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp
index 7003f4ef30d..0492797d6a6 100644
--- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp
+++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp
@@ -6,13 +6,13 @@ Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <limits>
-
 #include "symex_bmc_incremental_one_loop.h"
 
 #include <util/structured_data.h>
 
-#include <goto-instrument/unwindset.h>
+#include <goto-programs/unwindset.h>
+
+#include <limits>
 
 symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   message_handlert &message_handler,
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index b33c52692f0..7349fe8bc31 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -99,7 +99,6 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
-      unwindset.cpp \
       value_set_fi_fp_removal.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index f99d87e4477..8cb69c96ed8 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -27,13 +27,13 @@ Date: February 2016
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/goto_program.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/unwindset.h>
 
 #include <analyses/local_may_alias.h>
 #include <ansi-c/c_expr.h>
 #include <goto-instrument/havoc_utils.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <langapi/language_util.h>
 
 #include "cfg_info.h"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
index 4b7302cd2c2..2bc0e1536cf 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp
@@ -20,13 +20,13 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/c_expr.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <langapi/language_util.h>
 
 #include "dfcc_cfg_info.h"
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index f9a5f51c2fe..5c8e8f2fb38 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -20,6 +20,7 @@ Author: Remi Delmas, delmarsd@amazon.com
 
 #include <goto-programs/goto_function.h>
 #include <goto-programs/goto_model.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/c_expr.h>
 #include <ansi-c/c_object_factory_parameters.h>
@@ -27,7 +28,6 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include <ansi-c/goto-conversion/goto_convert_functions.h>
 #include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/unwind.h>
-#include <goto-instrument/unwindset.h>
 #include <linking/static_lifetime_init.h>
 
 #include "dfcc_utils.h"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 5258481c270..1927f49e2bc 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/restrict_function_pointers.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/goto-conversion/goto_check_c.h>
@@ -39,7 +40,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "reachability_slicer.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
-#include "unwindset.h"
 
 #include "contracts/contracts.h"
 #include "contracts/contracts_wrangler.h"
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index c52adcdd905..c99e19f2280 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -20,8 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_functions.h>
-
-#include "unwindset.h"
+#include <goto-programs/unwindset.h>
 
 void goto_unwindt::copy_segment(
   const goto_programt::const_targett start,
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 21b06168563..bacc92ac152 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -56,6 +56,7 @@ SRC = adjust_float_expressions.cpp \
       string_abstraction.cpp \
       structured_trace_util.cpp \
       system_library_symbols.cpp \
+      unwindset.cpp \
       validate_code.cpp \
       validate_goto_model.cpp \
       vcd_goto_trace.cpp \
diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-programs/unwindset.cpp
similarity index 98%
rename from src/goto-instrument/unwindset.cpp
rename to src/goto-programs/unwindset.cpp
index 7dc097efd03..4d112e49f28 100644
--- a/src/goto-instrument/unwindset.cpp
+++ b/src/goto-programs/unwindset.cpp
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 #include <util/unicode.h>
 
-#include <goto-programs/abstract_goto_model.h>
+#include "abstract_goto_model.h"
 
 #include <algorithm>
 #include <fstream>
@@ -216,7 +216,7 @@ void unwindsett::parse_unwindset_file(
   std::ifstream file(widen_if_needed(file_name));
 
   if(!file)
-    throw "cannot open file "+file_name;
+    throw "cannot open file " + file_name;
 
   std::stringstream buffer;
   buffer << file.rdbuf();
diff --git a/src/goto-instrument/unwindset.h b/src/goto-programs/unwindset.h
similarity index 100%
rename from src/goto-instrument/unwindset.h
rename to src/goto-programs/unwindset.h
diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile
index 53d634021e3..8b85a230c80 100644
--- a/src/goto-synthesizer/Makefile
+++ b/src/goto-synthesizer/Makefile
@@ -26,7 +26,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/loop_utils$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/unwind$(OBJEXT) \
-      ../goto-instrument/unwindset$(OBJEXT) \
       ../goto-symex/goto-symex$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
diff --git a/src/libcprover-cpp/Makefile b/src/libcprover-cpp/Makefile
index 54746d50058..d1d05f89c09 100644
--- a/src/libcprover-cpp/Makefile
+++ b/src/libcprover-cpp/Makefile
@@ -25,7 +25,6 @@ OBJ += \
   ../goto-instrument/nondet_static$(OBJEXT) \
   ../goto-instrument/reachability_slicer$(OBJEXT) \
   ../goto-instrument/source_lines$(OBJEXT) \
-  ../goto-instrument/unwindset$(OBJEXT) \
   ../goto-programs/goto-programs$(LIBEXT) \
   ../goto-symex/goto-symex$(LIBEXT) \
   ../json-symtab-language/json-symtab-language$(LIBEXT) \
diff --git a/unit/Makefile b/unit/Makefile
index ebd38a5aa4b..bc93e74a34c 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -260,7 +260,6 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/goto-instrument/reachability_slicer$(OBJEXT) \
           ../src/goto-instrument/nondet_static$(OBJEXT) \
           ../src/goto-instrument/full_slicer$(OBJEXT) \
-          ../src/goto-instrument/unwindset$(OBJEXT) \
           ../src/goto-synthesizer/expr_enumerator$(OBJEXT) \
           ../src/xmllang/xmllang$(LIBEXT) \
           ../src/goto-symex/goto-symex$(LIBEXT) \
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
index 4b9ff978e99..e118a684be7 100644
--- a/unit/path_strategies.cpp
+++ b/unit/path_strategies.cpp
@@ -6,31 +6,25 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
 
 \*******************************************************************/
 
-#include <testing-utils/use_catch.h>
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/tempfile.h>
 
-#include <path_strategies.h>
-
-#include <fstream>
-#include <functional>
-#include <string>
+#include <goto-programs/unwindset.h>
 
 #include <ansi-c/ansi_c_language.h>
-
 #include <cbmc/cbmc_parse_options.h>
-
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/goto_symex_property_decider.h>
 #include <goto-checker/symex_bmc.h>
-
 #include <goto-symex/path_storage.h>
-
-#include <goto-instrument/unwindset.h>
-
 #include <langapi/mode.h>
+#include <testing-utils/use_catch.h>
 
-#include <util/cmdline.h>
-#include <util/config.h>
-#include <util/tempfile.h>
+#include <fstream>
+#include <functional>
+#include <path_strategies.h>
+#include <string>
 
 // The actual test suite.
 //