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);
       }
   }