aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Basic/CmdLineOptions.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Basic/CmdLineOptions.cpp')
-rw-r--r--lib/Basic/CmdLineOptions.cpp12
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index ac0474fb..1201ac29 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,5 +73,17 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
llvm::cl::CommaSeparated
);
+
+llvm::cl::opt<klee::MetaSMTBackendType>
+UseMetaSMT("use-metasmt",
+ llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."),
+ llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"),
+ clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
+ clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
+ clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"),
+ clEnumValEnd),
+ llvm::cl::init(METASMT_BACKEND_NONE));
+
+
}