From 22075d6fb494946e435eebad697d289e70a575a5 Mon Sep 17 00:00:00 2001
From: Ravi <ravi.kandhadai@epfl.ch>
Date: Sun, 1 May 2016 11:57:49 +0200
Subject: [PATCH] Fixing a bug in the SMTLIB encoding of ADTs
---
src/main/scala/leon/solvers/ADTManager.scala | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index 7aefd9577..a08fbc1ae 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 {
--
GitLab