1 files changed, 13 insertions, 0 deletions
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 -----------------