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

12 files changed, 309 insertions, 38 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9a871e93..2f4b4e8a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2617,6 +2617,71 @@ namespace Microsoft.Boogie {
     public List<Block/*!*/> OriginalBlocks;

     public List<Variable> OriginalLocVars;

 

+    ISet<byte[]> assertionChecksums;

+    public ISet<byte[]> AssertionChecksums

+    {

+      get

+      {

+        return assertionChecksums;

+      }

+    }

+

+    sealed class ChecksumComparer : IEqualityComparer<byte[]>

+    {

+      static IEqualityComparer<byte[]> defaultComparer;

+      public static IEqualityComparer<byte[]> Default

+      {

+        get

+        {

+          if (defaultComparer == null)

+          {

+            defaultComparer = new ChecksumComparer();

+          }

+          return defaultComparer;

+        }

+      }

+

+      public bool Equals(byte[] x, byte[] y)

+      {

+        if (x == null || y == null)

+        {

+          return x == y;

+        }

+        else

+        {

+          return x.SequenceEqual(y);

+        }

+      }

+

+      public int GetHashCode(byte[] checksum)

+      {

+        if (checksum == null)

+        {

+          throw new ArgumentNullException("checksum");

+        }

+        else

+        {

+          var result = 17;

+          for (int i = 0; i < checksum.Length; i++)

+          {

+            result = result * 23 + checksum[i];

+          }

+          return result;

+        }

+      }

+    }

+

+    public void AddAssertionChecksum(byte[] checksum)

+    {

+      if (assertionChecksums == null)

+      {

+        assertionChecksums = new HashSet<byte[]>(ChecksumComparer.Default);

+      }

+      assertionChecksums.Add(checksum);

+    }

+

+    public ISet<byte[]> AssertionChecksumsInPreviousSnapshot { get; set; }

+

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

     [ContractInvariantMethod]

@@ -2688,14 +2753,18 @@ namespace Microsoft.Boogie {
       }

     }

 

-    // TODO(wuestholz): Make this a 'List<Counterexample>'.

-    public IList<object> ErrorsInCachedSnapshot { get; set; }

+    public ISet<byte[]> ErrorChecksumsInCachedSnapshot { get; private set; }

+

+    public void SetErrorChecksumsInCachedSnapshot(IEnumerable<byte[]> errorChecksums)

+    {

+      ErrorChecksumsInCachedSnapshot = new HashSet<byte[]>(errorChecksums, ChecksumComparer.Default);

+    }

 

     public bool NoErrorsInCachedSnapshot

     {

       get

       {

-        return ErrorsInCachedSnapshot != null && !ErrorsInCachedSnapshot.Any();

+        return ErrorChecksumsInCachedSnapshot != null && !ErrorChecksumsInCachedSnapshot.Any();

       }

     }

 

@@ -2703,7 +2772,7 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        return ErrorsInCachedSnapshot != null && ErrorsInCachedSnapshot.Any();

+        return ErrorChecksumsInCachedSnapshot != null && ErrorChecksumsInCachedSnapshot.Any();

       }

     }

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index a7693b00..869c0dfa 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -800,6 +800,8 @@ namespace Microsoft.Boogie {
     [Rep]  //PM: needed to verify Traverse.Visit

     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)

 

+    public byte[] Checksum;

+

     // Abstract interpretation

 

     // public bool currentlyTraversed;

@@ -937,8 +939,104 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

   }

+

+  public static class ChecksumHelper

+  {

+    public static void ComputeChecksums(Cmd cmd, Implementation impl, byte[] currentChecksum = null, bool unordered = false)

+    {

+      if (CommandLineOptions.Clo.VerifySnapshots < 2)

+      {

+        return;

+      }

+

+      var assumeCmd = cmd as AssumeCmd;

+      if (assumeCmd != null

+          && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization"))

+      {

+        // Ignore assumption variable initializations.

+        assumeCmd.Checksum = currentChecksum;

+        return;

+      }

+

+      using (var strWr = new System.IO.StringWriter())

+      using (var tokTxtWr = new TokenTextWriter("<no file>", strWr, false, false))

+      {

+        tokTxtWr.UseForComputingChecksums = true;

+        cmd.Emit(tokTxtWr, 0);

+        var md5 = System.Security.Cryptography.MD5.Create();

+        var str = strWr.ToString();

+        if (str.Any())

+        {

+          var data = System.Text.Encoding.UTF8.GetBytes(str);

+          var checksum = md5.ComputeHash(data);

+          currentChecksum = currentChecksum != null ? CombineChecksums(currentChecksum, checksum, unordered) : checksum;

+        }

+        cmd.Checksum = currentChecksum;

+      }

+

+      var assertCmd = cmd as AssertCmd;

+      if (assertCmd != null && assertCmd.Checksum != null)

+      {

+        var assertRequiresCmd = assertCmd as AssertRequiresCmd;

+        if (assertRequiresCmd != null)

+        {

+          // Add the checksum of the call instead of the assertion itself

+          // because a corresponding counterexample will also have the

+          // checksum of the failing call.

+          impl.AddAssertionChecksum(assertRequiresCmd.Call.Checksum);

+        }

+        else

+        {

+          impl.AddAssertionChecksum(assertCmd.Checksum);

+        }

+      }

+

+      var sugaredCmd = cmd as SugaredCmd;

+      if (sugaredCmd != null)

+      {

+        // The checksum of a sugared command should not depend on the desugaring itself.

+        var stateCmd = sugaredCmd.Desugaring as StateCmd;

+        if (stateCmd != null)

+        {

+          foreach (var c in stateCmd.Cmds)

+          {

+            ComputeChecksums(c, impl, currentChecksum, unordered);

+            currentChecksum = c.Checksum;

+          }

+          sugaredCmd.DesugaringChecksum = currentChecksum;

+        }

+        else

+        {

+          ComputeChecksums(sugaredCmd.Desugaring, impl, currentChecksum, unordered);

+          sugaredCmd.DesugaringChecksum = sugaredCmd.Desugaring.Checksum;

+        }

+      }

+    }

+

+    public static byte[] CombineChecksums(byte[] first, byte[] second, bool unordered = false)

+    {

+      Contract.Requires(first != null && (second == null || first.Length == second.Length));

+

+      var result = (byte[])(first.Clone());

+      for (int i = 0; second != null && i < second.Length; i++)

+      {

+        if (unordered)

+        {

+          result[i] += second[i];

+        }

+        else

+        {

+          result[i] = (byte)(result[i] * 31 ^ second[i]);

+        }

+      }

+      return result;

+    }

+  }

+

   [ContractClass(typeof(CmdContracts))]

   public abstract class Cmd : Absy {

+    public byte[] Checksum { get; internal set; }

+

     public Cmd(IToken/*!*/ tok)

       : base(tok) {

       Contract.Assert(tok != null);

@@ -1046,6 +1144,9 @@ namespace Microsoft.Boogie {
     /// </summary>

     public static void EmitAttributes(TokenTextWriter stream, QKeyValue attributes) {

       Contract.Requires(stream != null);

+

+      if (stream.UseForComputingChecksums) { return; }

+

       for (QKeyValue kv = attributes; kv != null; kv = kv.Next) {

         kv.Emit(stream);

         stream.Write(" ");

@@ -1170,6 +1271,14 @@ namespace Microsoft.Boogie {
     }

 

     public override void Emit(TokenTextWriter stream, int level) {

+      if (stream.UseForComputingChecksums)

+      {

+        var lhs = Lhss.FirstOrDefault() as SimpleAssignLhs;

+        if (lhs != null && lhs.AssignedVariable.Decl != null && QKeyValue.FindBoolAttribute(lhs.AssignedVariable.Decl.Attributes, "assumption"))

+        {

+          return;

+        }

+      }

       

       stream.Write(this, level, "");

 

@@ -1651,6 +1760,8 @@ namespace Microsoft.Boogie {
   abstract public class SugaredCmd : Cmd {

     private Cmd desugaring;  // null until desugared

 

+    public byte[] DesugaringChecksum { get; set; }

+

     public SugaredCmd(IToken/*!*/ tok)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -1702,7 +1813,7 @@ namespace Microsoft.Boogie {
 

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

-      if (CommandLineOptions.Clo.PrintDesugarings) {

+      if (CommandLineOptions.Clo.PrintDesugarings && !stream.UseForComputingChecksums) {

         stream.WriteLine(this, level, "/*** desugaring:");

         Desugaring.Emit(stream, level);

         stream.WriteLine(level, "**** end desugaring */");

@@ -2429,7 +2540,7 @@ namespace Microsoft.Boogie {
       return Conjunction(ensures);

     }

 

-    public Expr Precondition(Procedure procedure, Program program)

+    public Expr CheckedPrecondition(Procedure procedure, Program program)

     {

       Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

 

@@ -2583,6 +2694,11 @@ namespace Microsoft.Boogie {
       stream.Write(this, level, "assert ");

       EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

+      if (1 < CommandLineOptions.Clo.VerifySnapshots && !stream.UseForComputingChecksums)

+      {

+        var cs = Checksum != null ? BitConverter.ToString(Checksum) : "<unknown>";

+        stream.Write(string.Format(" /* checksum: {0} */ ", cs));

+      }

       stream.WriteLine(";");

     }

     public override void Resolve(ResolutionContext rc) {

@@ -2737,6 +2853,9 @@ namespace Microsoft.Boogie {
     }

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

+

+      if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

+

       stream.Write(this, level, "assume ");

       EmitAttributes(stream, Attributes);

       this.Expr.Emit(stream);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index d6dd17c9..ffd95f77 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1802,6 +1802,10 @@ namespace Microsoft.Boogie {
       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

       this.name.Emit(stream, 0xF0, false);

+      if (stream.UseForComputingChecksums && Func.DependenciesChecksum != null)

+      {

+        stream.Write(string.Format("[dependencies_checksum:{0}]", Func.DependenciesChecksum));

+      }

       stream.Write("(");

       args.Emit(stream);

       stream.Write(")");

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 66eefd8c..6aafec7f 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -80,6 +80,7 @@ namespace Microsoft.Boogie {
     bool setTokens = true;

     int line = 1;

     int col;

+    public bool UseForComputingChecksums;

 

     private const int indent_size = 2;

     protected static string Indent(int level) {

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 21e29c44..48a35e80 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -316,7 +316,7 @@ namespace Microsoft.Boogie
   #endregion

 

 

-  public class VerificationResult

+  public sealed class VerificationResult

   {

     public readonly string RequestId;

     public readonly string Checksum;

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 58423f24..1f92c4ac 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Boogie
   }

 

 

-  class CachedVerificationResultInjectorStatistics

+  sealed class CachedVerificationResultInjectorStatistics

   {

     ConcurrentDictionary<string, CachedVerificationResultInjectorRun> runs = new ConcurrentDictionary<string, CachedVerificationResultInjectorRun>();

 

@@ -63,7 +63,7 @@ namespace Microsoft.Boogie
   }

 

 

-  class CachedVerificationResultInjector : StandardVisitor

+  sealed class CachedVerificationResultInjector : StandardVisitor

   {

     readonly IEnumerable<Implementation> Implementations;

     readonly Program Program;

@@ -106,6 +106,12 @@ namespace Microsoft.Boogie
       assumptionVariableCount = 0;

       temporaryVariableCount = 0;

       currentImplementation = implementation;

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      var implPrevSnap = programInCachedSnapshot.Implementations().FirstOrDefault(i => i.Id == implementation.Id);

+      if (implPrevSnap != null)

+      {

+        currentImplementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

+      }

       var result = VisitImplementation(implementation);

       currentImplementation = null;

       this.programInCachedSnapshot = null;

@@ -128,13 +134,13 @@ namespace Microsoft.Boogie
             run.LowPriorityImplementationCount++;

             if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

             {

-              if (vr.Errors != null)

+              if (vr.Errors != null && vr.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

               {

-                impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();

+                impl.SetErrorChecksumsInCachedSnapshot(vr.Errors.Select(cex => cex.Checksum));

               }

               else if (vr.Outcome == ConditionGeneration.Outcome.Correct)

               {

-                impl.ErrorsInCachedSnapshot = new List<object>();

+                impl.SetErrorChecksumsInCachedSnapshot(new List<byte[]>());

               }

               if (vr.ProgramId != null)

               {

@@ -183,17 +189,12 @@ namespace Microsoft.Boogie
         currentImplementation.InjectAssumptionVariable(lv);

 

         var before = new List<Cmd>();

-        if (currentImplementation.NoErrorsInCachedSnapshot

-            && oldProc.Requires.Any())

+        if (oldProc.Requires.Any())

         {

-          var pre = node.Precondition(oldProc, Program);

+          var pre = node.CheckedPrecondition(oldProc, Program);

           var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

           before.Add(assume);

         }

-        else if (currentImplementation.AnyErrorsInCachedSnapshot)

-        {

-          // TODO(wuestholz): Add an assume statement if the precondition was verified in the previous snapshot.

-        }

 

         var post = node.Postcondition(oldProc, Program);

         var mods = node.UnmodifiedBefore(oldProc);

@@ -219,7 +220,7 @@ namespace Microsoft.Boogie
   }

 

 

-  public class OtherDefinitionAxiomsCollector : ReadOnlyVisitor

+  sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor

   {

     Axiom currentAxiom;

     Trigger currentTrigger;

@@ -265,7 +266,7 @@ namespace Microsoft.Boogie
   }

 

 

-  class DependencyCollector : ReadOnlyVisitor

+  sealed class DependencyCollector : ReadOnlyVisitor

   {

     private HashSet<Procedure> procedureDependencies;

     private HashSet<Function> functionDependencies;

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

 

 

-  public class VerificationResultCache

+  public sealed class VerificationResultCache

   {

     private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache");

     private readonly CacheItemPolicy Policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 0898641b..9d8669dd 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -82,6 +82,7 @@ namespace Microsoft.Boogie {
     [Peer]

     public List<string>/*!>!*/ relatedInformation;

     public string RequestId;

+    public abstract byte[] Checksum { get; }

 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

@@ -395,6 +396,11 @@ namespace Microsoft.Boogie {
       return FailingAssert.tok.line * 1000 + FailingAssert.tok.col;

     }

 

+    public override byte[] Checksum

+    {

+      get { return FailingAssert.Checksum; }

+    }

+

     public override Counterexample Clone()

     {

         var ret = new AssertCounterexample(Trace, FailingAssert, Model, MvInfo, Context);

@@ -428,6 +434,11 @@ namespace Microsoft.Boogie {
       return FailingCall.tok.line * 1000 + FailingCall.tok.col;

     }

 

+    public override byte[] Checksum

+    {

+      get { return FailingCall.Checksum; }

+    }

+

     public override Counterexample Clone()

     {

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

@@ -446,7 +457,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public ReturnCounterexample(List<Block> trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public ReturnCounterexample(List<Block> trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum)

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

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

@@ -455,15 +466,29 @@ namespace Microsoft.Boogie {
       Contract.Requires(!failingEnsures.Free);

       this.FailingReturn = failingReturn;

       this.FailingEnsures = failingEnsures;

+      this.checksum = checksum;

     }

 

     public override int GetLocation() {

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

     }

 

+    byte[] checksum;

+

+    /// <summary>

+    /// Returns the checksum of the corresponding assertion.

+    /// </summary>

+    public override byte[] Checksum

+    {

+      get

+      {

+        return checksum;

+      }

+    }

+

     public override Counterexample Clone()

     {

-        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context);

+        var ret = new ReturnCounterexample(Trace, FailingReturn, FailingEnsures, Model, MvInfo, Context, checksum);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -1297,7 +1322,7 @@ namespace VC {
 

     Dictionary<Variable, Expr> preHavocIncarnationMap = null;     // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement

 

-    protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) {

+    protected void TurnIntoPassiveBlock(Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst, byte[] currentChecksum = null) {

       Contract.Requires(b != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(mvInfo != null);

@@ -1307,8 +1332,11 @@ namespace VC {
       List<Cmd> passiveCmds = new List<Cmd>();

       foreach (Cmd c in b.Cmds) {

         Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction

+        ChecksumHelper.ComputeChecksums(c, currentImplementation, currentChecksum);

+        currentChecksum = c.Checksum;

         TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);

       }

+      b.Checksum = currentChecksum;

       b.Cmds = passiveCmds;

 

       if (b.TransferCmd is ReturnExprCmd) {

@@ -1389,8 +1417,14 @@ namespace VC {
 

         // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, 

         // all its successors have been passified.  Consequently, its entry in block2Incarnation can be removed.

+        byte[] currentChecksum = null;

         foreach (Block p in b.Predecessors) {

           p.succCount--;

+          if (b.Checksum != null)

+          {

+            // Compute the checksum based on the checksums of the predecessor. The order should not matter.

+            currentChecksum = ChecksumHelper.CombineChecksums(b.Checksum, currentChecksum, true);

+          }

           if (p.succCount == 0)

             block2Incarnation.Remove(p);

         }

@@ -1407,7 +1441,7 @@ namespace VC {
         }

         #endregion Each block's map needs to be available to successor blocks

 

-        TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst);

+        TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst, currentChecksum);

         exitBlock = b;

         exitIncarnationMap = incarnationMap;

       }

@@ -1463,15 +1497,22 @@ namespace VC {
           }

         }

         Contract.Assert(copy != null);

+        var isAssumePre = false;

         if (pc is AssertCmd) {

           ((AssertCmd)pc).OrigExpr = pc.Expr;

           Contract.Assert(((AssertCmd)pc).IncarnationMap == null);

           ((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

 

           if (currentImplementation != null

-              && currentImplementation.NoErrorsInCachedSnapshot

-              && currentImplementation.InjectedAssumptionVariables != null

-              && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

+              && ((currentImplementation.NoErrorsInCachedSnapshot

+                   && currentImplementation.InjectedAssumptionVariables != null

+                   && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

+                  || (currentImplementation.AnyErrorsInCachedSnapshot

+                      && currentImplementation.InjectedAssumptionVariables != null

+                      && currentImplementation.InjectedAssumptionVariables.Any()

+                      && pc.Checksum != null

+                      && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))

+                      && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum))))

           {

             // Bind the assertion expression to a local variable.

             var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, new IdentifierExpr(Token.NoToken, CurrentTemporaryVariableForAssertions));

@@ -1483,21 +1524,25 @@ namespace VC {
             var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy);

             passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));

           }

-          else if (currentImplementation != null

-                   && currentImplementation.AnyErrorsInCachedSnapshot)

-          {

-            // TODO(wuestholz): Add an assume statement if the assertion was verified in the previous snapshot.

-          }

         }

         else if (pc is AssumeCmd

-                 && QKeyValue.FindStringAttribute(pc.Attributes, "precondition_previous_snapshot") != null

+                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")

                  && currentImplementation.InjectedAssumptionVariables != null

                  && currentImplementation.InjectedAssumptionVariables.Any())

         {

           copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy);

+          isAssumePre = true;

         }

         pc.Expr = copy;

-        passiveCmds.Add(pc);

+        if (!isAssumePre

+            || currentImplementation.NoErrorsInCachedSnapshot

+            || (currentImplementation.AnyErrorsInCachedSnapshot

+                && pc.Checksum != null

+                && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))

+                && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum)))

+        {

+          passiveCmds.Add(pc);

+        }

       }

       #endregion

       #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]

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;

       }

diff --git a/Test/snapshots/Snapshots19.v0.bpl b/Test/snapshots/Snapshots19.v0.bpl
new file mode 100644
index 00000000..935ee793
--- /dev/null
+++ b/Test/snapshots/Snapshots19.v0.bpl
@@ -0,0 +1,11 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    call N();

+

+    assert 1 != 1;

+}

+

+procedure {:checksum "2"} N();

+  requires 2 == 2;

diff --git a/Test/snapshots/Snapshots19.v1.bpl b/Test/snapshots/Snapshots19.v1.bpl
new file mode 100644
index 00000000..2afdd641
--- /dev/null
+++ b/Test/snapshots/Snapshots19.v1.bpl
@@ -0,0 +1,11 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    call N();

+

+    assert 1 != 1;

+}

+

+procedure {:checksum "3"} N();

+  requires 2 == 2;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index e2d566d8..b36e1aa2 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl > "%t"
+// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8b363791..554837e6 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -180,3 +180,13 @@ Execution trace:
     Snapshots18.v1.bpl(20,5): anon4

 

 Boogie program verifier finished with 0 verified, 2 errors

+Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots19.v0.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots19.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error