diff options
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 12 |
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)
{
|