summaryrefslogtreecommitdiff
path: root/test/regress/regress0/print_model.cvc
blob: 0ad9ddf4cbf70356286cf223c1b67e62f4a5a745 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

% COMMAND-LINE: --produce-models
% EXPECT: sat
% EXPECT: MODEL BEGIN
% EXPECT: s1 : INT = 2;
% EXPECT: s2 : INT = 1;
% EXPECT: MODEL END;

OPTION "produce-models";
s1, s2 : INT;
ASSERT s1 = 2;
CHECKSAT s2 > 0 AND s2 < s1;
COUNTERMODEL;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback