path: root/test/regress/regress0/uflra/simple.04.cvc

% EXPECT: unsat
x1, x2: REAL;
y1, y2: REAL;
f: REAL -> REAL;
g: (REAL, REAL) -> REAL;

ASSERT (x1 <= x2) AND (x2 <= x1);

ASSERT NOT (g(x1, y1) = g(x2, y2));

ASSERT (y1 <= f(x1)) AND (f(x1) <= y1);
ASSERT (y2 <= f(x2)) AND (f(x2) <= y2);

CHECKSAT;