10 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f9e036aa3..8f1ba5fca 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,9 +21,9 @@
 #include "expr/kind.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
+#include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 #include "proof/theory_proof.h"
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 842ff60b1..27ca61cfd 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -15,7 +15,7 @@
 #include "theory/bv/abstraction.h"
 
 #include "options/bv_options.h"
-#include "smt_util/dump.h"
+#include "smt/dump.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index af080a970..9f3c34e8e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -22,7 +22,7 @@
 #include <sstream>
 
 #include "context/context.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 3ff0cda92..b02c9a740 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -14,7 +14,7 @@
 #include "theory/quantifiers/ceg_instantiator.h"
 
 #include "options/quantifiers_options.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 5790fc34a..d5ef2e290 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -14,7 +14,7 @@
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 
 #include "options/quantifiers_options.h"
-#include "smt_util/ite_removal.h"
+#include "smt/ite_removal.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c0a892926..529e69e82 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -22,7 +22,7 @@
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "theory/strings/type_enumerator.h"
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 9849dd0b9..c988c9120 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -31,9 +31,9 @@
 #include "options/options.h"
 #include "options/theory_options.h"
 #include "options/theoryof_mode.h"
+#include "smt/command.h"
+#include "smt/dump.h"
 #include "smt/logic_request.h"
-#include "smt_util/command.h"
-#include "smt_util/dump.h"
 #include "theory/logic_info.h"
 #include "theory/output_channel.h"
 #include "theory/valuation.h"
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 60716146e..45f7506de 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -28,8 +28,8 @@
 #include "options/quantifiers_options.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
+#include "smt/ite_removal.h"
 #include "smt/logic_exception.h"
-#include "smt_util/ite_removal.h"
 #include "smt_util/lemma_output_channel.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/arith_ite_utils.h"
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index cdd05c096..886aa6863 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -30,7 +30,7 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
 #include "smt_util/lemma_channels.h"
 #include "theory/atom_requests.h"
 #include "theory/bv/bv_to_bool.h"
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index e609bf703..0c2f109bb 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -17,7 +17,7 @@
 #ifndef __CVC4__THEORY__THEORY_MODEL_H
 #define __CVC4__THEORY__THEORY_MODEL_H
 
-#include "smt_util/model.h"
+#include "smt/model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"