Added lazy summary computation to stratified inlining (not finished yet)

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index ae051b40..676ffd5a 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2161,6 +2161,11 @@ namespace Microsoft.Boogie {
         {

             assume.Attributes = Attributes;

         }

+        if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))

+        {

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

+            assume.Attributes.Params.Add(this.callee);

+        }

         #endregion

         newBlockBody.Add(assume);

       }