From: ajreynol Date: Thu, 8 Dec 2016 18:45:59 +0000 (-0600) Subject: Enable remaining cardinality benchmarks X-Git-Tag: cvc5-1.0.0~5944 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be7662bdcd3881d349bfba4c959a0c2be4159ce9;p=cvc5.git Enable remaining cardinality benchmarks --- 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))