From 55037e0bcef45c795f28ff3fcf6c1055af465c70 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 15 Feb 2018 15:31:48 -0600 Subject: Refactor regressions (#1581) --- test/regress/regress1/sets/card-7.smt2 | 47 ++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 test/regress/regress1/sets/card-7.smt2 (limited to 'test/regress/regress1/sets/card-7.smt2') diff --git a/test/regress/regress1/sets/card-7.smt2 b/test/regress/regress1/sets/card-7.smt2 new file mode 100644 index 000000000..df1867c63 --- /dev/null +++ b/test/regress/regress1/sets/card-7.smt2 @@ -0,0 +1,47 @@ +(set-logic QF_UFLIAFS) +(set-info :status sat) +(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