From d34a946acb7f5155ee62f1bdc95ae7ef7b848e49 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 11 Apr 2016 08:19:02 -0500
Subject: Add ``-debug-cross-check-core-solver`` option to allow cross-checking
 with another solver. For example the core solver can be STP and the cross
 checking solver can be Z3.

Unfortunately a few fragile tests don't pass when actually using this
option.
---
 include/klee/CommandLine.h | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'include')

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
-- 
cgit 1.4.1