diff --git a/include/exceptions.h b/include/exceptions.h
index b6aaec3b8..a973fe85c 100644
--- a/include/exceptions.h
+++ b/include/exceptions.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <exception>
diff --git a/include/ops.h b/include/ops.h
index 9b45e539c..e9acc5538 100644
--- a/include/ops.h
+++ b/include/ops.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <cstdint>
@@ -191,7 +193,7 @@ namespace std
         return str_hash(o.to_string());
       }
     };
-}
+}  // namespace std
 
 namespace smt {
 // ops that can be applied to n arguments
diff --git a/include/smt_defs.h b/include/smt_defs.h
index f2c356236..8ecd90774 100644
--- a/include/smt_defs.h
+++ b/include/smt_defs.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <memory>
@@ -42,4 +44,3 @@ class AbsDatatype;
 using Datatype = std::shared_ptr<AbsDatatype>;
 
 }  // namespace smt
-
diff --git a/include/solver.h b/include/solver.h
index 98317fd3b..1ab46ff76 100644
--- a/include/solver.h
+++ b/include/solver.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <string>
diff --git a/include/solver_enums.h b/include/solver_enums.h
index ec4c39404..331ba43a4 100644
--- a/include/solver_enums.h
+++ b/include/solver_enums.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <unordered_set>
diff --git a/include/sort.h b/include/sort.h
index a3391dcbe..eb06466ee 100644
--- a/include/sort.h
+++ b/include/sort.h
@@ -14,14 +14,14 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <string>
 #include <unordered_set>
 #include <vector>
 
-#include "ops.h"
-#include "datatype.h"
 #include "smt_defs.h"
 
 // Sort needs to have arguments
@@ -113,5 +113,4 @@ struct hash<smt::Sort>
 {
   size_t operator()(const smt::Sort & s) const { return s->hash(); }
 };
-}
-
+}  // namespace std
diff --git a/include/term.h b/include/term.h
index 4674bc6f0..2485b9e83 100644
--- a/include/term.h
+++ b/include/term.h
@@ -14,6 +14,8 @@
 **
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <iostream>
@@ -193,4 +195,3 @@ namespace std
     }
   };
 }
-
diff --git a/include/term_translator.h b/include/term_translator.h
index a39dae3cd..d57e0e1a6 100644
--- a/include/term_translator.h
+++ b/include/term_translator.h
@@ -14,6 +14,8 @@
 **        symbols, which would throw an exception).
 **/
 
+// IWYU pragma: private, include "smt.h"
+
 #pragma once
 
 #include <unordered_map>
@@ -156,4 +158,3 @@ class TermTranslator
   std::unordered_map<std::string, Sort> uninterpreted_sorts;
 };
 }  // namespace smt
-