diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-08 18:01:39 +0200 |
|---|---|---|
| committer | Hoang M. Le <hle@informatik.uni-bremen.de> | 2016-06-10 11:32:20 +0200 |
| commit | 3e5288a6d9719735a505647ad9fcfc63b5bb2fc1 (patch) | |
| tree | 6f245eb7af61bfefbb1723bdbfb12c62867ebca4 /configure | |
| parent | 70bb7ef976a6a7b43d8aad6577773feaed7a2ebd (diff) | |
| download | klee-3e5288a6d9719735a505647ad9fcfc63b5bb2fc1.tar.gz | |
add --with-metasmt-default-solver option to configure
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 50 |
1 files changed, 49 insertions, 1 deletions
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 |