MetaSMT builder, solver and command-line options.

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));
+
+
 }