Add isConst check for lambda expressions. (#1084)

Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.

1 files changed, 2 insertions, 1 deletions

diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc
index aee61a533..548623954 100644
--- a/test/regress/regress0/print_lambda.cvc
+++ b/test/regress/regress0/print_lambda.cvc
@@ -1,6 +1,7 @@
+% 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(_ufmt_1:INT): 0);
+% EXPECT: f : (INT) -> INT = (LAMBDA(VAR:INT): 0);
 
 f : INT -> INT;
 ASSERT f(1) = 0;