5 files changed, 27 insertions, 23 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5dc618899..4c431a9b1 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -22,16 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <iostream>
 
-#include "prop/minisat/mtl/Sort.h"
-#include "prop/minisat/core/Solver.h"
-
-#include "prop/theory_proxy.h"
-#include "prop/minisat/minisat.h"
-#include "prop/options.h"
-#include "util/output.h"
-#include "expr/command.h"
+#include "base/output.h"
+#include "options/prop_options.h"
 #include "proof/proof_manager.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"
+#include "smt_util/command.h"
 
 using namespace CVC4::prop;
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index b5895de6e..3ed828f7c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -25,16 +25,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <iostream>
 
-#include "prop/minisat/mtl/Vec.h"
-#include "prop/minisat/mtl/Heap.h"
+#include "base/output.h"
+#include "context/context.h"
+#include "prop/minisat/core/SolverTypes.h"
 #include "prop/minisat/mtl/Alg.h"
+#include "prop/minisat/mtl/Heap.h"
+#include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/utils/Options.h"
-#include "prop/minisat/core/SolverTypes.h"
-
-#include "context/context.h"
+#include "smt_util/command.h"
 #include "theory/theory.h"
-#include "util/output.h"
-#include "expr/command.h"
+
 
 namespace CVC4 {
   class SatProof;
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 0df5eb123..b0d78242c 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_SolverTypes_h
 
 #include <assert.h>
-#include "util/output.h"
+#include "base/output.h"
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/Alg.h"
 #include "prop/minisat/mtl/Vec.h"
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 53ab2eccf..23a740a26 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -17,13 +17,14 @@
  **/
 
 #include "prop/minisat/minisat.h"
+
+#include "options/decision_options.h"
+#include "options/prop_options.h"
+#include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
-#include "prop/options.h"
-#include "smt/options.h"
-#include "decision/options.h"
 
-using namespace CVC4;
-using namespace CVC4::prop;
+namespace CVC4 {
+namespace prop {
 
 //// DPllMinisatSatSolver
 
@@ -270,3 +271,6 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
   d_statMaxLiterals.setData(d_minisat->max_literals);
   d_statTotLiterals.setData(d_minisat->tot_literals);
 }
+
+} /* namespace CVC4::prop */
+} /* namespace CVC4 */
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8408503e2..235c97e8f 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,11 +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 "options/prop_options.h"
+#include "proof/proof.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/minisat/simp/SimpSolver.h"
 #include "prop/minisat/utils/System.h"
-#include "prop/options.h"
-#include "proof/proof.h"
+
 using namespace CVC4;
 using namespace CVC4::Minisat;