diff options
Diffstat (limited to 'test/regress/regress0/rels/joinImg_2_1.cvc')
-rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 24 |
1 files changed, 24 insertions, 0 deletions
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 |