diff options
author | 2011-05-26 18:31:53 -0700 | |
---|---|---|
committer | 2011-05-26 18:31:53 -0700 | |
commit | 38a81d249bdc1f40359a7d2c74b33c7a198bc551 (patch) | |
tree | 9a0bc1734ae11126304c4f11f1ace35bbe384277 | |
parent | ee3d7dcd4eaf1694336ae8f12672bd9e8fa37389 (diff) |
Dafny: fixed bug in induction-tactic heuristic (should never pick values whose type is a type parameter)
-rw-r--r-- | Source/Dafny/Translator.cs | 2 | ||||
-rw-r--r-- | Test/dafny1/Answer | 2 | ||||
-rw-r--r-- | Test/dafny1/Induction.dfy | 13 |
3 files changed, 15 insertions, 2 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);
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 0111f9af..5ee9f921 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -81,7 +81,7 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 29 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index d785eead..7c7d3baf 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -156,6 +156,19 @@ class DatatypeInduction<T> { }
// see also Test/dafny0/DTypes.dfy for more variations of this example
+
+ function OccurrenceCount<T>(tree: Tree<T>, x: T): int
+ {
+ match tree
+ case Leaf(t) => if x == t then 1 else 0
+ case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
+ }
+ method RegressionTest(tree: Tree<T>)
+ // the translation of the following line once crashed Dafny
+ requires forall y :: 0 <= OccurrenceCount(tree, y);
+ {
+ }
+
}
// ----------------------- Induction and case splits -----------------
|