Enable remaining cardinality benchmarks

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index d509a9fd5e763c96e8f457d8d8b7fda004a85a82..fb5084b9dc703cf381f109b024900c7b8fb9d169 100644 (file)
--- 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 cb414dbef6e85683e2b191ad8aae020bc903c23e..bc460fb4af38bd8e9ce59c6f7d39fa913bcc8b9a 100644 (file)
--- 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 949ed34575f904d3d9a6c25316974ef26f6c2e6e..0e96b0231db5277fae26b4a127c74501f1f11764 100644 (file)
--- 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 ea7fe42f3b34963e8f43eaf55df04fe90fc31848..456e24ca7c47b3332034614d308979bf437e6804 100644 (file)
--- 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 65135e7b48cfd07edb18b2d76d12aff6c48a6500..4135a0c16b768edd46cf35384e3ea5cec857bb2e 100644 (file)
--- 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 1611952b7338142631c44db63134fa9f596933f7..87d87c03b42a1faa5023b4dfe0d67a4b3cbe0b54 100644 (file)
--- 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 94468dc576df8e82636b6763c5dfe41119922fcc..df1867c634d597cffe9ae70434d4b9a8050b6424 100644 (file)
--- 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))