diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-08 12:45:59 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-08 12:45:59 -0600 |
| commit | be7662bdcd3881d349bfba4c959a0c2be4159ce9 (patch) | |
| tree | 00ab473b1ab6197fea0668403b3fb7cc44ef8c43 /test | |
| parent | 87c471be5794ddfaf285ac3cb27eaeae6c8a267c (diff) | |
Enable remaining cardinality benchmarks
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 9 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-2.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-3.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-4.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-5.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-6.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/card-7.smt2 | 1 |
7 files changed, 14 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index d509a9fd5..fb5084b9d 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -65,7 +65,14 @@ TESTS = \ dt-simp-mem.smt2 \ card3-ground.smt2 \ card-3sets.cvc \ - card.smt2 + card.smt2 \ + card-2.smt2 \ + card-3.smt2 \ + card-4.smt2 \ + card-5.smt2 \ + card-6.smt2 \ + card-7.smt2 + EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/card-2.smt2 b/test/regress/regress0/sets/card-2.smt2 index cb414dbef..bc460fb4a 100644 --- a/test/regress/regress0/sets/card-2.smt2 +++ b/test/regress/regress0/sets/card-2.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status sat) (declare-sort E 0) (declare-fun s () (Set E)) (declare-fun t () (Set E)) diff --git a/test/regress/regress0/sets/card-3.smt2 b/test/regress/regress0/sets/card-3.smt2 index 949ed3457..0e96b0231 100644 --- a/test/regress/regress0/sets/card-3.smt2 +++ b/test/regress/regress0/sets/card-3.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status unsat) (declare-sort E 0) (declare-fun s () (Set E)) (declare-fun t () (Set E)) diff --git a/test/regress/regress0/sets/card-4.smt2 b/test/regress/regress0/sets/card-4.smt2 index ea7fe42f3..456e24ca7 100644 --- a/test/regress/regress0/sets/card-4.smt2 +++ b/test/regress/regress0/sets/card-4.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status sat) (declare-sort E 0) (declare-fun s () (Set E)) (declare-fun t () (Set E)) diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2 index 65135e7b4..4135a0c16 100644 --- a/test/regress/regress0/sets/card-5.smt2 +++ b/test/regress/regress0/sets/card-5.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status unsat) (declare-sort E 0) (declare-fun s () (Set E)) (declare-fun t () (Set E)) diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2 index 1611952b7..87d87c03b 100644 --- a/test/regress/regress0/sets/card-6.smt2 +++ b/test/regress/regress0/sets/card-6.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status unsat) (declare-sort E 0) (declare-fun A () (Set E)) (declare-fun B () (Set E)) diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2 index 94468dc57..df1867c63 100644 --- a/test/regress/regress0/sets/card-7.smt2 +++ b/test/regress/regress0/sets/card-7.smt2 @@ -1,4 +1,5 @@ (set-logic QF_UFLIAFS) +(set-info :status sat) (declare-sort E 0) (declare-fun A1 () (Set E)) (declare-fun A2 () (Set E)) |