diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-09 12:24:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-09 17:24:50 +0000 |
| commit | e25d2ce5eff672bb5b58c245f0414a1ed9c51a6c (patch) | |
| tree | 4713df6d48a3a61a551a361a4d511dc229d083ea /test/regress/CMakeLists.txt | |
| parent | ff91290122d478dc637fb3e9ff4fe4c0ead5bd32 (diff) | |
Fix sets cardinality inference involving equivalent parents (#6855)
This fixes an unsoundness issue in the sets + cardinality solver.
One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:
if T = (union T S), then (intersect T S) = S.
The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.
This PR also does some minor cleanup.
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 ea78096dc..cdc77c980 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2068,6 +2068,7 @@ set(regress_1_tests regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 regress1/sets/sets-tuple-poly.cvc + regress1/sets/sets-uc-wrong.smt2 regress1/sets/set-comp-sat.smt2 regress1/sets/sharingbug.smt2 regress1/sets/univ-set-uf-elim.smt2 |