From ab68adfc44049598ee79a3c8b4379694d786d9aa Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Mar 2017 11:17:34 -0600
Subject: More fixes for printing/parsing sets, fix kind name.

---
 test/regress/regress0/sets/Makefile.am       |  3 ++-
 test/regress/regress0/sets/complement.cvc    |  9 +++++++++
 test/regress/regress0/sets/complement2.cvc   | 11 +++++++++++
 test/regress/regress0/sets/compliment.cvc    |  9 ---------
 test/regress/regress0/sets/univset-simp.smt2 |  2 +-
 5 files changed, 23 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress0/sets/complement.cvc
 create mode 100644 test/regress/regress0/sets/complement2.cvc
 delete mode 100644 test/regress/regress0/sets/compliment.cvc

(limited to 'test')

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 629e8a8a0..06bd6cbf1 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -76,7 +76,8 @@ TESTS =	\
 	abt-te-exh.smt2 \
 	abt-te-exh2.smt2 \
 	univset-simp.smt2 \
-	compliment.cvc
+	complement.cvc \
+	complement2.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc
new file mode 100644
index 000000000..6181cbee7
--- /dev/null
+++ b/test/regress/regress0/sets/complement.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+a : SET OF [Atom];
+b : SET OF [Atom];
+
+ASSERT a = (NOT b);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
new file mode 100644
index 000000000..6802065f1
--- /dev/null
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -0,0 +1,11 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+a : SET OF Atom;
+b : SET OF Atom;
+c : Atom;
+
+ASSERT a = NOT(a);
+ASSERT c IS_IN a;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/compliment.cvc
deleted file mode 100644
index 6181cbee7..000000000
--- a/test/regress/regress0/sets/compliment.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-Atom: TYPE;
-a : SET OF [Atom];
-b : SET OF [Atom];
-
-ASSERT a = (NOT b);
-
-CHECKSAT;
diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index 5d10e27cb..ec9750776 100644
--- a/test/regress/regress0/sets/univset-simp.smt2
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -15,7 +15,7 @@
 (assert (not (member 1 c)))
 (assert (member 2 d))
 (assert (= e (as univset (Set Int))))
-(assert (= f (compliment d)))
+(assert (= f (complement d)))
 (assert (not (member x (as univset (Set Int)))))
 
 (check-sat)
-- 
cgit v1.2.3