summaryrefslogtreecommitdiff
path: root/test/regress/regress0/parser/choice.cvc
blob: e0ebac051e3fd2d4616a7057cedabdf1c8622bb1 (plain) 
1
2
3
4
5
6
7
8
9
10

% EXPECT: sat

a : INT;
b : INT;
c : INT;

ASSERT (CHOICE(x: INT): x = a) = 1;
ASSERT (CHOICE(x: INT): x = b) = 2;

CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback