summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/sets/Makefile.am3
-rw-r--r--test/regress/regress0/sets/compliment.cvc9
2 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index a92c534a1..629e8a8a0 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -75,7 +75,8 @@ TESTS = \
abt-min.smt2 \
abt-te-exh.smt2 \
abt-te-exh2.smt2 \
- univset-simp.smt2
+ univset-simp.smt2 \
+ compliment.cvc
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/compliment.cvc
new file mode 100644
index 000000000..6181cbee7
--- /dev/null
+++ b/test/regress/regress0/sets/compliment.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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback