Clarify the inlining warning.

1 files changed, 2 insertions, 6 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e2c45558..83078fb5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -12956,12 +12956,8 @@ namespace Microsoft.Dafny {
           } else {

             // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger

             // CLEMENT: Report inlining issue in a VS plugin friendly way

-            var info = new AdditionalInformation {

-              Token = fexp.tok,

-              Length = fexp.tok.val.Length,

-              Text = "This call cannot be safely inlined.",

-            };

-            Resolver.DefaultInformationReporter(info);

+            //CLEMENT this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy

+            Dafny.Util.ReportIssue("Info", fexp.tok, "Some instances of this call cannot safely be inlined.");

           }

         }