From a0ce2ae13ff2b96befe633742ce5ce0c014666ed Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Wed, 8 Jun 2016 18:03:51 +0200
Subject: use default metaSMT solver as defined in configuration

---
 MetaSMT.mk                   |  1 +
 lib/Basic/CmdLineOptions.cpp | 18 ++++++++++++++++--
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/MetaSMT.mk b/MetaSMT.mk
index dd34e5fd..8733d9ec 100644
--- a/MetaSMT.mk
+++ b/MetaSMT.mk
@@ -4,6 +4,7 @@
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
   LD.Flags += $(metaSMT_LDFLAGS)
+  CXX.Flags += -DMETASMT_DEFAULT_SOLVER_$(METASMT_DEFAULT_SOLVER)
   CXX.Flags += $(metaSMT_CXXFLAGS)
   CXX.Flags += $(metaSMT_INCLUDES)
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index a0fbda03..7bff3437 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_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
+#else
+#define DEFAULT_METASMT_BACKEND_STR "(default = stp)."
+#define DEFAULT_METASMT_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 " DEFAULT_METASMT_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(DEFAULT_METASMT_BACKEND));
+
+#undef DEFAULT_METASMT_BACKEND
+#undef DEFAULT_METASMT_BACKEND_STR
 
 #endif /* ENABLE_METASMT */
 
-- 
cgit 1.4.1