More fixes for printing/parsing sets, fix kind name.

4 files changed, 14 insertions, 2 deletions

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/compliment.cvc b/test/regress/regress0/sets/complement.cvc
index 6181cbee7..6181cbee7 100644
--- a/test/regress/regress0/sets/compliment.cvc
+++ b/test/regress/regress0/sets/complement.cvc
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/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)