aboutsummaryrefslogtreecommitdiffhomepage
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"),