7 files changed, 5 insertions, 8 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cdaaa0558..f10191c75 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -39,6 +39,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "util/sexpr.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
 using namespace std;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index b1fb0589c..aedd946c1 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -16,6 +16,7 @@
 
 #include "smt/dump.h"
 
+#include "base/configuration.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
 #include "preprocessing/preprocessing_pass_registry.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 0347a24ef..f0fad93fe 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/listeners.h"
 
+#include "base/configuration.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 3210de7b1..4e8dcce6c 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -26,7 +26,7 @@
 #ifndef CVC4__LOGIC_REQUEST_H
 #define CVC4__LOGIC_REQUEST_H
 
-#include "expr/kind.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 98fbfe1b3..3d306a7a2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -35,6 +35,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory.h"
 
 using namespace CVC4::theory;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 941fd111a..ed5e73d5d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -42,7 +42,6 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
-#include "smt/logic_request.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/node_command.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb8eb6ca0..53a5b7f2f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,20 +23,15 @@
 #include <vector>
 #include <map>
 
-#include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
-#include "context/cdhashset_forward.h"
 #include "context/cdlist_forward.h"
 #include "options/options.h"
-#include "smt/logic_exception.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
-#include "util/hash.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/statistics.h"
-#include "util/unsafe_interrupt_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -51,7 +46,6 @@ class TypeNode;
 struct NodeHashFunction;
 
 class NodeManager;
-class DecisionEngine;
 class TheoryEngine;
 class ProofManager;
 class UnsatCore;