diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 18:31:53 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 18:31:53 -0700 |
| commit | 38a81d249bdc1f40359a7d2c74b33c7a198bc551 (patch) | |
| tree | 9a0bc1734ae11126304c4f11f1ace35bbe384277 /Source/Dafny/Translator.cs | |
| parent | ee3d7dcd4eaf1694336ae8f12672bd9e8fa37389 (diff) | |
Dafny: fixed bug in induction-tactic heuristic (should never pick values whose type is a type parameter)
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 |
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);
|