1 files changed, 4 insertions, 19 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0c75a924..834f35d90 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -21,22 +21,11 @@
 #ifndef CVC4__PROP_ENGINE_H
 #define CVC4__PROP_ENGINE_H
 
-#include <sys/time.h>
-
-#include "base/modal_exception.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
-#include "options/options.h"
-#include "proof/proof_manager.h"
-#include "prop/minisat/core/Solver.h"
-#include "prop/minisat/minisat.h"
-#include "prop/proof_cnf_stream.h"
-#include "prop/prop_proof_manager.h"
-#include "prop/sat_solver_types.h"
+#include "theory/output_channel.h"
 #include "theory/trust_node.h"
-#include "theory/theory_inference_manager.h"
-#include "util/resource_manager.h"
 #include "util/result.h"
-#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
@@ -45,16 +34,12 @@ class DecisionEngine;
 class OutputManager;
 class TheoryEngine;
 
-namespace theory {
-  class TheoryRegistrar;
-}/* CVC4::theory namespace */
-
 namespace prop {
 
 class CnfStream;
 class CDCLTSatSolverInterface;
-
-class PropEngine;
+class ProofCnfStream;
+class PropPfManager;
 
 /**
  * PropEngine is the abstraction of a Sat Solver, providing methods for