Patch by Hristina Palikareva which enables Kleaver to configure the

solver chain.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 1 insertions, 16 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f3278c89..a0c4de1c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -145,31 +145,16 @@ namespace {
 			      cl::desc("Only output test cases covering new code."));
 
   cl::opt<bool>
-  UseIndependentSolver("use-independent-solver",
-                       cl::init(true),
-		       cl::desc("Use constraint independence (default=on)"));
-
-  cl::opt<bool>
   EmitAllErrors("emit-all-errors",
                 cl::init(false),
                 cl::desc("Generate tests cases for all errors "
                          "(default=off, i.e. one per (error,instruction) pair)"));
-
-  cl::opt<bool>
-  UseCexCache("use-cex-cache",
-              cl::init(true),
-	      cl::desc("Use counterexample caching (default=on)"));
-   
+  
   cl::opt<bool>
   NoExternals("no-externals", 
            cl::desc("Do not allow external function calls (default=off)"));
 
   cl::opt<bool>
-  UseCache("use-cache",
-	   cl::init(true),
-	   cl::desc("Use validity caching (default=on)"));
-
-  cl::opt<bool>
   AlwaysOutputSeeds("always-output-seeds",
 		    cl::init(true));