InlineAssume attribute for ensures clauses; if present, the ensures condition is assumed while inlining.

1 files changed, 4 insertions, 1 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index d8adf7d3..6bb2d4db 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -296,7 +296,10 @@ namespace Microsoft.Boogie.Houdini {
   public class InlineEnsuresVisitor : ReadOnlyVisitor {

       public override Ensures VisitEnsures(Ensures ensures)

       {

-          ensures.Attributes = new QKeyValue(Token.NoToken, "HoudiniAssume", new List<object>(), ensures.Attributes);

+          if (!ensures.Free)

+          {

+              ensures.Attributes = new QKeyValue(Token.NoToken, "InlineAssume", new List<object>(), ensures.Attributes);

+          }

           return base.VisitEnsures(ensures);

       }

   }