From 7ae95fdc63d65bf9768f07a873d36f87842da0cf Mon Sep 17 00:00:00 2001
From: Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com>
Date: Wed, 16 Nov 2011 10:34:45 +0530
Subject: Debugging output for stratified inlining. Emit attribute on Ensures
 while printing it.

---
 Source/Core/Absy.cs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Source/Core/Absy.cs')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0c9538d4..32b27ae6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2112,6 +2112,7 @@ namespace Microsoft.Boogie {
         stream.WriteLine(this, level, "// " + Comment);
       }
       stream.Write(this, level, "{0}ensures ", Free ? "free " : "");
+      Cmd.EmitAttributes(stream, Attributes);
       this.Condition.Emit(stream);
       stream.WriteLine(";");
     }
-- 
cgit v1.2.3