Added missing header to SolverCmdLine.h and clang-format it

2 files changed, 33 insertions, 23 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index e4762ae2..2b80e9ec 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,8 +10,8 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
-#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType
 #include "klee/Expr.h"
+#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType
 
 #include <vector>
 
diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h
index 9668d00b..7a122e72 100644
--- a/include/klee/SolverCmdLine.h
+++ b/include/klee/SolverCmdLine.h
@@ -1,10 +1,19 @@
+//===-- SolverCmdLine.h -----------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
 /*
- * This header groups command line options declarations and associated data
- * that is common for klee and kleaver.
+ * This header groups command-line options and associated declarations
+ * that are common to both KLEE and Kleaver.
  */
 
-#ifndef KLEE_COMMANDLINE_H
-#define KLEE_COMMANDLINE_H
+#ifndef KLEE_SOLVERCOMMANDLINE_H
+#define KLEE_SOLVERCOMMANDLINE_H
 
 #include "klee/Config/config.h"
 
@@ -19,10 +28,10 @@ extern llvm::cl::opt<bool> UseCexCache;
 
 extern llvm::cl::opt<bool> UseCache;
 
-extern llvm::cl::opt<bool> UseIndependentSolver; 
+extern llvm::cl::opt<bool> UseIndependentSolver;
 
 extern llvm::cl::opt<bool> DebugValidateSolver;
-  
+
 extern llvm::cl::opt<int> MinQueryTimeToLog;
 
 extern llvm::cl::opt<double> MaxCoreSolverTime;
@@ -33,13 +42,14 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
 extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
 
-///The different query logging solvers that can 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
+/// The different query logging solvers that can 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
 };
 
 extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions;
@@ -51,19 +61,19 @@ enum CoreSolverType {
   Z3_SOLVER,
   NO_SOLVER
 };
+
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
 extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
 
 #ifdef ENABLE_METASMT
 
-enum MetaSMTBackendType
-{
-    METASMT_BACKEND_STP,
-    METASMT_BACKEND_Z3,
-    METASMT_BACKEND_BOOLECTOR,
-    METASMT_BACKEND_CVC4,
-    METASMT_BACKEND_YICES2
+enum MetaSMTBackendType {
+  METASMT_BACKEND_STP,
+  METASMT_BACKEND_Z3,
+  METASMT_BACKEND_BOOLECTOR,
+  METASMT_BACKEND_CVC4,
+  METASMT_BACKEND_YICES2
 };
 
 extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
@@ -79,6 +89,6 @@ public:
   static void HideUnrelatedOptions(
       llvm::ArrayRef<const llvm::cl::OptionCategory *> Categories);
 };
-}
+} // namespace klee
 
-#endif	/* KLEE_COMMANDLINE_H */
+#endif /* KLEE_SOLVERCOMMANDLINE_H */