Make it preserve the fact that the value of an assumption variable never becomes logically weaker after a havoc.

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) {