% EXPECT: unsat
x, y: REAL;
f: REAL -> REAL;

ASSERT (x <= y);
ASSERT (y <= x);
ASSERT NOT (f(x) = f(y));

CHECKSAT;