diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index f81e5f44d593afbd97068db3aac4a0f72a8d3ca4..2a20a478b4688dc93b8058db0df3178282d2a7b2 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -415,13 +415,15 @@ object DefOps {
     
     def duplicateClassDef(cd: ClassDef): ClassDef = {
       cdMapCache.get(cd) match {
-        case Some(new_cd) => new_cd.get // None would have meant that this class would never be duplicated, which is not possible.
+        case Some(new_cd) => 
+          new_cd.get // None would have meant that this class would never be duplicated, which is not possible.
         case None =>
           val parent = cd.parent.map(duplicateAbstractClassType)
           val new_cd = cdMapF(cd).map(f => f(parent)).getOrElse{
             cd match {
               case acd:AbstractClassDef => acd.duplicate(parent = parent)
-              case ccd:CaseClassDef => ccd.duplicate(parent = parent, fields = ccd.fieldsIds.map(id => ValDef(idMap(id)))) // Should not cycle since fields have to be abstract.
+              case ccd:CaseClassDef => 
+                ccd.duplicate(parent = parent, fields = ccd.fieldsIds.map(id => ValDef(idMap(id)))) // Should not cycle since fields have to be abstract.
             }
           }
           cdMapCache += cd -> Some(new_cd)
@@ -440,10 +442,11 @@ object DefOps {
     // If at least one descendants or known case class needs conversion, then all the hierarchy will be converted.
     // If something extends List[A] and A is modified, then the first something should be modified.
     def dependencies(s: ClassDef): Set[ClassDef] = {
-      Set(s) ++ s.parent.toList.flatMap(p => TypeOps.collect[ClassDef]{
-        case AbstractClassType(acd, _) => Set(acd:ClassDef) ++ acd.knownCCDescendants
+      leon.utils.fixpoint((s: Set[ClassDef]) => s ++ s.flatMap(_.knownDescendants) ++ s.flatMap(_.parent.toList.flatMap(p => TypeOps.collect[ClassDef]{
+        case AbstractClassType(acd, _) => Set(acd:ClassDef) ++ acd.knownDescendants
         case CaseClassType(ccd, _) => Set(ccd:ClassDef)
-      }(p))
+        case _ => Set()
+      }(p))))(Set(s))
     }
     
     def cdMap(cd: ClassDef): ClassDef = {
@@ -461,7 +464,8 @@ object DefOps {
     }
     def idMap(id: Identifier): Identifier = {
       if (!(idMapCache contains id)) {
-        idMapCache += id -> id.duplicate(tpe = tpMap(id.getType))
+        val new_id = id.duplicate(tpe = tpMap(id.getType))
+        idMapCache += id -> new_id
       }
       idMapCache(id)
     }
@@ -474,6 +478,7 @@ object DefOps {
       TypeOps.exists{
         case AbstractClassType(acd, _) => cdMap(acd) != acd
         case CaseClassType(ccd, _) => cdMap(ccd) != ccd
+        case _ => false
       }(tp)
     }
     
@@ -588,7 +593,8 @@ object DefOps {
         case ci @ CaseClass(ct, args) =>
           ciMapF(ci, tpMap(ct)).map(_.setPos(ci))
         case CaseClassSelector(cct, expr, identifier) =>
-          Some(CaseClassSelector(tpMap(cct), expr, idMap(identifier)))
+          val new_cct = tpMap(cct)
+          Some(CaseClassSelector(new_cct, expr, (if(new_cct != cct) idMap(identifier) else identifier)))
         case IsInstanceOf(e, ct) => Some(IsInstanceOf(e, tpMap(ct)))
         case AsInstanceOf(e, ct) => Some(AsInstanceOf(e, tpMap(ct)))
         case MatchExpr(scrut, cases) =>