diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-22 14:37:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-22 19:37:50 +0000 |
| commit | 78e84e867417642b04da5c136ef548dfde8ca7f0 (patch) | |
| tree | 835211a329d62764e8f1a724bc861d203a522429 /test/regress/CMakeLists.txt | |
| parent | d3df62e637057c77bab90ae644437fe250a64d37 (diff) | |
Prenex quantified formulas with user annotations by default (#7048)
Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.
This should avoid some more "unknown" responses on facebook benchmarks.
Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.
FYI @barrettcw .
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 1f2e17a7c..483e3a01e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1832,6 +1832,7 @@ set(regress_1_tests regress1/quantifiers/cdt-0208-to.smt2 regress1/quantifiers/const.cvc regress1/quantifiers/constfunc.cvc + regress1/quantifiers/ddatv-delta2.smt2 regress1/quantifiers/dt-tc-opt-small.smt2 regress1/quantifiers/dump-inst-i.smt2 regress1/quantifiers/dump-inst-proof.smt2 |