diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-11-06 15:28:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-06 15:28:38 -0600 |
| commit | 63df35c477ee9e6c7bdeae677656dd374563de55 (patch) | |
| tree | 1ab725ce9c6f8dafdeda032d572963363f181f7b /test/regress | |
| parent | 6476c8c75ed7fd584b5afa658dd2c8ba277c59e2 (diff) | |
Fix issue #5342 (#5349)
This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sets/issue5342.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sets/issue5342_difference_version.smt2 | 7 |
3 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 334901c7a..c6c55d847 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1793,6 +1793,8 @@ set(regress_1_tests regress1/sets/issue4391-card-lasso.smt2 regress1/sets/issue5271.smt2 regress1/sets/issue5309.smt2 + regress1/sets/issue5342.smt2 + regress1/sets/issue5342_difference_version.smt2 regress1/sets/lemmabug-ListElts317minimized.smt2 regress1/sets/remove_check_free_31_6.smt2 regress1/sets/sets-disequal.smt2 diff --git a/test/regress/regress1/sets/issue5342.smt2 b/test/regress/regress1/sets/issue5342.smt2 new file mode 100644 index 000000000..e5e7ed65d --- /dev/null +++ b/test/regress/regress1/sets/issue5342.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --sets-ext +(set-logic ALL) +(set-info :status unsat) +(declare-fun S () (Set Int)) +(assert (is_singleton (complement (complement S)))) +(assert (= 2 (card S))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/issue5342_difference_version.smt2 b/test/regress/regress1/sets/issue5342_difference_version.smt2 new file mode 100644 index 000000000..143ac56c2 --- /dev/null +++ b/test/regress/regress1/sets/issue5342_difference_version.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --sets-ext +(set-logic ALL) +(set-info :status unsat) +(declare-fun S () (Set Int)) +(assert (is_singleton (setminus (as univset (Set Int)) (setminus (as univset (Set Int)) S)))) +(assert (= 2 (card S))) +(check-sat)
\ No newline at end of file |