diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-22 12:04:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 17:04:00 +0000 |
| commit | 739f947fb53bc44fbae59952b3d9878b65ed0576 (patch) | |
| tree | cfdaaf4294a825633098f513ff07c719c5eb0489 /test/regress/CMakeLists.txt | |
| parent | 43106313622c0f147459bef44d25025335b6b4a5 (diff) | |
Always check legal eliminations in quantified logics (#6720)
Fixes #6699.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ca281af7b..6706ed4f6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1614,13 +1614,10 @@ set(regress_1_tests regress1/ho/issue4065-no-rep.smt2 regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 - regress1/ho/nested_lambdas-AGT034^2.smt2 - regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p regress1/ho/store-ax-min.p - regress1/ho/SYO056^1.p regress1/hole6.cvc regress1/ite5.smt2 regress1/issue3970-nl-ext-purify.smt2 @@ -1849,6 +1846,7 @@ set(regress_1_tests regress1/quantifiers/issue5658-qe.smt2 regress1/quantifiers/issue5766-wrong-sel-trigger.smt2 regress1/quantifiers/issue5899-qe.smt2 + regress1/quantifiers/issue6699-nc-shadow.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -2632,6 +2630,10 @@ set(regression_disabled_tests regress1/fmf/ko-bound-set.cvc # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 + # after disallowing solving for terms with quantifiers + regress1/ho/nested_lambdas-AGT034^2.smt2 + regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 + regress1/ho/SYO056^1.p # slow on some builds after changes to tangent planes regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator |