From 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Wed, 20 Apr 2016 14:43:18 -0500 Subject: update from the master --- test/regress/regress0/sets/card-7.smt2 | 46 ++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test/regress/regress0/sets/card-7.smt2 (limited to 'test/regress/regress0/sets/card-7.smt2') diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2 new file mode 100644 index 000000000..94468dc57 --- /dev/null +++ b/test/regress/regress0/sets/card-7.smt2 @@ -0,0 +1,46 @@ +(set-logic QF_UFLIAFS) +(declare-sort E 0) +(declare-fun A1 () (Set E)) +(declare-fun A2 () (Set E)) +(declare-fun A3 () (Set E)) +(declare-fun A4 () (Set E)) +(declare-fun A5 () (Set E)) +(declare-fun A6 () (Set E)) +(declare-fun A7 () (Set E)) +(declare-fun A8 () (Set E)) +(declare-fun A9 () (Set E)) +(declare-fun A10 () (Set E)) +(declare-fun A11 () (Set E)) +(declare-fun A12 () (Set E)) +(declare-fun A13 () (Set E)) +(declare-fun A14 () (Set E)) +(declare-fun A15 () (Set E)) +(declare-fun A16 () (Set E)) +(declare-fun A17 () (Set E)) +(declare-fun A18 () (Set E)) +(declare-fun A19 () (Set E)) +(declare-fun A20 () (Set E)) +(assert (and + (= (card A1) 1) + (= (card A2) 1) + (= (card A3) 1) + (= (card A4) 1) + (= (card A5) 1) + (= (card A6) 1) + (= (card A7) 1) + (= (card A8) 1) + (= (card A9) 1) + (= (card A10) 1) + (= (card A11) 1) + (= (card A12) 1) + (= (card A13) 1) + (= (card A14) 1) + (= (card A15) 1) + (= (card A16) 1) + (= (card A17) 1) + (= (card A18) 1) + (= (card A19) 1) + (= (card A20) 1) +)) +(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20)))) +(check-sat) -- cgit v1.2.3