From 4f1ad0a8426e0bba970bfaef1367e4e7a70ad0c1 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 22 Jan 2013 18:37:12 +0000 Subject: 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 --- include/klee/CommandLine.h | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'include') diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index 4b537174..c8397cf1 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -20,6 +20,21 @@ llvm::cl::opt UseFastCexSolver("use-fast-cex-solver", llvm::cl::init(false), llvm::cl::desc("(default=off)")); + +llvm::cl::opt +UseCexCache("use-cex-cache", + llvm::cl::init(true), + llvm::cl::desc("Use counterexample caching (default=on)")); + +llvm::cl::opt +UseCache("use-cache", + llvm::cl::init(true), + llvm::cl::desc("Use validity caching (default=on)")); + +llvm::cl::opt +UseIndependentSolver("use-independent-solver", + llvm::cl::init(true), + llvm::cl::desc("Use constraint independence (default=on)")); llvm::cl::opt MinQueryTimeToLog("min-query-time-to-log", -- cgit 1.4.1