about summary refs log tree commit diff homepage
path: root/lib/Basic
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:14:06 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 12:14:06 +0200
commit05a7b4c79603c5803cff1cc0e82d3e666ff486a2 (patch)
treea280013f3f184a78d4e90767f4b3d8e4d5b5f0ae /lib/Basic
parent9ef3c841b6d22e972ba8635a2eb2d3919bce9192 (diff)
downloadklee-05a7b4c79603c5803cff1cc0e82d3e666ff486a2.tar.gz
rename the configure option --with-metasmt-default-solver to --with-metasmt-default-backend and improve the associated CXX flag
Diffstat (limited to 'lib/Basic')
-rw-r--r--lib/Basic/CmdLineOptions.cpp24
1 files changed, 12 insertions, 12 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 7bff3437..20c190a5 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -84,30 +84,30 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 #ifdef ENABLE_METASMT
 
-#ifdef METASMT_DEFAULT_SOLVER_BTOR
-#define DEFAULT_METASMT_BACKEND_STR "(default = btor)."
-#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_BOOLECTOR
-#elif METASMT_DEFAULT_SOLVER_Z3
-#define DEFAULT_METASMT_BACKEND_STR "(default = z3)."
-#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_Z3
+#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 DEFAULT_METASMT_BACKEND_STR "(default = stp)."
-#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_STP
+#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_METASMT_BACKEND_STR),
+    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(DEFAULT_METASMT_BACKEND));
+    llvm::cl::init(METASMT_DEFAULT_BACKEND));
 
-#undef DEFAULT_METASMT_BACKEND
-#undef DEFAULT_METASMT_BACKEND_STR
+#undef METASMT_DEFAULT_BACKEND
+#undef METASMT_DEFAULT_BACKEND_STR
 
 #endif /* ENABLE_METASMT */