a fix in Inline method; it should look for inline attribute only on procedures and implementations

1 files changed, 8 insertions, 4 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 2f75b234..5e1d75ed 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -726,6 +726,10 @@ namespace Microsoft.Boogie
     public static void Inline(Program program)

     {

       Contract.Requires(program != null);

+      

+      if (CommandLineOptions.Clo.Trace)

+          Console.WriteLine("Inlining...");

+

       // Inline

       var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);

 

@@ -734,10 +738,10 @@ namespace Microsoft.Boogie
         bool inline = false;

         foreach (var d in TopLevelDeclarations)

         {

-          if (d.FindExprAttribute("inline") != null)

-          {

-            inline = true;

-          }

+            if ((d is Procedure || d is Implementation) && d.FindExprAttribute("inline") != null)

+            {

+                inline = true;

+            }

         }

         if (inline)

         {