13 files changed, 30 insertions, 18 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 936778e0d..54e3f2e8b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -19,6 +19,7 @@
 #include "prop/bvminisat/bvminisat.h"
 
 #include "prop/bvminisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ec8c3455a..20724efd2 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -21,6 +21,7 @@
 #pragma once
 
 #include "context/cdo.h"
+#include "proof/clause_id.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
 #include "util/statistics_registry.h"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 2100160de..d626a5d15 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -30,11 +30,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
-#include "theory/interrupted.h"
-#include "proof/proof_manager.h"
 #include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "proof/sat_proof_implementation.h"
+#include "theory/interrupted.h"
 #include "util/utility.h"
 
 namespace CVC4 {
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 019c09bcd..555495149 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -21,20 +21,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_Solver_h
 #define BVMinisat_Solver_h
 
+#include <ext/hash_set>
+#include <vector>
+
+#include "context/context.h"
+#include "proof/clause_id.h"
+#include "proof/sat_proof.h"
 #include "prop/bvminisat/core/SolverTypes.h"
-#include "prop/bvminisat/mtl/Vec.h"
-#include "prop/bvminisat/mtl/Heap.h"
 #include "prop/bvminisat/mtl/Alg.h"
+#include "prop/bvminisat/mtl/Heap.h"
+#include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/Options.h"
-#include "context/cdhashmap.h"
-#include "proof/sat_proof.h"
 
-#include <ext/hash_set>
-#include <vector>
 
 namespace CVC4 {
 
-typedef unsigned ClauseId;
 namespace BVMinisat {
 class Solver;
 }
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 311ed1dd1..cb5929320 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,8 +23,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
-#include "utils/System.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
+#include "utils/System.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 5f6f46b91..9854bf77d 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define BVMinisat_SimpSolver_h
 
 #include "context/context.h"
+#include "proof/clause_id.h"
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
 #include "util/statistics_registry.h"
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index d54848d26..9bc352f9b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -15,6 +15,8 @@
  ** A CNF converter that takes in asserts and has the side effect
  ** of given an equisatisfiable stream of assertions to PropEngine.
  **/
+#include "prop/cnf_stream.h"
+
 #include <queue>
 
 #include "base/cvc4_assert.h"
@@ -22,10 +24,10 @@
 #include "expr/expr.h"
 #include "expr/node.h"
 #include "options/bv_options.h"
+#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
-#include "proof/cnf_proof.h"
-#include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b7fb1603d..b13448bb2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -18,21 +18,22 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/core/Solver.h"
+
 #include <math.h>
 
 #include <iostream>
 
 #include "base/output.h"
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
-#include "prop/minisat/core/Solver.h"
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
 
-
 using namespace CVC4::prop;
 
 namespace CVC4 {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 777fb1093..99c47e045 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/output.h"
 #include "context/context.h"
+#include "proof/clause_id.h"
 #include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
 #include "prop/minisat/mtl/Heap.h"
@@ -43,7 +44,6 @@ namespace prop {
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
-typedef unsigned ClauseId;
 
 namespace CVC4 {
 namespace Minisat {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 739d9087a..bfbf9da6f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5bdaea950..9b551fa70 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,10 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "prop/minisat/simp/SimpSolver.h"
+
 #include "options/prop_options.h"
+#include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
-#include "prop/minisat/simp/SimpSolver.h"
 #include "prop/minisat/utils/System.h"
 
 using namespace CVC4;
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a19bec1ef..a995c1357 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
+#include "proof/clause_id.h"
 #include "prop/minisat/mtl/Queue.h"
 #include "prop/minisat/core/Solver.h"
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1383308a3..99e981220 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,6 +26,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
 
@@ -37,8 +38,6 @@ namespace prop {
 
 class TheoryProxy;
 
-typedef unsigned ClauseId;
-
 class SatSolver {
 
 public: