% EXPECT: sat
x: REAL;
b: BOOLEAN;

ASSERT (x = IF b THEN 10 ELSE -10 ENDIF);
ASSERT b;

CHECKSAT;

% EXIT: 10