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

% COMMAND-LINE: --produce-models
% EXPECT: sat
% EXPECT: f : (INT) -> INT = (LAMBDA(_ufmt_1:INT): 0);
% EXIT: 10

f : INT -> INT;
ASSERT f(1) = 0;
CHECKSAT;
COUNTEREXAMPLE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback