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/regress1/sets | |
| 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/regress1/sets')
| -rw-r--r-- | test/regress/regress1/sets/issue5342.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sets/issue5342_difference_version.smt2 | 7 |
2 files changed, 14 insertions, 0 deletions
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 |