Fixed issue in the verification result caching.

2 files changed, 10 insertions, 6 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 640b0db2..178f8ddb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -84,6 +84,7 @@ namespace Microsoft.Boogie {
     public string OriginalRequestId;

     public string RequestId;

     public abstract byte[] Checksum { get; }

+    public byte[] SugaredCmdChecksum;

 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

@@ -420,7 +421,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

@@ -429,20 +430,23 @@ namespace Microsoft.Boogie {
       Contract.Requires(failingRequires != null);

       this.FailingCall = failingCall;

       this.FailingRequires = failingRequires;

+      this.checksum = checksum;

+      this.SugaredCmdChecksum = failingCall.Checksum;

     }

 

     public override int GetLocation() {

       return FailingCall.tok.line * 1000 + FailingCall.tok.col;

     }

 

+    byte[] checksum;

     public override byte[] Checksum

     {

-      get { return FailingCall.Checksum; }

+      get { return checksum; }

     }

 

     public override Counterexample Clone()

     {

-        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);

+        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -1540,7 +1544,7 @@ namespace VC {
         var dropCmd = false;

         var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

         var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

-        var checksum = pc.SugaredCmdChecksum != null ? pc.SugaredCmdChecksum : pc.Checksum;

+        var checksum = pc.Checksum;

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index d92f8661..5e83a337 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1626,7 +1626,7 @@ namespace VC {
         outcome = Outcome.Errors;

         foreach (var a in impl.RecycledFailingAssertions)

         {

-          var checksum = a.SugaredCmdChecksum != null ? a.SugaredCmdChecksum : a.Checksum;

+          var checksum = a.Checksum;

           var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;

           if (oldCex != null)

           {

@@ -2965,7 +2965,7 @@ namespace VC {
       {

         AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;

         Contract.Assert(assertCmd != null);

-        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context);

+        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context, assertCmd.Checksum);

         cc.relatedInformation = relatedInformation;

         return cc;

       }