1 2 3 4 5 6 7 8 9 10
% SCRUBBER: sed -e 's/f : (INT) -> INT = (LAMBDA(.*:INT): 0);$/f : (INT) -> INT = (LAMBDA(VAR:INT): 0);/' % COMMAND-LINE: --produce-models % EXPECT: sat % EXPECT: f : (INT) -> INT = (LAMBDA(VAR:INT): 0); f : INT -> INT; ASSERT f(1) = 0; CHECKSAT; COUNTEREXAMPLE;