about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2018-10-08 23:28:10 +0100
committerMartinNowack <martin.nowack@gmail.com>2018-10-16 23:00:15 +0100
commit9d730c318aa77593d2cb6898c0b530dbec14f045 (patch)
tree2e0a2c85c52d01d4de6a93a6cd6ca11c4852b8ee
parent5b9f6d171f06c3619db20647abf2c185b4112346 (diff)
downloadklee-9d730c318aa77593d2cb6898c0b530dbec14f045.tar.gz
Small changes to comments
-rw-r--r--include/klee/Solver.h2
-rw-r--r--include/klee/SolverCmdLine.h12
2 files changed, 6 insertions, 8 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 2b80e9ec..c2a8ef1e 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -11,7 +11,7 @@
 #define KLEE_SOLVER_H
 
 #include "klee/Expr.h"
-#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType
+#include "klee/SolverCmdLine.h"
 
 #include <vector>
 
diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h
index 7a122e72..19e5fae6 100644
--- a/include/klee/SolverCmdLine.h
+++ b/include/klee/SolverCmdLine.h
@@ -42,14 +42,12 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
 extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
 
-/// The different query logging solvers that can switched on/off
+/// The different query logging solvers that can be switched on/off
 enum QueryLoggingSolverType {
-  ALL_KQUERY,    ///< Log all queries (un-optimised) in .kquery (KQuery) format
-  ALL_SMTLIB,    ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) 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
+  ALL_KQUERY,    ///< Log all queries in .kquery (KQuery) format
+  ALL_SMTLIB,    ///< Log all queries .smt2 (SMT-LIBv2) format
+  SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format
+  SOLVER_SMTLIB  ///< Log queries passed to solver in .smt2 (SMT-LIBv2) format
 };
 
 extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;