summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sets/choose.cvc
blob: 2112e702b331662c502b375c0d561e6bd873dcb6 (plain) 
1
2
3
4
5
6
7
8
9
10
11

% 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