5 files changed, 18 insertions, 23 deletions
diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt
index ff696b403..39e503a81 100644
--- a/examples/hashsmt/CMakeLists.txt
+++ b/examples/hashsmt/CMakeLists.txt
@@ -1,13 +1,11 @@
-include_directories(.)
-
-set(EXAMPLES_HASHSMT_LINK_LIBS cvc4)
-
 if(Boost_FOUND)
    cvc4_add_example(sha1_inversion
-     "sha1_inversion.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
-     "a" "sha1_inversion.outfile")  # arguments to binary (for testing)
+     "sha1_inversion.cpp word.cpp" "hashsmt"
+     # arguments to binary (for testing)
+     "a" "sha1_inversion.outfile")
 endif()
 
 cvc4_add_example(sha1_collision
-  "sha1_collision.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
-  "1" "1" "sha1_collision.outfile")  # arguments to binary (for testing)
+  "sha1_collision.cpp word.cpp" "hashsmt"
+  # arguments to binary (for testing)
+  "1" "1" "sha1_collision.outfile")
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index e26b2623b..ea93db144 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -27,11 +27,10 @@
 #include <sstream>
 #include <string>
 
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
 #include "sha1.hpp"
-#include "smt/command.h"
 #include "word.h"
 
 using namespace std;
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 667c3c4e0..b53f4b149 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -35,11 +35,11 @@
 #include <string>
 #include <vector>
 
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/set_language.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
+
 #include "sha1.hpp"
-#include "smt/command.h"
 #include "word.h"
 
 using namespace std;
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 189eaf485..b26e3b4d3 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -26,10 +26,10 @@
 
 #include <vector>
 
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
-#include "options/language.h"
-#include "options/options.h"
+#include <cvc4/cvc4.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/language.h>
+#include <cvc4/options/options.h>
 
 using namespace std;
 using namespace hashsmt;
diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h
index cbe53d549..ad08a63ae 100644
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -28,9 +28,7 @@
 #include <string>
 #include <iostream>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "options/options.h"
+#include <cvc4/cvc4.h>
 
 namespace hashsmt {