diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-20 19:37:28 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-20 19:37:28 -0700 |
| commit | dd0bd217e222b2db5fac9aedee3aacee8a28d0b1 (patch) | |
| tree | 49705cb159dffa749e4363ee955d0a0ae44f7394 /configure.ac | |
| parent | 31043ac507a58d757f39eda3c74d0ae8884a071b (diff) | |
Check unsat cores in regressions also without LFSC (#1955)
When moving the LFSC checker out of the CVC4 repository in commit
dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0, we disabled checking unsat
cores when CVC4 was compiled without LFSC due to the complexity of the
regression script. This commit changes the new(-ish) Python regression
script to check unsat cores even when CVC4 was compiled without LFSC.
This is done by having two separate flags, --with-lfsc and
--enable-proof, for the regression script that mirror the configuration
flags. The regression script performs unsat cores and proofs checks
based on those flags.
Additionally, this commit changes the regression script to check proofs
and unsat cores in two independent runs. Testing them in a single run
masked issues #1953 and #1954.
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/configure.ac b/configure.ac index 222a6b4f6..81e3f1fdc 100644 --- a/configure.ac +++ b/configure.ac @@ -1053,9 +1053,11 @@ AC_ARG_WITH([cxxtest-dir], TESTS_ENVIRONMENT= RUN_REGRESSION_ARGS= -# FIXME currently, unsat core regressions are disabled without LFSC if test "$with_lfsc" = yes; then - RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof" + RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--with-lfsc" +fi +if test "$enable_proof" = yes; then + RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof" fi AC_SUBST([TESTS_ENVIRONMENT]) AC_SUBST([RUN_REGRESSION_ARGS]) |