diff --git a/lib/cbmc b/lib/cbmc
index 2b050a0..f17599e 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit 2b050a063ee60ee88b45409d533b409cf1efc26a
+Subproject commit f17599e78ffd53553e58e4aa610a326b86cdc0b7
diff --git a/src/Makefile b/src/Makefile
index a101c9c..80d5e66 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,4 +1,4 @@
-DIRS = symex
+DIRS = symex path-symex
 CPROVER_DIR ?= lib/cbmc/src
 export CPROVER_DIR
 
diff --git a/src/path-symex/Makefile b/src/path-symex/Makefile
index 111597f..fdb2cf7 100644
--- a/src/path-symex/Makefile
+++ b/src/path-symex/Makefile
@@ -8,10 +8,10 @@ SRC = build_goto_trace.cpp \
       var_map.cpp \
       # Empty last line
 
-INCLUDES= -I ..
+INCLUDES= -I ../../$(CPROVER_DIR) -I ../
 
-include ../config.inc
-include ../common
+include ../../$(CPROVER_DIR)/config.inc
+include ../../$(CPROVER_DIR)/common
 
 CLEANFILES = path-symex$(LIBEXT)
 
diff --git a/src/symex/Makefile b/src/symex/Makefile
index 8f553c9..e391786 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -20,9 +20,18 @@ OBJ += ../../$(CPROVER_DIR)/ansi-c/ansi-c$(LIBEXT) \
        ../../$(CPROVER_DIR)/goto-symex/rewrite_union$(OBJEXT) \
        ../../$(CPROVER_DIR)/pointer-analysis/dereference$(OBJEXT) \
        ../../$(CPROVER_DIR)/goto-instrument/cover$(OBJEXT) \
-       ../../$(CPROVER_DIR)/path-symex/path-symex$(LIBEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_basic_blocks$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_filter$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_branch$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_condition$(OBJEXT)  \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_decision$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_location$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_other$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_util$(OBJEXT) \
        ../../$(CPROVER_DIR)/miniz/miniz$(OBJEXT) \
-       ../../$(CPROVER_DIR)/json/json$(LIBEXT)
+       ../../$(CPROVER_DIR)/json/json$(LIBEXT) \
+       ../path-symex/path-symex$(LIBEXT)
 
 INCLUDES= -I .. -I ../../$(CPROVER_DIR)
 
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 28b029c..c2aec7a 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>