3 files changed, 14 insertions, 6 deletions
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 8c85d5df..1f9518b5 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -485,8 +485,8 @@ procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
   }
 }
 
-procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
-procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
+procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
 
 implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
   $result := (a$in == b$in);
@@ -500,19 +500,19 @@ implementation System.String.op_Inequality$System.String$System.String(a$in: Ref
 var isControlEnabled: [Ref]bool;
 var isControlChecked: [Ref]bool;
 
-procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
+procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
 implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool) {
   isControlEnabled[$this] := value$in;
 }
 
-procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
+procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
 implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref) {
   var enabledness: bool;
   enabledness := isControlEnabled[$this];
   $result := Box2Ref(Bool2Box(enabledness));
 }
 
-procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
 implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {
   var check: bool;
 
@@ -520,7 +520,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
   isControlChecked[$this] := check;
 }
 
-procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
 implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref) {
   var isChecked: bool;
   isChecked := isControlChecked[$this];
diff --git a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
index 5bc32f57..97935721 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
@@ -13,10 +13,14 @@ namespace BytecodeTranslator.Phone {
     private bool changedOnLastPass = false;
     private IAssemblyReference assemblyBeingTranslated;
 
+    public int TotalMethodsCount { get; private set; }
+    public int InlinedMethodsCount { get { return methodsToInline.Count(); } }
+
     public PhoneMethodInliningMetadataTraverser(PhoneCodeHelper phoneHelper) {
       methodsToInline = new HashSet<IMethodDefinition>();
       iterMethodsToInline = new HashSet<IMethodDefinition>();
       this.phoneHelper = phoneHelper;
+      TotalMethodsCount = 0;
     }
 
     public override void Visit(IEnumerable<IModule> modules) {
@@ -28,6 +32,9 @@ namespace BytecodeTranslator.Phone {
     }
 
     public override void Visit(IMethodDefinition method) {
+      if (!firstPassDone)
+        TotalMethodsCount++;
+
       if (iterMethodsToInline.Contains(method) || (!firstPassDone && phoneHelper.mustInlineMethod(method))) {
         PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser();
         codeTraverser.Visit(method);
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4c046b24..d921c481 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -317,6 +317,7 @@ namespace BytecodeTranslator {
           new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance());
         inlineTraverser.findAllMethodsToInline(modules);
         updateInlinedMethods(sink, inlineTraverser.getMethodsToInline());
+        System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
       }
 
       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");