about summary refs log tree commit diff homepage
path: root/lib/Basic/ConstructSolverChain.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Basic/ConstructSolverChain.cpp')
-rw-r--r--lib/Basic/ConstructSolverChain.cpp15
1 files changed, 7 insertions, 8 deletions
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 5880ad59..8341f62d 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -13,8 +13,10 @@
 #include "klee/Common.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Internal/System/Time.h"
 #include "llvm/Support/raw_ostream.h"
 
+
 namespace klee {
 Solver *constructSolverChain(Solver *coreSolver,
                              std::string querySMT2LogPath,
@@ -22,17 +24,16 @@ Solver *constructSolverChain(Solver *coreSolver,
                              std::string queryKQueryLogPath,
                              std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
+  const time::Span minQueryTimeToLog(MinQueryTimeToLog);
 
   if (queryLoggingOptions.isSet(SOLVER_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
-                                   MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .kquery format to %s\n",
                  baseSolverQueryKQueryLogPath.c_str());
   }
 
   if (queryLoggingOptions.isSet(SOLVER_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
-                                       MinQueryTimeToLog);
+    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
                  baseSolverQuerySMT2LogPath.c_str());
   }
@@ -56,15 +57,13 @@ Solver *constructSolverChain(Solver *coreSolver,
     solver = createValidatingSolver(solver, coreSolver);
 
   if (queryLoggingOptions.isSet(ALL_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
-                                       MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .kquery format to %s\n",
                  queryKQueryLogPath.c_str());
   }
 
   if (queryLoggingOptions.isSet(ALL_SMTLIB)) {
-    solver =
-        createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
+    solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .smt2 format to %s\n",
                  querySMT2LogPath.c_str());
   }