Renamed .pc to .kquery (kleaver query)

37 files changed, 92 insertions, 90 deletions

diff --git a/TODO.txt b/TODO.txt
index e547d1bc..794c3352 100644
--- a/TODO.txt
+++ b/TODO.txt
@@ -3,8 +3,6 @@ TODO
 
 Build System / Configure / Release Cleanups
 --
- o Rename .pc to .kquery (kleaver query)
-
  o Configure doesn't check for bison / flex, we don't really use these
    for anything important (just the command line STP tool), it would
    be nice if they weren't required.
diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h
index 6cce8031..9319b487 100644
--- a/include/expr/Lexer.h
+++ b/include/expr/Lexer.h
@@ -72,7 +72,7 @@ namespace expr {
     void dump();
   };
 
-  /// Lexer - Interface for lexing tokens from a .pc language file.
+  /// Lexer - Interface for lexing tokens from a .kquery language file.
   class Lexer {
     const char *BufferPos;      /// The current lexer position.
     const char *BufferEnd;      /// The buffer end position.
diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index a9133e9d..fa07bae2 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -202,7 +202,7 @@ namespace expr {
     static bool classof(const QueryCommand *) { return true; }
   };
   
-  /// Parser - Public interface for parsing a .pc language file.
+  /// Parser - Public interface for parsing a .kquery language file.
   class Parser {
   protected:
     Parser();
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index dc69de6e..95aa51e0 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -32,9 +32,9 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
 {
-    ALL_PC,       ///< Log all queries (un-optimised) in .pc (KQuery) format
+    ALL_KQUERY,   ///< Log all queries (un-optimised) in .kquery (KQuery) format
     ALL_SMTLIB,   ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
-    SOLVER_PC,    ///< Log queries passed to solver (optimised) in .pc (KQuery) format
+    SOLVER_KQUERY,///< Log queries passed to solver (optimised) in .kquery (KQuery) format
     SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
 };
 
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 7149708a..5f0f0e1d 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -19,14 +19,14 @@
 namespace klee {
     const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2";
     const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2";
-    const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
-    const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
+    const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery";
+    const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery";
 
     Solver *constructSolverChain(Solver *coreSolver,
                                  std::string querySMT2LogPath,
                                  std::string baseSolverQuerySMT2LogPath,
-                                 std::string queryPCLogPath,
-                                 std::string baseSolverQueryPCLogPath);
+                                 std::string queryKQueryLogPath,
+                                 std::string baseSolverQueryKQueryLogPath);
 }
 
 
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 3a4d40b4..ece84b2c 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -66,7 +66,7 @@ public:
   enum LogType
   {
 	  STP, //.CVC (STP's native language)
-	  KQUERY, //.PC files (kQuery native language)
+	  KQUERY, //.KQUERY files (kQuery native language)
 	  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
   };
 
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index c82ab135..2f613992 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -296,9 +296,9 @@ namespace klee {
   /// \param s - The underlying solver to use.
   Solver *createIndependentSolver(Solver *s);
   
-  /// createPCLoggingSolver - Create a solver which will forward all queries
-  /// after writing them to the given path in .pc format.
-  Solver *createPCLoggingSolver(Solver *s, std::string path,
+  /// createKQueryLoggingSolver - Create a solver which will forward all queries
+  /// after writing them to the given path in .kquery format.
+  Solver *createKQueryLoggingSolver(Solver *s, std::string path,
                                 int minQueryTimeToLog);
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
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)) {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 0981b8f4..1f3c1939 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -353,12 +353,13 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
   if (!coreSolver) {
     klee_error("Failed to create core solver\n");
   }
+
   Solver *solver = constructSolverChain(
       coreSolver,
       interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
-      interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
-      interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
+      interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
+      interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index eefe443a..19ce5af7 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -67,11 +67,11 @@ Decl* SMTParser::ParseTopLevelDecl() {
 
 bool SMTParser::Solve() {
   // FIXME: Support choice of solver.
-  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true;
+  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true;
   Solver *S, *STP = S = 
     UseDummySolver ? createDummySolver() : new STPSolver(true);
-  if (UseSTPQueryPCLog)
-    S = createPCLoggingSolver(S, "stp-queries.pc");
+  if (UseSTPQueryKQueryLog)
+    S = createKQueryLoggingSolver(S, "stp-queries.kquery");
   if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt
index 20da74da..1302db38 100644
--- a/lib/Solver/CMakeLists.txt
+++ b/lib/Solver/CMakeLists.txt
@@ -16,7 +16,7 @@ klee_add_component(kleaverSolver
   IncompleteSolver.cpp
   IndependentSolver.cpp
   MetaSMTSolver.cpp
-  PCLoggingSolver.cpp
+  KQueryLoggingSolver.cpp
   QueryLoggingSolver.cpp
   SMTLIBLoggingSolver.cpp
   Solver.cpp
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
index 67e9be45..a0ac950c 100644
--- a/lib/Solver/PCLoggingSolver.cpp
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -1,4 +1,4 @@
-//===-- PCLoggingSolver.cpp -----------------------------------------------===//
+//===-- KQueryLoggingSolver.cpp -----------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -17,52 +17,53 @@ using namespace klee;
 
 ///
 
-class PCLoggingSolver : public QueryLoggingSolver {
+class KQueryLoggingSolver : public QueryLoggingSolver {
 
 private :
     ExprPPrinter *printer;
-        
+
     virtual void printQuery(const Query& query,
                             const Query* falseQuery = 0,
                             const std::vector<const Array*>* objects = 0) {
-        
+
         const ref<Expr>* evalExprsBegin = 0;
         const ref<Expr>* evalExprsEnd = 0;
-        
+
         if (0 != falseQuery) {
             evalExprsBegin = &query.expr;
             evalExprsEnd = &query.expr + 1;
         }
-        
+
         const Array* const *evalArraysBegin = 0;
         const Array* const *evalArraysEnd = 0;
-        
+
         if ((0 != objects) && (false == objects->empty())) {
             evalArraysBegin = &((*objects)[0]);
-            evalArraysEnd = &((*objects)[0]) + objects->size();            
+            evalArraysEnd = &((*objects)[0]) + objects->size();
         }
-        
+
         const Query* q = (0 == falseQuery) ? &query : falseQuery;
-        
+
         printer->printQuery(logBuffer, q->constraints, q->expr,
                             evalExprsBegin, evalExprsEnd,
                             evalArraysBegin, evalArraysEnd);
     }
-  
+
 public:
-    PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) 
-    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),    
+    KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
+    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),
     printer(ExprPPrinter::create(logBuffer)) {
-    }                                                      
-    
-    virtual ~PCLoggingSolver() {    
+    }
+
+    virtual ~KQueryLoggingSolver() {
         delete printer;
-    }    
+    }
 };
 
 ///
 
-Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path,
+Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path,
                                     int minQueryTimeToLog) {
-  return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog));
+  return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog));
 }
+
diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.kquery
index 43134475..43134475 100644
--- a/test/Expr/Evaluate.pc
+++ b/test/Expr/Evaluate.kquery
diff --git a/test/Expr/Evaluate2.pc b/test/Expr/Evaluate2.kquery
index d62241f0..d62241f0 100644
--- a/test/Expr/Evaluate2.pc
+++ b/test/Expr/Evaluate2.kquery
diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.kquery
index 6b8e2e37..6b8e2e37 100644
--- a/test/Expr/Lexer/Numbers.pc
+++ b/test/Expr/Lexer/Numbers.kquery
diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.kquery
index 0b1479d4..0b1479d4 100644
--- a/test/Expr/Parser/Concat64.pc
+++ b/test/Expr/Parser/Concat64.kquery
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.kquery
index a02920db..a02920db 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.kquery
diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.kquery
index 4a6adf7e..4a6adf7e 100644
--- a/test/Expr/Parser/Exprs.pc
+++ b/test/Expr/Parser/Exprs.kquery
diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.kquery
index 71f0288f..71f0288f 100644
--- a/test/Expr/Parser/MultiByteReads.pc
+++ b/test/Expr/Parser/MultiByteReads.kquery
diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.kquery
index 6d817b6f..6d817b6f 100644
--- a/test/Expr/Parser/Simplify.pc
+++ b/test/Expr/Parser/Simplify.kquery
diff --git a/test/Expr/Parser/TypeChecking.kquery b/test/Expr/Parser/TypeChecking.kquery
new file mode 100644
index 00000000..d9685b70
--- /dev/null
+++ b/test/Expr/Parser/TypeChecking.kquery
@@ -0,0 +1,16 @@
+# RUN: not %kleaver %s 2> %t.log
+
+
+
+# RUN: grep "TypeChecking.kquery:7:9: error: type widths do not match in binary expression" %t.log
+array arr1[8] : w32 -> w8 = symbolic
+(query [(Eq (ReadLSB w32 0 arr1) true)]
+       false)
+
+# RUN: grep "TypeChecking.kquery:14:25: error: invalid write index (doesn't match array domain)" %t.log
+# RUN: grep "TypeChecking.kquery:14:35: error: invalid write value (doesn't match array range)" %t.log
+# FIXME: Add array declarations
+array arr2[8] : w32 -> w8 = symbolic
+(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)
+
+# RUN: grep "TypeChecking.kquery: parse failure: 3 errors." %t.log
diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc
deleted file mode 100644
index 66991c20..00000000
--- a/test/Expr/Parser/TypeChecking.pc
+++ /dev/null
@@ -1,16 +0,0 @@
-# RUN: not %kleaver %s 2> %t.log
-
-
-
-# RUN: grep "TypeChecking.pc:7:9: error: type widths do not match in binary expression" %t.log
-array arr1[8] : w32 -> w8 = symbolic
-(query [(Eq (ReadLSB w32 0 arr1) true)] 
-       false)
-
-# RUN: grep "TypeChecking.pc:14:25: error: invalid write index (doesn't match array domain)" %t.log
-# RUN: grep "TypeChecking.pc:14:35: error: invalid write value (doesn't match array range)" %t.log
-# FIXME: Add array declarations
-array arr2[8] : w32 -> w8 = symbolic
-(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)
-
-# RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log
diff --git a/test/Expr/print-smt-let.pc b/test/Expr/print-smt-let.kquery
index de097135..de097135 100644
--- a/test/Expr/print-smt-let.pc
+++ b/test/Expr/print-smt-let.kquery
diff --git a/test/Expr/print-smt-named.pc b/test/Expr/print-smt-named.kquery
index 0e0d87b7..0e0d87b7 100644
--- a/test/Expr/print-smt-named.pc
+++ b/test/Expr/print-smt-named.kquery
diff --git a/test/Expr/print-smt-none.pc b/test/Expr/print-smt-none.kquery
index c29392ab..c29392ab 100644
--- a/test/Expr/print-smt-none.pc
+++ b/test/Expr/print-smt-none.kquery
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c
index a2a07d8b..425c4551 100644
--- a/test/Feature/CompressedExprLogging.c
+++ b/test/Feature/CompressedExprLogging.c
@@ -3,10 +3,10 @@
 // solvers, in particular when counting the number of queries in the last two
 // commands
 // RUN: rm -rf %t.klee-out %t.klee-out2
-// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc
-// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc
-// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz
-// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery %t1.bc
+// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:kquery %t1.bc
+// RUN: gunzip -d %t.klee-out2/all-queries.kquery.gz
+// RUN: diff %t.klee-out/all-queries.kquery %t.klee-out/all-queries.kquery
 
 #include <assert.h>
 
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
index bba0570e..4479e850 100644
--- a/test/Feature/ExprLogging.c
+++ b/test/Feature/ExprLogging.c
@@ -1,11 +1,11 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
 // We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log
-// RUN: %kleaver -print-ast %t.klee-out/all-queries.pc > %t3.log
+// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery,all:smt2,solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
+// RUN: %kleaver -print-ast %t.klee-out/all-queries.kquery > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
-// RUN: %kleaver -print-ast %t.klee-out/solver-queries.pc > %t3.log
+// RUN: %kleaver -print-ast %t.klee-out/solver-queries.kquery > %t3.log
 // RUN: %kleaver -print-ast %t3.log > %t4.log
 // RUN: diff %t3.log %t4.log
 // RUN: grep "^; Query" %t.klee-out/all-queries.smt2 | wc -l | grep -q 17
diff --git a/test/Feature/MultiMkSym.c b/test/Feature/MultiMkSym.c
index 85b6ed70..fde864d7 100644
--- a/test/Feature/MultiMkSym.c
+++ b/test/Feature/MultiMkSym.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc -I../../../include -emit-llvm -g -c %s -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --write-pcs %t.bc > %t.log
-// RUN: cat %t.klee-out/test000001.pc %t.klee-out/test000002.pc %t.klee-out/test000003.pc %t.klee-out/test000004.pc > %t1
+// RUN: %klee --output-dir=%t.klee-out --write-kqueries %t.bc > %t.log
+// RUN: cat %t.klee-out/test000001.kquery %t.klee-out/test000002.kquery %t.klee-out/test000003.kquery %t.klee-out/test000004.kquery > %t1
 // RUN: grep "a\[1\]" %t1 | wc -l | grep 2
 // RUN: grep "a\[100\]" %t1 | wc -l | grep 2
 
diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c
index 3cb9c5fe..6bf199f7 100644
--- a/test/Feature/RewriteEqualities.c
+++ b/test/Feature/RewriteEqualities.c
@@ -1,11 +1,11 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities=false %t.bc
-// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.pc
-// RUN: grep "N0)" %t.klee-out/test000003.pc
+// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities=false %t.bc
+// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.kquery
+// RUN: grep "N0)" %t.klee-out/test000003.kquery
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-pcs --rewrite-equalities %t.bc
-// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.pc
+// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc
+// RUN: grep "(Read w8 8 const_arr1)" %t.klee-out/test000003.kquery
 
 #include <stdio.h>
 #include <klee/klee.h>
diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.kquery
index b3ec63e3..b3ec63e3 100644
--- a/test/Solver/FastCexSolver.pc
+++ b/test/Solver/FastCexSolver.kquery
diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.kquery
index e0921393..e0921393 100644
--- a/test/Solver/LargeIntegers.pc
+++ b/test/Solver/LargeIntegers.kquery
diff --git a/test/lit.cfg b/test/lit.cfg
index fdf9bf7b..4fe24ba2 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -21,7 +21,7 @@ config.test_format = lit.formats.ShTest(execute_external=False)
 
 # suffixes: A list of file extensions to treat as test files
 # Note this can be overridden by lit.local.cfg files
-config.suffixes = ['.ll', '.c', '.cpp', '.pc']
+config.suffixes = ['.ll', '.c', '.cpp', '.kquery']
 
 # test_source_root: The root path where tests are located.
 config.test_source_root = os.path.dirname(__file__)
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index a937d761..3fde0abf 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -224,8 +224,8 @@ static bool EvaluateInputAST(const char *Filename,
   Solver *S = constructSolverChain(coreSolver,
                                    getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
                                    getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
-                                   getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
-                                   getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
+                                   getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
+                                   getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index ee20f5ea..c4eaa30c 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -107,8 +107,8 @@ namespace {
             cl::desc("Write .cvc files for each test case"));
 
   cl::opt<bool>
-  WritePCs("write-pcs",
-            cl::desc("Write .pc files for each test case"));
+  WriteKQueries("write-kqueries",
+            cl::desc("Write .kquery files for each test case"));
 
   cl::opt<bool>
   WriteSMT2s("write-smt2s",
@@ -416,7 +416,7 @@ llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix,
 }
 
 
-/* Outputs all files (.ktest, .pc, .cov etc.) describing a test case */
+/* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */
 void KleeHandler::processTestCase(const ExecutionState &state,
                                   const char *errorMessage,
                                   const char *errorSuffix) {
@@ -482,10 +482,10 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       delete f;
     }
 
-    if (errorMessage || WritePCs) {
+    if (errorMessage || WriteKQueries) {
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
-      llvm::raw_ostream *f = openTestFile("pc", id);
+      llvm::raw_ostream *f = openTestFile("kquery", id);
       *f << constraints;
       delete f;
     }
diff --git a/utils/data/Queries/pcresymperf-3.pc b/utils/data/Queries/pcresymperf-3.kquery
index 209eaad9..209eaad9 100644
--- a/utils/data/Queries/pcresymperf-3.pc
+++ b/utils/data/Queries/pcresymperf-3.kquery
diff --git a/utils/data/Queries/pcresymperf-4.pc b/utils/data/Queries/pcresymperf-4.kquery
index 53da43ec..53da43ec 100644
--- a/utils/data/Queries/pcresymperf-4.pc
+++ b/utils/data/Queries/pcresymperf-4.kquery