stats: rename numQueries/Queries -> SolverQueries, add Queries

5 files changed, 8 insertions, 7 deletions

diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp
index 60a4fb51..a845f901 100644
--- a/lib/Solver/DummySolver.cpp
+++ b/lib/Solver/DummySolver.cpp
@@ -30,19 +30,19 @@ public:
 DummySolverImpl::DummySolverImpl() {}
 
 bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) {
-  ++stats::queries;
+  ++stats::solverQueries;
   // FIXME: We should have stats::queriesFail;
   return false;
 }
 
 bool DummySolverImpl::computeTruth(const Query &, bool &isValid) {
-  ++stats::queries;
+  ++stats::solverQueries;
   // FIXME: We should have stats::queriesFail;
   return false;
 }
 
 bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
-  ++stats::queries;
+  ++stats::solverQueries;
   ++stats::queryCounterexamples;
   return false;
 }
@@ -50,7 +50,7 @@ bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
 bool DummySolverImpl::computeInitialValues(
     const Query &, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
-  ++stats::queries;
+  ++stats::solverQueries;
   ++stats::queryCounterexamples;
   return false;
 }
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 0f78bb5b..37c22f0e 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -194,7 +194,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(
   TimerStatIncrementer t(stats::queryTime);
   assert(_builder);
 
-  ++stats::queries;
+  ++stats::solverQueries;
   ++stats::queryCounterexamples;
 
   bool success = true;
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index 13536910..6e62b82b 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -387,7 +387,7 @@ bool STPSolverImpl::computeInitialValues(
   for (const auto &constraint : query.constraints)
     vc_assertFormula(vc, builder->construct(constraint));
 
-  ++stats::queries;
+  ++stats::solverQueries;
   ++stats::queryCounterexamples;
 
   ExprHandle stp_e = builder->construct(query.expr);
diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp
index 40f0d53f..97b8902a 100644
--- a/lib/Solver/SolverStats.cpp
+++ b/lib/Solver/SolverStats.cpp
@@ -12,6 +12,7 @@
 using namespace klee;
 
 Statistic stats::cexCacheTime("CexCacheTime", "CCtime");
+Statistic stats::solverQueries("SolverQueries", "SQ");
 Statistic stats::queries("Queries", "Q");
 Statistic stats::queriesInvalid("QueriesInvalid", "Qiv");
 Statistic stats::queriesValid("QueriesValid", "Qv");
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index b628b86b..8319e5f3 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -268,7 +268,7 @@ bool Z3SolverImpl::internalRunSolver(
     Z3_solver_assert(builder->ctx, theSolver, builder->construct(constraint));
     constant_arrays_in_query.visit(constraint);
   }
-  ++stats::queries;
+  ++stats::solverQueries;
   if (objects)
     ++stats::queryCounterexamples;