diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-28 22:08:55 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-28 22:08:55 +0000 |
| commit | b695ce10f294b2469434656fb2c5dc8e6d701c5d (patch) | |
| tree | 7e803cfebd987b2255d9a3ce70740ad4356e0c9e /configure.ac | |
| parent | 890bacd7cb11c6e991722e8a7b7cd0ef9147ea3b (diff) | |
proof regressions
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/configure.ac b/configure.ac index 922f65416..729544391 100644 --- a/configure.ac +++ b/configure.ac @@ -478,7 +478,6 @@ if test "$enable_proof" = yes; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF" fi - AC_MSG_CHECKING([whether to optimize libcvc4]) AC_ARG_ENABLE([optimized], @@ -722,6 +721,24 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then esac fi +AC_ARG_VAR(LFSC, [path to LFSC proof checker]) +AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker]) +if test -z "$LFSC"; then + AC_CHECK_PROGS(LFSC, lfsc, [], []) +else + AC_CHECK_PROG(LFSC, "$LFSC", [], []) +fi +AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes]) +if test -z "$LFSC"; then + support_proof_tests='no, lfsc proof checker unavailable' +elif test "$enable_proof" = yes; then + support_proof_tests='yes, proof regression tests enabled' +else + support_proof_tests='no, proof generation disabled for this build' +fi +AC_SUBST([LFSC]) +AC_SUBST([LFSCARGS]) + CXXTESTGEN= AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH]) if test -z "$CXXTESTGEN"; then @@ -1061,6 +1078,7 @@ Dumping : $enable_dumping Muzzle : $enable_muzzle Unit tests : $support_unit_tests +Proof tests : $support_proof_tests gcov support : $enable_coverage gprof support: $enable_profiling CUDD : $cvc4cudd |