diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 8715767c94ae37f1c639bc06b2a479ae0b5f1600..546e5726382d814ba533dc3de87241c7517e0f99 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -268,10 +268,20 @@ object TypeOps extends GenTreeOps[TypeTree] {
         Math.pow(t + 1, f).toInt
       }
     case cct: CaseClassType =>
-      Some(cct.fields.map { field =>
-        typeCardinality(field.getType).getOrElse(return None)
+      Some(cct.fieldsTypes.map { tpe =>
+        typeCardinality(tpe).getOrElse(return None)
       }.product)
     case act: AbstractClassType =>
+      val possibleChildTypes = leon.utils.fixpoint((tpes: Set[TypeTree]) => {
+        tpes.flatMap(tpe => 
+          Set(tpe) ++ (tpe match {
+            case cct: CaseClassType => cct.fieldsTypes
+            case act: AbstractClassType => Set(act) ++ act.knownCCDescendants
+            case _ => Set.empty
+          })
+        )
+      })(act.knownCCDescendants.toSet)
+      if(possibleChildTypes(act)) return None
       Some(act.knownCCDescendants.map(typeCardinality).map(_.getOrElse(return None)).sum)
     case _ => None
   }