From 1d83074ef6903514110415f24b092e52740aa7bf Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 11 Feb 2011 19:55:36 +0000
Subject: Fix a bug in cloning of nested lambda expressions in AI engine

---
 Test/test2/Answer     | 4 ++--
 Test/test2/Lambda.bpl | 8 ++++++++
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index ca050273..f9d9a92e 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -363,7 +363,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Lambda.bpl(36,5): anon0
 
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 2 errors
 
 -------------------- LambdaPoly.bpl --------------------
 LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
@@ -419,7 +419,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Lambda.bpl(36,5): anon0
 
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 2 errors
 
 -------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
 TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
index 177900f4..477d0f36 100644
--- a/Test/test2/Lambda.bpl
+++ b/Test/test2/Lambda.bpl
@@ -55,3 +55,11 @@ procedure a()
   assert diff(a,b)[1];
   assert !diff(a,b)[2];
 }
+
+procedure nestedLambda()
+{
+  var a: [int][int]int;
+
+  a := (lambda x: int :: (lambda y: int :: x+y));
+}
+
-- 
cgit v1.2.3