% 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;