diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-02 10:28:36 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 15:28:36 +0000 |
| commit | ec6fe33ab778a7bb5d2d016b799b1918b90fc338 (patch) | |
| tree | a870fea033a8cbf0761d7574c773b18e05f32a2e /test/regress/CMakeLists.txt | |
| parent | c54fe84863ce4257bd466a95ec42d7a6100d3c19 (diff) | |
Fix unsat core proofs (#6655)
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index daa28580a..860d1854a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1687,9 +1687,11 @@ set(regress_1_tests regress1/non-fatal-errors.smt2 regress1/parsing_ringer.cvc regress1/proof00.smt2 + regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 regress1/proofs/sat-trivial-cycle.smt2 + regress1/proofs/unsat-cores-proofs.smt2 regress1/push-pop/arith_lra_01.smt2 regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 |