about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp7
1 files changed, 6 insertions, 1 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"),