2 files changed, 15 insertions, 13 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 399c27a2..e55c4550 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,9 +73,9 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     "use-query-log",
     llvm::cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."),
     llvm::cl::values(
-        clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
+        clEnumValN(ALL_KQUERY,"all:kquery","All queries in .kquery (KQuery) format"),
         clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
-        clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
+        clEnumValN(SOLVER_KQUERY,"solver:kquery","All queries reaching the solver in .kquery (KQuery) format"),
         clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"),
         clEnumValEnd
 	),
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index debb1e9e..68e1b08b 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -16,17 +16,18 @@
 #include "llvm/Support/raw_ostream.h"
 
 namespace klee {
-Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
+Solver *constructSolverChain(Solver *coreSolver,
+                             std::string querySMT2LogPath,
                              std::string baseSolverQuerySMT2LogPath,
-                             std::string queryPCLogPath,
-                             std::string baseSolverQueryPCLogPath) {
+                             std::string queryKQueryLogPath,
+                             std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_PC)) {
-    solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath,
+  if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
+    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
                                    MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .pc format to %s\n",
-                 baseSolverQueryPCLogPath.c_str());
+    klee_message("Logging queries that reach solver in .kquery format to %s\n",
+                 baseSolverQueryKQueryLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
@@ -51,10 +52,11 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, coreSolver);
 
-  if (optionIsSet(queryLoggingOptions, ALL_PC)) {
-    solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog);
-    klee_message("Logging all queries in .pc format to %s\n",
-                 queryPCLogPath.c_str());
+  if (optionIsSet(queryLoggingOptions, ALL_KQUERY)) {
+    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
+                                       MinQueryTimeToLog);
+    klee_message("Logging all queries in .kquery format to %s\n",
+                 queryKQueryLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {