1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress1/sets/arjun-set-univ.cvc b/test/regress/regress1/sets/arjun-set-univ.cvc
new file mode 100644
index 000000000..3c35a62a5
--- /dev/null
+++ b/test/regress/regress1/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;