Fix a bug in cloning of nested lambda expressions in AI engine

3 files changed, 11 insertions, 3 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index e677f85c..0f29c9a0 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -390,7 +390,7 @@ namespace Microsoft.Boogie {
           if (innerquant.arg.dummyIndex > 0) {

             realquant = innerquant.arg.RealQuantifier;

           } else {

-            realquant = (QuantifierExpr)RealQuantifier.Clone();

+            realquant = (BinderExpr)RealQuantifier.Clone();

             VariableSeq/*!*/ newdummies = new VariableSeq();

             newdummies.Add(Param);

             newdummies.AddRange(innerquant.arg.RealQuantifier.Dummies);

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));
+}
+