1 2 3 4 5 6 7 8 9 10 11
% EXPECT: sat x1, y1, z1: REAL; x2, y2, z2: REAL; f: REAL -> REAL; g: (REAL, REAL) -> REAL; ASSERT (z1 = f(x1)); ASSERT (z2 = f(y1)); ASSERT NOT (g(z1, z2) = g(z2, y2)); CHECKSAT;