From 3b4b2d1ee8b260b450274ee0ad86d0d2d6743210 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 17 Sep 2014 22:43:09 -0700
Subject: fixed a bug in inlining changed the attribute on callee ensures to
 "HoudiniAssume" rather than "assume"

---
 Source/Houdini/AbstractHoudini.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/Houdini/AbstractHoudini.cs')

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 716456ea..49273f94 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("assume", en.Attributes);
+                    en.Attributes = removeAttr("HoudiniAssume", en.Attributes);
 
                 proc.Ensures = nensures;
             }
-- 
cgit v1.2.3