From: ajreynol <andrew.j.reynolds@gmail.com>
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))