diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala index 7aefd95773e05f0a22f9bb435f2b2771a2c93da0..a08fbc1ae9f5bd4eb67cb06be2007f2ec848f73a 100644 --- a/src/main/scala/leon/solvers/ADTManager.scala +++ b/src/main/scala/leon/solvers/ADTManager.scala @@ -70,7 +70,15 @@ class ADTManager(ctx: LeonContext) { def forEachType(t: TypeTree)(f: TypeTree => Unit): Unit = t match { case NAryType(tps, builder) => f(t) - tps.foreach(forEachType(_)(f)) + // note: each of the tps could be abstract classes in which case we need to + // lock their dependencies, transitively. + tps.foreach { + case ct: ClassType => + val (root, sub) = getHierarchy(ct) + (root +: sub).flatMap(_.fields.map(_.getType)).foreach(subt => forEachType(subt)(f)) + case othert => + forEachType(othert)(f) + } } protected def findDependencies(t: TypeTree): Unit = t match {