5 files changed, 9 insertions, 4 deletions
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"