summaryrefslogtreecommitdiff
path: root/test/regress/regress0/boolean-terms.cvc
blob: 00bcf389179e6d93e8f0be0d9f56c269af840c27 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

% EXPECT: sat
%OPTION "produce-models";

f : BOOLEAN -> INT;
x : INT;
p : BOOLEAN -> BOOLEAN;

ASSERT f(p(TRUE)) = x;
ASSERT f(p(FALSE)) = x + 1;

CHECKSAT;
%GET_VALUE f(p(TRUE));
%GET_VALUE f(p(TRUE)) = x;
%GET_VALUE f(p(FALSE)) = x + 1;
%COUNTERMODEL;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback