test/regress/regress0/rels/joinImg_2.cvc

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