3 files changed, 15 insertions, 13 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index ca7228ee8..5a37da27c 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -18,19 +18,20 @@ 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 "core/Solver.h"
+
 #include <math.h>
 
-#include "mtl/Sort.h"
-#include "core/Solver.h"
 #include <vector>
 #include <iostream>
 
-#include "util/output.h"
-#include "util/utility.h"
-#include "util/exception.h"
-#include "theory/bv/options.h"
-#include "smt/options.h"
+#include "base/exception.h"
+#include "base/output.h"
+#include "mtl/Sort.h"
+#include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "theory/interrupted.h"
+#include "util/utility.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index e7e489985..c5b185c95 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/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 "mtl/Sort.h"
 #include "simp/SimpSolver.h"
+
+#include "mtl/Sort.h"
+#include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "utils/System.h"
-#include "theory/bv/options.h"
-#include "smt/options.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 707f62e34..bef8e0a70 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -21,10 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_SimpSolver_h
 #define BVMinisat_SimpSolver_h
 
-#include "prop/bvminisat/mtl/Queue.h"
-#include "prop/bvminisat/core/Solver.h"
-#include "util/statistics_registry.h"
 #include "context/context.h"
+#include "expr/statistics_registry.h"
+#include "prop/bvminisat/core/Solver.h"
+#include "prop/bvminisat/mtl/Queue.h"
 
 namespace CVC4 {
 namespace BVMinisat {