From 2920db784b61f02b6d68e249bc3b1c6d1cf26efd Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Fri, 12 Jun 2015 08:28:07 +0200
Subject: Fix issue with computation of statement checksums for lambda
 expressions.

---
 Source/Core/Absy.cs         |  2 ++
 Source/Core/AbsyExpr.cs     | 10 +++++++++-
 Source/Core/LambdaHelper.cs |  1 +
 3 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 56bfc90f..0fedcd44 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2630,6 +2630,8 @@ namespace Microsoft.Boogie {
     private bool neverTrigger;
     private bool neverTriggerComputed;
 
+    public string OriginalLambdaExprAsString;
+
     public Function(IToken tok, string name, List<Variable> args, Variable result)
       : this(tok, name, new List<TypeVariable>(), args, result, null) {
       Contract.Requires(result != null);
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index c19140d7..c816d7f2 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1983,7 +1983,15 @@ namespace Microsoft.Boogie {
     virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
       //Contract.Requires(stream != null);
       //Contract.Requires(args != null);
-      this.name.Emit(stream, 0xF0, false);
+
+      if (stream.UseForComputingChecksums && Func.OriginalLambdaExprAsString != null)
+      {
+        stream.Write(Func.OriginalLambdaExprAsString);
+      }
+      else
+      {
+        this.name.Emit(stream, 0xF0, false);
+      }
       if (stream.UseForComputingChecksums)
       {
         var c = Func.DependencyChecksum;
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index 0d115777..a2b0f143 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -176,6 +176,7 @@ namespace Microsoft.Boogie {
           }
           Function fn = new Function(tok, FreshLambdaFunctionName(), freshTypeVars, formals, res, "auto-generated lambda function",
             Substituter.Apply(Substituter.SubstitutionFromHashtable(substFnAttrs), lambdaAttrs));
+          fn.OriginalLambdaExprAsString = lam_str;
 
           fcall = new FunctionCall(new IdentifierExpr(tok, fn.Name));
           fcall.Func = fn;  // resolve here
-- 
cgit v1.2.3