diff options
| author | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
|---|---|---|
| committer | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
| commit | dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch) | |
| tree | 7516d3d5d43f0dadb943bb186615e0903cbd9f7f /test/regress/regress0/sets | |
| parent | 74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff) | |
| parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) | |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'test/regress/regress0/sets')
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card3-ground.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress0/sets/dt-simp-mem.smt2 | 9 |
3 files changed, 18 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 5069d061e..4e1806aba 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -62,7 +62,9 @@ TESTS = \ union-1a.smt2 \ union-1b-flip.smt2 \ union-1b.smt2 \ - union-2.smt2 + union-2.smt2 \ + dt-simp-mem.smt2 \ + card3-ground.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2 new file mode 100644 index 000000000..54a9a5cfc --- /dev/null +++ b/test/regress/regress0/sets/card3-ground.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun S () (Set Int)) +(assert (>= (card S) 3)) +(assert (not (member 1 S))) +(check-sat) diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 new file mode 100644 index 000000000..a38544aa2 --- /dev/null +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-datatypes () ((D (A (a Int))))) +(declare-fun x1 () D) +(declare-fun S () (Set D)) +(declare-fun P (D) Bool) +(assert (member x1 S)) +(assert (=> (member (A 0) S) (P x1))) +(check-sat) |