summaryrefslogtreecommitdiff
path: root/Source/Dafny/Resolver.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Resolver.cs')
-rw-r--r--Source/Dafny/Resolver.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2e4c0c00..4c354e6a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1560,7 +1560,10 @@ namespace Microsoft.Dafny
var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
if (status != TailRecursionStatus.NotTailRecursive) {
m.IsTailRecursive = true;
- ReportAdditionalInformation(m.tok, "tail recursive", m.Name.Length);
+ if (tailCall != null) {
+ // this means there was at least one recursive call
+ ReportAdditionalInformation(m.tok, "tail recursive", m.Name.Length);
+ }
}
}
}