From 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c Mon Sep 17 00:00:00 2001
From: Paul Meng <baolmeng@gmail.com>
Date: Thu, 20 Apr 2017 14:04:24 -0500
Subject: Support for relational operators identity and join image

---
 test/regress/regress0/rels/joinImg_2_1.cvc | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test/regress/regress0/rels/joinImg_2_1.cvc

(limited to 'test/regress/regress0/rels/joinImg_2_1.cvc')

diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
new file mode 100644
index 000000000..b38bfab06
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_2_1.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+f : Atom;
+g : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1);
+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
-- 
cgit v1.2.3