% COMMAND-LINE: --no-check-models
% EXPECT: sat
A : SET OF INT;
a : INT;
ASSERT NOT (A = {} :: SET OF INT);
ASSERT CHOOSE (A) = 10;
ASSERT CHOOSE (A) = a;
CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback