path: root/test/regress/regress0/sets/sets-tuple-poly.cvc

% EXPECT: sat
OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";

a : SET OF [REAL, INT];
b : SET OF [INT, REAL];

x : [ REAL, REAL ];


ASSERT NOT x = (0,0);

ASSERT x IS_IN a;
ASSERT x IS_IN b;

ASSERT NOT x.0 = x.1;

CHECKSAT;