summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/complement2.cvc
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-03-07 11:17:34 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2017-03-07 11:17:34 -0600
commitab68adfc44049598ee79a3c8b4379694d786d9aa (patch)
tree1609ecda726c535466b4f7501d4dba5b72409ba9 /test/regress/regress0/sets/complement2.cvc
parent105cae4ed94f0ce13b0525a348b29d2fc7d5af72 (diff)
More fixes for printing/parsing sets, fix kind name.
Diffstat (limited to 'test/regress/regress0/sets/complement2.cvc')
-rw-r--r--test/regress/regress0/sets/complement2.cvc11
1 files changed, 11 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback