summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r--Source/Dafny/Translator.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f89ded6a..f224f35e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5555,7 +5555,7 @@ namespace Microsoft.Dafny {
// consider automatically applying induction
var inductionVariables = new List<BoundVar>();
foreach (var n in e.BoundVars) {
- if (VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
+ if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
new Printer(Console.Out).PrintExpression(e);