Fixed dependency finder

src/main/scala/leon/purescala/DependencyFinder.scala

@@ -20,7 +20,6 @@ class DependencyFinder {
 
   private class Finder(var current: Definition) extends TreeTraverser {
     val foundDeps: MutableMap[Definition, MutableSet[Definition]] = MutableMap.empty
-    foundDeps(current) = MutableSet.empty
 
     private def withCurrent[T](d: Definition)(b: => T): T = {
       if (!(foundDeps contains d)) foundDeps(d) = MutableSet.empty
@@ -35,31 +34,35 @@ class DependencyFinder {
 
     override def traverse(cd: ClassDef): Unit = if (!foundDeps(current)(cd)) {
       foundDeps(current) += cd
-      if (!(deps contains cd) && !(foundDeps contains cd)) {
-        for (cd <- cd.root.knownDescendants :+ cd) {
-          cd.invariant foreach (fd => withCurrent(cd)(traverse(fd)))
-          withCurrent(cd)(cd.fieldsIds foreach traverse)
-          cd.parent foreach { p =>
-            foundDeps(p.classDef) = foundDeps.getOrElse(p.classDef, MutableSet.empty) + cd
-            foundDeps(cd) = foundDeps.getOrElse(cd, MutableSet.empty) + p.classDef
-          }
+      if (!(deps contains cd) && !(foundDeps contains cd)) traverseClassDef(cd)
+    }
+
+    private def traverseClassDef(cd: ClassDef): Unit = {
+      for (cd <- cd.root.knownDescendants :+ cd) {
+        cd.invariant foreach (fd => withCurrent(cd)(traverse(fd)))
+        withCurrent(cd)(cd.fieldsIds foreach traverse)
+        cd.parent foreach { p =>
+          foundDeps(p.classDef) = foundDeps.getOrElse(p.classDef, MutableSet.empty) + cd
+          foundDeps(cd) = foundDeps.getOrElse(cd, MutableSet.empty) + p.classDef
         }
       }
     }
 
     override def traverse(fd: FunDef): Unit = if (!foundDeps(current)(fd)) {
       foundDeps(current) += fd
-      if (!(deps contains fd) && !(foundDeps contains fd)) withCurrent(fd) {
-        fd.params foreach (vd => traverse(vd.id))
-        traverse(fd.returnType)
-        traverse(fd.fullBody)
-      }
+      if (!(deps contains fd) && !(foundDeps contains fd)) traverseFunDef(fd)
+    }
+
+    private def traverseFunDef(fd: FunDef): Unit = withCurrent(fd) {
+      fd.params foreach (vd => traverse(vd.id))
+      traverse(fd.returnType)
+      traverse(fd.fullBody)
     }
 
     def dependencies: Set[Definition] = {
       current match {
-        case fd: FunDef => traverse(fd)
-        case cd: ClassDef => traverse(cd)
+        case fd: FunDef => traverseFunDef(fd)
+        case cd: ClassDef => traverseClassDef(cd)
         case _ =>
       }
 
@@ -69,8 +72,9 @@ class DependencyFinder {
 
       var changed = false
       do {
+        changed = false
         for ((d, ds) <- deps.toSeq) {
-          val next = ds.flatMap(d => deps.getOrElse(d, Set.empty))
+          val next = ds ++ ds.flatMap(d => deps.getOrElse(d, Set.empty))
           if (!(next subsetOf ds)) {
             deps(d) = next
             changed = true