% EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; IntTup: TYPE = [INT, INT, INT]; x : SET OF IntTup; y : SET OF IntTup; z : IntTup; ASSERT z = (1,2,3); zt : IntTup; ASSERT zt = (3,2,1); ASSERT z IS_IN x; ASSERT NOT (zt IS_IN (TRANSPOSE x)); CHECKSAT;