1 files changed, 14 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 515ec16d..206e0ee7 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1742,8 +1742,8 @@ namespace VC {
         Contract.Assert(c != null);
         // If an assumption variable for postconditions is included here, it must have been assigned within a loop.
         // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop
-        // invariant) in the previous snapshot and are therefore not going refer to the assumption variable after
-        // the loop. We can achieve this by simply not updating/adding it in the incarnation map.
+        // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the
+        // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map.
         List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList();
         // First, compute the new incarnations
         foreach (IdentifierExpr ie in havocVars) {
@@ -1767,6 +1767,18 @@ namespace VC {
             }
           }
         }
+
+        // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one:
+        // assume v_post ==> v_pre;
+        foreach (IdentifierExpr ie in havocVars)
+        {
+          if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption"))
+          {
+            var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone());
+            var postInc = (Expr)(incarnationMap[ie.Decl].Clone());
+            passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc)));
+          }
+        }
       }
       #endregion
  else if (c is CommentCmd) {