about summary refs log tree commit diff homepage
path: root/include/klee/CommandLine.h
diff options
context:
space:
mode:
Diffstat (limited to 'include/klee/CommandLine.h')
-rw-r--r--include/klee/CommandLine.h10
1 files changed, 9 insertions, 1 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 00cdeebb..dc69de6e 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -44,9 +44,17 @@ enum QueryLoggingSolverType
  */
 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
-enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER, Z3_SOLVER };
+enum CoreSolverType {
+  STP_SOLVER,
+  METASMT_SOLVER,
+  DUMMY_SOLVER,
+  Z3_SOLVER,
+  NO_SOLVER
+};
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
+extern llvm::cl::opt<CoreSolverType> DebugCrossCheckCoreSolverWith;
+
 #ifdef ENABLE_METASMT
 
 enum MetaSMTBackendType