Skip to content
Snippets Groups Projects
Commit 22075d6f authored by Ravi's avatar Ravi
Browse files

Fixing a bug in the SMTLIB encoding of ADTs

parent 37bc9723
No related branches found
No related tags found
No related merge requests found
...@@ -70,7 +70,15 @@ class ADTManager(ctx: LeonContext) { ...@@ -70,7 +70,15 @@ class ADTManager(ctx: LeonContext) {
def forEachType(t: TypeTree)(f: TypeTree => Unit): Unit = t match { def forEachType(t: TypeTree)(f: TypeTree => Unit): Unit = t match {
case NAryType(tps, builder) => case NAryType(tps, builder) =>
f(t) 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 { protected def findDependencies(t: TypeTree): Unit = t match {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment