2 files changed, 11 insertions, 6 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index fd6cf441..17b87873 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -249,6 +249,11 @@ namespace {
   cl::opt<bool>
   UseForkedSTP("use-forked-stp", 
                  cl::desc("Run STP in forked process"));
+
+  cl::opt<bool>
+  STPOptimizeDivides("stp-optimize-divides", 
+                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP"),
+                 cl::init(true));
 }
 
 
@@ -314,7 +319,7 @@ Executor::Executor(const InterpreterOptions &opts,
     stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
       ? std::min(MaxSTPTime,MaxInstructionTime)
       : std::max(MaxSTPTime,MaxInstructionTime)) {
-  STPSolver *stpSolver = new STPSolver(UseForkedSTP);
+  STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
   Solver *solver = 
     constructSolverChain(stpSolver,
                          interpreterHandler->getOutputFilename("queries.qlog"),
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 5dd24273..1d13a11d 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -420,7 +420,7 @@ private:
   bool useForkedSTP;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP);
+  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
 
   char *getConstraintLog(const Query&);
@@ -443,10 +443,10 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP) 
+STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
   : solver(_solver),
     vc(vc_createValidityChecker()),
-    builder(new STPBuilder(vc)),
+    builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP)
 {
@@ -472,8 +472,8 @@ STPSolverImpl::~STPSolverImpl() {
 
 /***/
 
-STPSolver::STPSolver(bool useForkedSTP) 
-  : Solver(new STPSolverImpl(this, useForkedSTP))
+STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
+  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
 {
 }