about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2010-04-22 12:54:43 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2010-04-22 12:54:43 +0000
commit2624f435755c9de3632019fcd2ec68425a39c9e8 (patch)
treecd99cd4562befd28be648ce0a1a96555c8f29e3c /lib
parent3a96dd9b7d46247fea7754fdd54049ee723e11e4 (diff)
downloadklee-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
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp4
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,