diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
| commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
| tree | 0989e95f24c2eeedd177d2281069d266b31d971d /test/regress/CMakeLists.txt | |
| parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) | |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 52bdd6854..a3eaeee57 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1711,7 +1711,6 @@ set(regress_1_tests regress1/quantifiers/constfunc.cvc regress1/quantifiers/dt-tc-opt-small.smt2 regress1/quantifiers/dump-inst-i.smt2 - regress1/quantifiers/dump-inst-proof.smt2 regress1/quantifiers/dump-inst.smt2 regress1/quantifiers/eqrange_ex_1.smt2 regress1/quantifiers/ext-ex-deq-trigger.smt2 @@ -2491,6 +2490,8 @@ set(regression_disabled_tests regress1/quantifiers/anti-sk-simp.smt2 # no longer support snorm option regress1/quantifiers/arith-snorm.smt2 + # until we have support for minimizing instantiations based on unsat core + regress1/quantifiers/dump-inst-proof.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build, ok with other builds: |