Fix issue in computation of checksums for calls.

2 files changed, 4 insertions, 7 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 838699c1..d9176ca9 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1999,7 +1999,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ callee { get; set; }

     public Procedure Proc;

     public LocalVariable AssignedAssumptionVariable;

-    public bool EmitDependencyChecksum;

+    public string ProcDependencyChecksumInPreviousSnapshot { get; set; }

 

     // Element of the following lists can be null, which means that

     // the call happens with * as these parameters

@@ -2087,9 +2087,9 @@ namespace Microsoft.Boogie {
         stream.Write(" := ");

       }

       stream.Write(TokenTextWriter.SanitizeIdentifier(callee));

-      if (stream.UseForComputingChecksums && EmitDependencyChecksum)

+      if (stream.UseForComputingChecksums)

       {

-        var c = Proc.DependencyChecksum;

+        var c = ProcDependencyChecksumInPreviousSnapshot != null ? ProcDependencyChecksumInPreviousSnapshot : Proc.DependencyChecksum;

         if (c != null)

         {

           stream.Write(string.Format("[dependency_checksum:{0}]", c));

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 1de1a0ce..3d145c53 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -253,10 +253,7 @@ namespace Microsoft.Boogie
           var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

 

           node.ExtendDesugaring(before, new List<Cmd> { assumed });

-        }

-        else

-        {

-          node.EmitDependencyChecksum = true;

+          node.ProcDependencyChecksumInPreviousSnapshot = oldProc.DependencyChecksum;

         }

       }