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

% EXPECT: sat
% EXIT: 10
%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