Frontend support for the choice operator (#4175)

[cvc5.git] / test / regress / regress0 / bug596b.cvc

% EXPECT: sat

f : INT -> [ INT, BOOLEAN ];
a : INT;
ASSERT f(a) /= ( 0, FALSE );

CHECKSAT;