diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-22 00:50:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-22 07:50:02 +0000 |
| commit | d3af203110d575a89a119c4f2c3956a4f6ce69f5 (patch) | |
| tree | 865ff8ba65e9ea03008680a493091d0ba4a441b6 /test/regress/CMakeLists.txt | |
| parent | b839049634d97025ac57ba9a342fd8ab70737a33 (diff) | |
Add support for minimal unsat cores (#4605)
This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index db6a7ae48..6ebb91f9e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1649,6 +1649,7 @@ set(regress_1_tests regress1/issue5739-rtf-processed.smt2 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2 regress1/lemmas/pursuit-safety-8.smtv1.smt2 + regress1/minimal_unsat_core.smt2 regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 |