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

f : INT -> INT;
ASSERT f(1) = 0;
CHECKSAT;
COUNTEREXAMPLE;