summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/card-6.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/card-6.smt2')
-rw-r--r--test/regress/regress0/sets/card-6.smt216
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2
new file mode 100644
index 000000000..1611952b7
--- /dev/null
+++ b/test/regress/regress0/sets/card-6.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_UFLIAFS)
+(declare-sort E 0)
+(declare-fun A () (Set E))
+(declare-fun B () (Set E))
+(declare-fun C () (Set E))
+(assert
+ (and
+ (= (as emptyset (Set E))
+ (intersection A B))
+ (subset C (union A B))
+ (>= (card C) 5)
+ (<= (card A) 2)
+ (<= (card B) 2)
+ )
+)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback