test/regress/regress0/rels/joinImg_2_1.cvc

   1 % EXPECT: sat
   2 OPTION "logic" "ALL_SUPPORTED";
   3 OPTION "sets-ext";
   4 Atom: TYPE;
   5 x : SET OF [Atom, Atom];
   6 y : SET OF [Atom, Atom];
   7 r : SET OF [Atom, Atom];
   8
   9 t : SET OF [Atom];
  10
  11 a : Atom;
  12 b : Atom;
  13 c : Atom;
  14 d : Atom;
  15 e : Atom;
  16 f : Atom;
  17 g : Atom;
  18
  19 ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
  20 ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1);
  21 ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
  22 ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
  23 ASSERT (NOT(a = b)) OR (NOT(a = f));
  24
  25 CHECKSAT;