summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug596b.cvc
blob: 4765e03b2ba04cd09411772b07be42b3c7a4dcd0 (plain) 
1
2
3
4
5
6
7

% EXPECT: sat

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

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