about summary refs log tree commit diff homepage
path: root/lib/Basic/CmdLineOptions.cpp
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2016-06-23 12:17:02 +0100
committerGitHub <noreply@github.com>2016-06-23 12:17:02 +0100
commit83e797ab33aef2749e0f6ffb9b63877085ca4e7c (patch)
tree406a8fc982967a7e7e2a883cde75a06671ad6971 /lib/Basic/CmdLineOptions.cpp
parent96ed13583a464538cab900c851bcc7338150772a (diff)
parent7bcd56cb0c102d4f662205958b2a5aa6698b86ea (diff)
downloadklee-83e797ab33aef2749e0f6ffb9b63877085ca4e7c.tar.gz
Merge pull request #409 from hoangmle/fix_metaSMT
Add metaSMT to Travis CI, fix metaSMTBuilder to pass all tests
Diffstat (limited to 'lib/Basic/CmdLineOptions.cpp')
-rw-r--r--lib/Basic/CmdLineOptions.cpp18
1 files changed, 16 insertions, 2 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index a0fbda03..20c190a5 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -84,16 +84,30 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 #ifdef ENABLE_METASMT
 
+#ifdef METASMT_DEFAULT_BACKEND_IS_BTOR
+#define METASMT_DEFAULT_BACKEND_STR "(default = btor)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR
+#elif METASMT_DEFAULT_BACKEND_IS_Z3
+#define METASMT_DEFAULT_BACKEND_STR "(default = z3)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3
+#else
+#define METASMT_DEFAULT_BACKEND_STR "(default = stp)."
+#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP
+#endif
+
 llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
     "metasmt-backend",
-    llvm::cl::desc("Specify the MetaSMT solver backend type (default=STP)."),
+    llvm::cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR),
     llvm::cl::values(
         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_STP));
+    llvm::cl::init(METASMT_DEFAULT_BACKEND));
+
+#undef METASMT_DEFAULT_BACKEND
+#undef METASMT_DEFAULT_BACKEND_STR
 
 #endif /* ENABLE_METASMT */