diff --git a/include/datatype.h b/include/datatype.h
index fa097a97c..7572f84d7 100644
--- a/include/datatype.h
+++ b/include/datatype.h
@@ -16,8 +16,9 @@
 
 #pragma once
 
-#include "smt_defs.h"
+#include <string>
 
+#include "smt_defs.h"
 
 namespace smt {
 
@@ -26,7 +27,6 @@ class AbsDatatypeDecl {
  public:
   AbsDatatypeDecl(){};
   virtual ~AbsDatatypeDecl(){};
-
 };
 
 
@@ -38,19 +38,17 @@ class AbsDatatypeConstructorDecl {
   virtual bool compare(const DatatypeConstructorDecl & d) const = 0;
 };
 
-
 class AbsDatatype {
-
  public:
   AbsDatatype(){};
   virtual ~AbsDatatype(){};
-  virtual std::string get_name() const=0;
-  virtual int get_num_selectors(std::string cons) const=0;
-  virtual int get_num_constructors() const=0;
+  virtual std::string get_name() const = 0;
+  virtual int get_num_selectors(std::string cons) const = 0;
+  virtual int get_num_constructors() const = 0;
 };
 // Overloaded equivalence operators for two datatype constructor declarations
 bool operator==(const DatatypeConstructorDecl & d1,
                 const DatatypeConstructorDecl & d2);
 bool operator!=(const DatatypeConstructorDecl & d1,
                 const DatatypeConstructorDecl & d2);
-}
+}  // namespace smt
diff --git a/include/exceptions.h b/include/exceptions.h
index b6aaec3b8..9e540ce33 100644
--- a/include/exceptions.h
+++ b/include/exceptions.h
@@ -80,4 +80,3 @@ class InternalSolverException : public SmtException
   explicit InternalSolverException(const char * msg) : SmtException(msg){};
   explicit InternalSolverException(const std::string& msg) : SmtException(msg){};
 };
-
diff --git a/include/generic_datatype.h b/include/generic_datatype.h
index 9700eaeb6..8380076d1 100644
--- a/include/generic_datatype.h
+++ b/include/generic_datatype.h
@@ -1,9 +1,10 @@
 #pragma once
-#include <unordered_map>
+
+#include <functional>
+#include <string>
 #include <vector>
 
 #include "datatype.h"
-#include "exceptions.h"
 #include "generic_sort.h"
 #include "smt_defs.h"
 
diff --git a/include/generic_solver.h b/include/generic_solver.h
index ca9bba8fd..0e8f75267 100644
--- a/include/generic_solver.h
+++ b/include/generic_solver.h
@@ -23,13 +23,18 @@
 
 #pragma once
 
+#include <cstdint>
+#include <memory>
 #include <string>
 #include <unordered_map>
-#include <unordered_set>
+#include <vector>
 
-#include "generic_sort.h"
-#include "generic_term.h"
+#include "generic_datatype.h"
+#include "result.h"
+#include "smt_defs.h"
 #include "solver.h"
+#include "sort.h"
+#include "term.h"
 
 namespace smt {
 
diff --git a/include/generic_sort.h b/include/generic_sort.h
index 256a28f82..f7db7428a 100644
--- a/include/generic_sort.h
+++ b/include/generic_sort.h
@@ -16,16 +16,18 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <functional>
+#include <string>
+#include <vector>
 
 #include "exceptions.h"
-#include "generic_datatype.h"
 #include "smt_defs.h"
 #include "sort.h"
 
 namespace smt {
 
-class GenericDatatye;
 /* Helper functions for creating generic sorts */
 Sort make_uninterpreted_generic_sort(std::string name, uint64_t arity);
 Sort make_uninterpreted_generic_sort(Sort sort_cons, const SortVec& sorts);
diff --git a/include/generic_term.h b/include/generic_term.h
index 39f153830..932abed73 100644
--- a/include/generic_term.h
+++ b/include/generic_term.h
@@ -16,7 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <functional>
+#include <string>
 
 #include "ops.h"
 #include "smt_defs.h"
diff --git a/include/identity_walker.h b/include/identity_walker.h
index 0749403f4..90bf39579 100644
--- a/include/identity_walker.h
+++ b/include/identity_walker.h
@@ -16,10 +16,8 @@
 
 #pragma once
 
-#include <utility>
-
-#include "exceptions.h"
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 
 namespace smt
diff --git a/include/logging_solver.h b/include/logging_solver.h
index 3311ad05d..03ecb3140 100644
--- a/include/logging_solver.h
+++ b/include/logging_solver.h
@@ -16,11 +16,19 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <memory>
+#include <string>
+#include <unordered_map>
+
+#include "result.h"
+#include "smt_defs.h"
 #include "solver.h"
+#include "sort.h"
+#include "term.h"
 #include "term_hashtable.h"
 
-#include <string>
-
 namespace smt {
 
 class LoggingSolver : public AbsSmtSolver
diff --git a/include/logging_sort.h b/include/logging_sort.h
index 49c0688d5..e90a8ef21 100644
--- a/include/logging_sort.h
+++ b/include/logging_sort.h
@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
 #include "exceptions.h"
 #include "smt_defs.h"
 #include "sort.h"
diff --git a/include/logging_term.h b/include/logging_term.h
index e602133dd..178d6bb35 100644
--- a/include/logging_term.h
+++ b/include/logging_term.h
@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
 #include "ops.h"
 #include "smt_defs.h"
 #include "term.h"
diff --git a/include/ops.h b/include/ops.h
index 9b45e539c..61441446e 100644
--- a/include/ops.h
+++ b/include/ops.h
@@ -16,12 +16,13 @@
 
 #pragma once
 
+#include <cstddef>
 #include <cstdint>
+#include <functional>
 #include <iostream>
 #include <string>
-#include <utility>
 #include <unordered_set>
-#include <functional>
+#include <utility>
 
 namespace smt {
 
diff --git a/include/portfolio_solver.h b/include/portfolio_solver.h
index 987707211..6252e2270 100644
--- a/include/portfolio_solver.h
+++ b/include/portfolio_solver.h
@@ -17,9 +17,10 @@
 
 #include <condition_variable>
 #include <mutex>
-#include <thread>
+#include <vector>
 
-#include "smt.h"
+#include "result.h"
+#include "smt_defs.h"
 
 namespace smt {
 
diff --git a/include/printing_solver.h b/include/printing_solver.h
index 9e17a9ed0..43f7236ea 100644
--- a/include/printing_solver.h
+++ b/include/printing_solver.h
@@ -15,8 +15,13 @@
 
 #pragma once
 
+#include <cstdint>
+#include <iostream>
+#include <string>
+
+#include "smt_defs.h"
 #include "solver.h"
-#include "term_hashtable.h"
+#include "term.h"
 
 namespace smt {
 
diff --git a/include/result.h b/include/result.h
index 928258246..4aefcbadd 100644
--- a/include/result.h
+++ b/include/result.h
@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <iostream>
+#include <string>
 namespace smt
 {
 enum ResultType
diff --git a/include/smtlib_reader.h b/include/smtlib_reader.h
index 037390e18..3564e8ade 100644
--- a/include/smtlib_reader.h
+++ b/include/smtlib_reader.h
@@ -16,12 +16,21 @@
 
 #pragma once
 
-#include "assert.h"
+#include <cassert>
+#include <cstddef>
+#include <cstdint>
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
+#include <vector>
 
-#include "smt.h"
+#include "exceptions.h"
+#include "ops.h"
+#include "result.h"
+#include "smt_defs.h"
 #include "smtlibparser.h"
+#include "sort.h"
+#include "term.h"
 
 #define YY_DECL smtlib::parser::symbol_type yylex(smt::SmtLibReader & drv)
 YY_DECL;
diff --git a/include/smtlib_utils.h b/include/smtlib_utils.h
index 00fed1388..76596bc20 100644
--- a/include/smtlib_utils.h
+++ b/include/smtlib_utils.h
@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <string>
+
 /* string constants for the SMT-LIB commands */
 const std::string SET_OPTION_STR = "set-option";
 const std::string SET_LOGIC_STR = "set-logic";
diff --git a/include/smtlibparser_maps.h b/include/smtlibparser_maps.h
index 4d0ee0015..2a3830afa 100644
--- a/include/smtlibparser_maps.h
+++ b/include/smtlibparser_maps.h
@@ -1,4 +1,5 @@
 #include <string>
+#include <unordered_map>
 
 #include "ops.h"
 
diff --git a/include/solver.h b/include/solver.h
index 98317fd3b..4e19e2bc2 100644
--- a/include/solver.h
+++ b/include/solver.h
@@ -16,6 +16,7 @@
 
 #pragma once
 
+#include <cstdint>
 #include <string>
 #include <vector>
 
diff --git a/include/solver_enums.h b/include/solver_enums.h
index ec4c39404..fb0a4582c 100644
--- a/include/solver_enums.h
+++ b/include/solver_enums.h
@@ -16,6 +16,10 @@
 
 #pragma once
 
+#include <cstddef>
+#include <functional>
+#include <iostream>
+#include <string>
 #include <unordered_set>
 
 namespace smt {
diff --git a/include/solver_utils.h b/include/solver_utils.h
index 789b37831..91e808ca6 100644
--- a/include/solver_utils.h
+++ b/include/solver_utils.h
@@ -15,7 +15,8 @@
 **/
 #pragma once
 
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 
diff --git a/include/sort.h b/include/sort.h
index a3391dcbe..8d78305d5 100644
--- a/include/sort.h
+++ b/include/sort.h
@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <string>
 #include <unordered_set>
 #include <vector>
diff --git a/include/sort_inference.h b/include/sort_inference.h
index aa3efbb99..2ecdf11b4 100644
--- a/include/sort_inference.h
+++ b/include/sort_inference.h
@@ -18,10 +18,8 @@
 
 #include <unordered_set>
 
-#include "assert.h"
-#include "generic_sort.h"
-#include "ops.h"
-#include "solver.h"
+#include "smt_defs.h"
+#include "sort.h"
 #include "term.h"
 
 namespace smt {
@@ -240,4 +238,3 @@ Sort constructor_sort(Op op,
                       const SortVec & sorts);
 
 }  // namespace smt
-
diff --git a/include/sorting_network.h b/include/sorting_network.h
index 0c724722b..696c6095a 100644
--- a/include/sorting_network.h
+++ b/include/sorting_network.h
@@ -15,7 +15,8 @@
 
 #pragma once
 
-#include "smt.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 
diff --git a/include/substitution_walker.h b/include/substitution_walker.h
index cca24fbf7..fd1caade8 100644
--- a/include/substitution_walker.h
+++ b/include/substitution_walker.h
@@ -16,6 +16,8 @@
 #pragma once
 
 #include "identity_walker.h"
+#include "smt_defs.h"
+#include "term.h"
 
 namespace smt {
 // class for doing substitutions
diff --git a/include/term.h b/include/term.h
index 4674bc6f0..9f359c0b7 100644
--- a/include/term.h
+++ b/include/term.h
@@ -16,6 +16,8 @@
 
 #pragma once
 
+#include <cstddef>
+#include <cstdint>
 #include <iostream>
 #include <iterator>
 #include <list>
diff --git a/include/term_hashtable.h b/include/term_hashtable.h
index 31f98ee02..3b833ebb8 100644
--- a/include/term_hashtable.h
+++ b/include/term_hashtable.h
@@ -17,6 +17,7 @@
 
 #pragma once
 
+#include <cstddef>
 #include <unordered_map>
 
 #include "smt_defs.h"
diff --git a/include/term_translator.h b/include/term_translator.h
index a39dae3cd..9a4496670 100644
--- a/include/term_translator.h
+++ b/include/term_translator.h
@@ -16,6 +16,7 @@
 
 #pragma once
 
+#include <string>
 #include <unordered_map>
 
 #include "smt_defs.h"
diff --git a/include/tree_walker.h b/include/tree_walker.h
index b15cc8a84..46078a5f7 100644
--- a/include/tree_walker.h
+++ b/include/tree_walker.h
@@ -18,10 +18,11 @@
 
 #pragma once
 
+#include <unordered_map>
 #include <utility>
+#include <vector>
 
-#include "exceptions.h"
-#include "smt.h"
+#include "smt_defs.h"
 
 namespace smt {
 /* vector of pairs holding terms and ints that gets used within visit in the
diff --git a/include/utils.h b/include/utils.h
index ec3274970..91c93b221 100644
--- a/include/utils.h
+++ b/include/utils.h
@@ -16,12 +16,17 @@
 
 #pragma once
 
+#include <cassert>
+#include <cstddef>
 #include <iostream>
 #include <sstream>
 #include <string>
+#include <unordered_map>
 
-#include "assert.h"
-#include "smt.h"
+#include "ops.h"
+#include "smt_defs.h"
+#include "term.h"
+#include "term_translator.h"
 
 #ifndef NDEBUG
 #define _ASSERTIONS