Change class 'LambdaVisitor' to attach checksum to expanded lambda functions.

1 files changed, 14 insertions, 0 deletions

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index a727dc95..51c9ee23 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -93,6 +93,20 @@ namespace Microsoft.Boogie {
           Substituter.SubstitutionFromHashtable(oldSubst),

           lambda.Attributes);

 

+        if (CommandLineOptions.Clo.VerifySnapshots && QKeyValue.FindStringAttribute(lambdaAttrs, "checksum") == null)

+        {

+          // Attach a dummy checksum to avoid issues in the dependency analysis.

+          var checksumAttr = new QKeyValue(lambda.tok, "checksum", new List<object> { "dummy" }, null);

+          if (lambdaAttrs == null)

+          {

+            lambdaAttrs = checksumAttr;

+          }

+          else

+          {

+            lambdaAttrs.AddLast(checksumAttr);

+          }

+        }

+

         // this is ugly, the output will depend on hashing order

         var subst = new Dictionary<Variable, Expr>();

         var substFnAttrs = new Dictionary<Variable, Expr>();