1 files changed, 49 insertions, 3 deletions
diff --git a/configure b/configure
index 33893680..7f1839c0 100755
--- a/configure
+++ b/configure
@@ -624,6 +624,7 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
+METASMT_DEFAULT_BACKEND
 ENABLE_METASMT
 METASMT_ROOT
 Z3_LDFLAGS
@@ -739,6 +740,7 @@ with_tcmalloc
 with_stp
 with_z3
 with_metasmt
+with_metasmt_default_backend
 '
       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-backend
+                          Default backend 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
@@ -5384,8 +5388,6 @@ $as_echo "#define ENABLE_METASMT 1" >>confdefs.h
 
   METASMT_ROOT=$metasmt_root
 
-  REQUIRES_RTTI=1
-
   ENABLE_METASMT=1
   { $as_echo "$as_me:${as_lineno-$LINENO}: Using MetaSMT solver backend" >&5
 $as_echo "$as_me: Using MetaSMT solver backend" >&6;}
@@ -5394,6 +5396,50 @@ fi
 
 
 
+
+
+# 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_backend" != X ; then
+  if test "X$ENABLE_METASMT" != X1 ; then
+    as_fn_error $? "--with-metasmt-default-backend requires metaSMT to be enabled" "$LINENO" 5
+  fi
+  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_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_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_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_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
+
+
+
+
+
 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