10 files changed, 35 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc
index c3cefd767..c3dbb2cd6 100644
--- a/test/regress/regress0/fmf/quant_real_univ.cvc
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "fmf-bound";
+OPTION "sets-ext";
 Atom : TYPE;
 REAL_UNIVERSE : SET OF [REAL];
 ATOM_UNIVERSE : SET OF [Atom];
diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc
index e36c6a647..297898a81 100644
--- a/test/regress/regress0/rels/joinImg_0.cvc
+++ b/test/regress/regress0/rels/joinImg_0.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc
index 602c4fe3f..4e69394bd 100644
--- a/test/regress/regress0/rels/joinImg_0_1.cvc
+++ b/test/regress/regress0/rels/joinImg_0_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc
index 47e57c1fb..81f208fc4 100644
--- a/test/regress/regress0/rels/joinImg_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc
index a7927f7e2..003770a1b 100644
--- a/test/regress/regress0/rels/joinImg_1_1.cvc
+++ b/test/regress/regress0/rels/joinImg_1_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc
index bbf57629b..a4acfe6c6 100644
--- a/test/regress/regress0/rels/joinImg_2.cvc
+++ b/test/regress/regress0/rels/joinImg_2.cvc
@@ -1,5 +1,6 @@
 % EXPECT: unsat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
index b38bfab06..03f88be37 100644
--- a/test/regress/regress0/rels/joinImg_2_1.cvc
+++ b/test/regress/regress0/rels/joinImg_2_1.cvc
@@ -1,5 +1,6 @@
 % EXPECT: sat
 OPTION "logic" "ALL_SUPPORTED";
+OPTION "sets-ext";
 Atom: TYPE;
 x : SET OF [Atom, Atom];
 y : SET OF [Atom, Atom];
@@ -21,4 +22,4 @@ ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
 ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
 ASSERT (NOT(a = b)) OR (NOT(a = f));
 
-CHECKSAT;
-\ No newline at end of file
+CHECKSAT;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index c8e416a42..de2170768 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -86,7 +86,9 @@ TESTS =	\
 	sets-poly-nonint.smt2 \
 	int-real-univ.smt2 \
 	int-real-univ-unsat.smt2 \
-	sets-tuple-poly.cvc
+	sets-tuple-poly.cvc \
+	arjun-set-univ.cvc \
+	univ-set-uf-elim.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc
new file mode 100644
index 000000000..3c35a62a5
--- /dev/null
+++ b/test/regress/regress0/sets/arjun-set-univ.cvc
@@ -0,0 +1,8 @@
+% EXPECT: Extended set operators are not supported in default mode, try --sets-ext.
+% EXIT: 1
+OPTION "produce-models" true;
+x,y,z : SET OF BOOLEAN;
+ASSERT x = {TRUE};
+ASSERT y = {FALSE};
+CHECKSAT z = ~ y;
+COUNTERMODEL;
diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2
new file mode 100644
index 000000000..a22f2a44f
--- /dev/null
+++ b/test/regress/regress0/sets/univ-set-uf-elim.smt2
@@ -0,0 +1,16 @@
+; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun f ((Set Bool)) Int)
+(declare-fun s () (Set Bool))
+
+(assert (member true s))
+(assert (member false s))
+(assert (= a (f (as univset (Set Bool)))))
+
+(assert (= (f (as emptyset (Set Bool))) 1))
+(assert (= (f (singleton true)) 2))
+(assert (= (f (singleton false)) 3))
+(assert (= (f (union (singleton true) (singleton false))) 4))
+(check-sat)