rename the configure option --with-metasmt-default-solver to --with-metasmt-default-backend and improve the associated CXX flag

6 files changed, 64 insertions, 64 deletions

diff --git a/.travis/klee.sh b/.travis/klee.sh
index bb57f281..98dbbc0d 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -66,7 +66,7 @@ for solver in ${SOLVER_LIST}; do
     ;;
   metaSMT)
     echo "metaSMT"
-    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-solver=${METASMT_DEFAULT}"
+    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}"
     ;;
   *)
     echo "Unknown solver ${solver}"
diff --git a/Makefile.config.in b/Makefile.config.in
index d6eada4e..1b0b7ba8 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -35,7 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@
 
 ENABLE_METASMT := @ENABLE_METASMT@
 METASMT_ROOT := @METASMT_ROOT@
-METASMT_DEFAULT_SOLVER := @METASMT_DEFAULT_SOLVER@
+METASMT_DEFAULT_BACKEND := @METASMT_DEFAULT_BACKEND@
 
 ENABLE_Z3 := @ENABLE_Z3@
 Z3_CFLAGS := @Z3_CFLAGS@
diff --git a/MetaSMT.mk b/MetaSMT.mk
index 8733d9ec..817fa663 100644
--- a/MetaSMT.mk
+++ b/MetaSMT.mk
@@ -4,7 +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 += -DMETASMT_DEFAULT_BACKEND_IS_$(METASMT_DEFAULT_BACKEND)
   CXX.Flags += $(metaSMT_CXXFLAGS)
   CXX.Flags += $(metaSMT_INCLUDES)
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 00143171..a08e190e 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -776,41 +776,41 @@ AC_SUBST(ENABLE_METASMT)
 
 
 dnl **************************************************************************
-dnl User option to specify the default solver of metaSMT
+dnl User option to specify the default backend of metaSMT
 dnl **************************************************************************
 
-AC_ARG_WITH(metasmt-default-solver,
-  AS_HELP_STRING([--with-metasmt-default-solver],
-    [Default solver of metaSMT (btor|stp|z3, stp if unspecified)]),,)
+AC_ARG_WITH(metasmt-default-backend,
+  AS_HELP_STRING([--with-metasmt-default-backend],
+    [Default backend of metaSMT (btor|stp|z3, stp if unspecified)]),,)
 
-if test "X$with_metasmt_default_solver" != X ; then
+if test "X$with_metasmt_default_backend" != X ; then
   if test "X$ENABLE_METASMT" != X1 ; then
-    AC_MSG_ERROR([--with-metasmt-default-solver requires metaSMT to be enabled])
+    AC_MSG_ERROR([--with-metasmt-default-backend requires metaSMT to be enabled])
   fi
-  if test "$with_metasmt_default_solver" == "btor" ; then
-    METASMT_DEFAULT_SOLVER=BTOR
-    AC_MSG_NOTICE([metaSMT uses Boolector as default solver])
+  if test "$with_metasmt_default_backend" == "btor" ; then
+    METASMT_DEFAULT_BACKEND=BTOR
+    AC_MSG_NOTICE([metaSMT uses Boolector as default backend])
   fi
-  if test "$with_metasmt_default_solver" == "z3" ; then
-    METASMT_DEFAULT_SOLVER=Z3
-    AC_MSG_NOTICE([metaSMT uses Z3 as default solver])
+  if test "$with_metasmt_default_backend" == "z3" ; then
+    METASMT_DEFAULT_BACKEND=Z3
+    AC_MSG_NOTICE([metaSMT uses Z3 as default backend])
   fi
-  if test "$with_metasmt_default_solver" == "stp" ; then
-    METASMT_DEFAULT_SOLVER=STP
-    AC_MSG_NOTICE([metaSMT uses STP as default solver])
+  if test "$with_metasmt_default_backend" == "stp" ; then
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([metaSMT uses STP as default backend])
   fi
-  if test "X$METASMT_DEFAULT_SOLVER" == X ; then
-    METASMT_DEFAULT_SOLVER=STP
-    AC_MSG_NOTICE([$with_metasmt_default_solver unsupported, metaSMT uses STP as default solver])
+  if test "X$METASMT_DEFAULT_BACKEND" == X ; then
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([$with_metasmt_default_backend unsupported, metaSMT uses STP as default backend])
   fi
 else
   if test "X$ENABLE_METASMT" == X1 ; then
-    METASMT_DEFAULT_SOLVER=STP
-    AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default solver])
+    METASMT_DEFAULT_BACKEND=STP
+    AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default backend])
   fi  
 fi
 
-AC_SUBST(METASMT_DEFAULT_SOLVER)
+AC_SUBST(METASMT_DEFAULT_BACKEND)
 
 
 dnl **************************************************************************
diff --git a/configure b/configure
index 3c71aff4..7f1839c0 100755
--- a/configure
+++ b/configure
@@ -624,7 +624,7 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
-METASMT_DEFAULT_SOLVER
+METASMT_DEFAULT_BACKEND
 ENABLE_METASMT
 METASMT_ROOT
 Z3_LDFLAGS
@@ -740,7 +740,7 @@ with_tcmalloc
 with_stp
 with_z3
 with_metasmt
-with_metasmt_default_solver
+with_metasmt_default_backend
 '
       ac_precious_vars='build_alias
 host_alias
@@ -1395,8 +1395,8 @@ Optional Packages:
   --with-stp              Location of STP installation directory
   --with-z3               Location of Z3 installation directory
   --with-metasmt          Location of metaSMT installation directory
-  --with-metasmt-default-solver
-                          Default solver of metaSMT (btor|stp|z3, stp if
+  --with-metasmt-default-backend
+                          Default backend of metaSMT (btor|stp|z3, stp if
                           unspecified)
 
 Some influential environment variables:
@@ -5398,41 +5398,41 @@ fi
 
 
 
-# Check whether --with-metasmt-default-solver was given.
-if test "${with_metasmt_default_solver+set}" = set; then :
-  withval=$with_metasmt_default_solver;
+# Check whether --with-metasmt-default-backend was given.
+if test "${with_metasmt_default_backend+set}" = set; then :
+  withval=$with_metasmt_default_backend;
 fi
 
 
-if test "X$with_metasmt_default_solver" != X ; then
+if test "X$with_metasmt_default_backend" != X ; then
   if test "X$ENABLE_METASMT" != X1 ; then
-    as_fn_error $? "--with-metasmt-default-solver requires metaSMT to be enabled" "$LINENO" 5
+    as_fn_error $? "--with-metasmt-default-backend requires metaSMT to be enabled" "$LINENO" 5
   fi
-  if test "$with_metasmt_default_solver" == "btor" ; then
-    METASMT_DEFAULT_SOLVER=BTOR
-    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default solver" >&5
-$as_echo "$as_me: metaSMT uses Boolector as default solver" >&6;}
+  if test "$with_metasmt_default_backend" == "btor" ; then
+    METASMT_DEFAULT_BACKEND=BTOR
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default backend" >&5
+$as_echo "$as_me: metaSMT uses Boolector as default backend" >&6;}
   fi
-  if test "$with_metasmt_default_solver" == "z3" ; then
-    METASMT_DEFAULT_SOLVER=Z3
-    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default solver" >&5
-$as_echo "$as_me: metaSMT uses Z3 as default solver" >&6;}
+  if test "$with_metasmt_default_backend" == "z3" ; then
+    METASMT_DEFAULT_BACKEND=Z3
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default backend" >&5
+$as_echo "$as_me: metaSMT uses Z3 as default backend" >&6;}
   fi
-  if test "$with_metasmt_default_solver" == "stp" ; then
-    METASMT_DEFAULT_SOLVER=STP
-    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default solver" >&5
-$as_echo "$as_me: metaSMT uses STP as default solver" >&6;}
+  if test "$with_metasmt_default_backend" == "stp" ; then
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: metaSMT uses STP as default backend" >&6;}
   fi
-  if test "X$METASMT_DEFAULT_SOLVER" == X ; then
-    METASMT_DEFAULT_SOLVER=STP
-    { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_solver unsupported, metaSMT uses STP as default solver" >&5
-$as_echo "$as_me: $with_metasmt_default_solver unsupported, metaSMT uses STP as default solver" >&6;}
+  if test "X$METASMT_DEFAULT_BACKEND" == X ; then
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&6;}
   fi
 else
   if test "X$ENABLE_METASMT" == X1 ; then
-    METASMT_DEFAULT_SOLVER=STP
-    { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default solver" >&5
-$as_echo "$as_me: No solver specified, metaSMT uses STP as default solver" >&6;}
+    METASMT_DEFAULT_BACKEND=STP
+    { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default backend" >&5
+$as_echo "$as_me: No solver specified, metaSMT uses STP as default backend" >&6;}
   fi
 fi
 
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 */