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 | 1acd05253ea0fc614ac3e6a612be19a3f3bcf6a4 (patch) | |
| tree | 690ff82d9e2764aa54a076ad895bad0858dc25d1 | |
| parent | 3e31a8d7c1445748450c258a50160c37e112a702 (diff) | |
Dafny: fixed bug in induction-tactic heuristic (should never pick values whose type is a type parameter)
| -rw-r--r-- | 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/Dafny/Translator.cs b/Dafny/Translator.cs index f89ded6a..f224f35e 100644 --- a/Dafny/Translator.cs +++ b/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 -----------------
|