path: root/test/regress/regress0/sets/rels/tobesolved/test.cvc

% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
r : SET OF IntPair;
ASSERT (y JOIN x) = x;

ASSERT (1,2) IS_IN x;

CHECKSAT;