From d1d367b1e9fb1cde673332030ef68b230c22dd06 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 18 Sep 2014 09:33:33 -0700
Subject: InlineAssume attribute for ensures clauses; if present, the ensures
 condition is assumed while inlining.

---
 Source/Houdini/AbstractHoudini.cs | 2 +-
 Source/Houdini/Houdini.cs         | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 49273f94..31b38e8a 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2412,7 +2412,7 @@ namespace Microsoft.Boogie.Houdini {
                     QKeyValue.FindStringAttribute(ens.Attributes, "post") == null)
                 .Iter(ens => nensures.Add(ens));
                 foreach (Ensures en in nensures)
-                    en.Attributes = removeAttr("HoudiniAssume", en.Attributes);
+                    en.Attributes = removeAttr("InlineAssume", en.Attributes);
 
                 proc.Ensures = nensures;
             }
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);
       }
   }
-- 
cgit v1.2.3