diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-24 09:16:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-24 09:16:52 -0500 |
| commit | 0a4ee1ac60e6b914ca8173c773eb9db54cdf0f61 (patch) | |
| tree | 04171a29b35069bac913785daf30a188720b004c /test/regress/regress1/sets | |
| parent | 6937d6afe65ae3e51f514ca463f95faa3feda7aa (diff) | |
Fix issue 5271 (#5335)
This PR fixes #5271 by splitting on the equality of set members which ensures members are distinct when collectModelInfo is called.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Diffstat (limited to 'test/regress/regress1/sets')
| -rw-r--r-- | test/regress/regress1/sets/issue5271.smt2 | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2 new file mode 100644 index 000000000..ba8180b5e --- /dev/null +++ b/test/regress/regress1/sets/issue5271.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun s () (Set Int)) +(assert (> (card s) 1)) +(assert (and (member 0 s) (exists ((x Int)) (member (mod x 1) s)))) +(check-sat) |