Fixed issue in the verification result caching.

1 files changed, 2 insertions, 2 deletions

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;

       }