From bf4e6c393f78ef8bd1b00e1e67b200a6ec51fd7c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 22 Apr 2010 16:14:41 +0000 Subject: 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 --- include/klee/Solver.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'include') 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); -- cgit 1.4.1