Boogie: Fixed a crash due to old expressions in lambda expressions that were not replaced after lambda expansion.

(reported by Florian Egli)

1 files changed, 4 insertions, 0 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 486f940f..36b9edc2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2388,6 +2388,10 @@ namespace VC {
           Block entryBlock = cce.NonNull( impl.Blocks[0]);

           cmds.AddRange(entryBlock.Cmds);

           entryBlock.Cmds = cmds;

+          // Make sure that all added commands are passive commands.

+          Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());

+          TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,

+                               ComputeOldExpressionSubstitution(impl.Proc.Modifies));

         }

       }