Check unsat cores in regressions also without LFSC (#1955)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 21 Jun 2018 02:37:28 +0000 (19:37 -0700)
committerGitHub <noreply@github.com>
Thu, 21 Jun 2018 02:37:28 +0000 (19:37 -0700)
commitdd0bd217e222b2db5fac9aedee3aacee8a28d0b1
tree49705cb159dffa749e4363ee955d0a0ae44f7394
parent31043ac507a58d757f39eda3c74d0ae8884a071b
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.
configure.ac
test/regress/run_regression.py