diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-25 11:11:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-25 11:11:02 -0600 |
| commit | 7f851ea2e2b40f7e5d6e0c0fbe4e9c6ea0450209 (patch) | |
| tree | 2f0f280eebd98631aa839710dbf5713ccac10a89 /test/regress/CMakeLists.txt | |
| parent | 1dc23a88520ac3053f15bc16df2e302bbed49765 (diff) | |
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.
Positive impact (+222-69) on SMT-LIB, 30 second timeout
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 da4c6633b..cf4b0386d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1762,6 +1762,8 @@ set(regress_1_tests regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 regress1/quantifiers/lra-vts-inf.smt2 + regress1/quantifiers/min-ppgt-em-incomplete.smt2 + regress1/quantifiers/min-ppgt-em-incomplete2.smt2 regress1/quantifiers/mix-coeff.smt2 regress1/quantifiers/mutualrec2.cvc regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 |