test/regress/regress0/print_lambda.cvc

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