% EXPECT: sat

x: REAL;
y: REAL;
b: BOOLEAN;

ASSERT ((0 = IF b THEN x - y ELSE 2*x ENDIF));

CHECKSAT;

% EXIT: 10