1 2 3 4 5 6 7 8 9 10
; COMMAND-LINE: --produce-models ; EXPECT: sat ; EXPECT: f : (INT) -> INT = (LAMBDA(_ufmt_1:INT): 0); ; EXIT: 10 f : INT -> INT; ASSERT f(1) = 0; CHECKSAT; COUNTEREXAMPLE;