Did some refactoring, fixed minor issues, and made it apply the more advanced verification result caching even for implementations with errors.

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bfff8f0e..be3ab95d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2957,7 +2957,7 @@ namespace VC {
       {

         AssertEnsuresCmd assertCmd = (AssertEnsuresCmd)cmd;

         Contract.Assert(assertCmd != null);

-        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo, context);

+        ReturnCounterexample rc = new ReturnCounterexample(trace, transferCmd, assertCmd.Ensures, errModel, mvInfo, context, cmd.Checksum);

         rc.relatedInformation = relatedInformation;

         return rc;

       }