diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 16:14:41 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 16:14:41 +0000 |
| commit | bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c (patch) | |
| tree | 717d4f98ebe8d42aac3355af6b8c018485c1ac44 /include | |
| parent | 2624f435755c9de3632019fcd2ec68425a39c9e8 (diff) | |
| download | klee-bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c.tar.gz | |
Added --stp-optimize-divides flag. Patch submitted by Peter
Collingbourne: "This flag controls whether constant divides are optimized into add/shift/multiplies before passing to STP, and is set by default. In some circumstances the use of this optimisation can actually slow the solver down, so it is best to allow the user to disable it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102069 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Solver.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index dc787ad6..09cf4b47 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -157,7 +157,9 @@ namespace klee { /// /// \param useForkedSTP - Whether STP should be run in a separate process /// (required for using timeouts). - STPSolver(bool useForkedSTP); + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); |