3 files changed, 89 insertions, 2 deletions
diff --git a/Makefile.config.in b/Makefile.config.in
index 7d3c05f6..d6eada4e 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -35,6 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@
 
 ENABLE_METASMT := @ENABLE_METASMT@
 METASMT_ROOT := @METASMT_ROOT@
+METASMT_DEFAULT_SOLVER := @METASMT_DEFAULT_SOLVER@
 
 ENABLE_Z3 := @ENABLE_Z3@
 Z3_CFLAGS := @Z3_CFLAGS@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 63b1b6ca..00143171 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -742,7 +742,6 @@ dnl **************************************************************************
 AC_ARG_WITH(metasmt,
   AS_HELP_STRING([--with-metasmt],
     [Location of metaSMT installation directory]),,)
-
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
   AC_MSG_NOTICE([Not using MetaSMT solver backend])
@@ -775,6 +774,45 @@ fi
 
 AC_SUBST(ENABLE_METASMT)
 
+
+dnl **************************************************************************
+dnl User option to specify the default solver 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)]),,)
+
+if test "X$with_metasmt_default_solver" != X ; then
+  if test "X$ENABLE_METASMT" != X1 ; then
+    AC_MSG_ERROR([--with-metasmt-default-solver 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])
+  fi
+  if test "$with_metasmt_default_solver" == "z3" ; then
+    METASMT_DEFAULT_SOLVER=Z3
+    AC_MSG_NOTICE([metaSMT uses Z3 as default solver])
+  fi
+  if test "$with_metasmt_default_solver" == "stp" ; then
+    METASMT_DEFAULT_SOLVER=STP
+    AC_MSG_NOTICE([metaSMT uses STP as default solver])
+  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])
+  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])
+  fi  
+fi
+
+AC_SUBST(METASMT_DEFAULT_SOLVER)
+
+
 dnl **************************************************************************
 dnl Check at least one solver backend is enabled
 dnl **************************************************************************
diff --git a/configure b/configure
index c9cea90e..3c71aff4 100755
--- a/configure
+++ b/configure
@@ -624,6 +624,7 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
+METASMT_DEFAULT_SOLVER
 ENABLE_METASMT
 METASMT_ROOT
 Z3_LDFLAGS
@@ -739,6 +740,7 @@ with_tcmalloc
 with_stp
 with_z3
 with_metasmt
+with_metasmt_default_solver
 '
       ac_precious_vars='build_alias
 host_alias
@@ -1393,6 +1395,9 @@ 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
+                          unspecified)
 
 Some influential environment variables:
   CC          C compiler command
@@ -5324,7 +5329,6 @@ if test "${with_metasmt+set}" = set; then :
   withval=$with_metasmt;
 fi
 
-
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
   { $as_echo "$as_me:${as_lineno-$LINENO}: Not using MetaSMT solver backend" >&5
@@ -5392,6 +5396,50 @@ fi
 
 
 
+
+
+# Check whether --with-metasmt-default-solver was given.
+if test "${with_metasmt_default_solver+set}" = set; then :
+  withval=$with_metasmt_default_solver;
+fi
+
+
+if test "X$with_metasmt_default_solver" != X ; then
+  if test "X$ENABLE_METASMT" != X1 ; then
+    as_fn_error $? "--with-metasmt-default-solver 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;}
+  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;}
+  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;}
+  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;}
+  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;}
+  fi
+fi
+
+
+
+
+
 if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then
     as_fn_error $? "At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt" "$LINENO" 5
 fi