diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 12:54:43 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2010-04-22 12:54:43 +0000 |
commit | 2624f435755c9de3632019fcd2ec68425a39c9e8 (patch) | |
tree | cd99cd4562befd28be648ce0a1a96555c8f29e3c | |
parent | 3a96dd9b7d46247fea7754fdd54049ee723e11e4 (diff) | |
download | klee-2624f435755c9de3632019fcd2ec68425a39c9e8.tar.gz |
Applied patch submitted by Peter Collingbourne: "If either of these
values is 0, the overall STP timeout should be whichever of the two values is set, i.e. the maximum of the 2 values, rather than 0." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102058 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | lib/Core/Executor.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d0fc43cf..fd6cf441 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -311,7 +311,9 @@ Executor::Executor(const InterpreterOptions &opts, inhibitForking(false), haltExecution(false), ivcEnabled(false), - stpTimeout(std::min(MaxSTPTime,MaxInstructionTime)) { + stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0 + ? std::min(MaxSTPTime,MaxInstructionTime) + : std::max(MaxSTPTime,MaxInstructionTime)) { STPSolver *stpSolver = new STPSolver(UseForkedSTP); Solver *solver = constructSolverChain(stpSolver, |