Fixes in trees

src/main/scala/inox/ast/Definitions.scala

@@ -181,15 +181,12 @@ trait Definitions { self: Trees =>
                          val flags: Set[ClassFlag]) extends ClassDef {
     val isAbstract = true
 
-    def descendants(implicit s: Symbols): Seq[ClassDef] = children
+    def descendants(implicit s: Symbols): Seq[CaseClassDef] = children
       .map(id => s.getClass(id) match {
         case ccd: CaseClassDef => ccd
         case _ => throw NotWellFormedException(id, s)
       })
 
-    def ccDescendants(implicit s: Symbols): Seq[CaseClassDef] =
-      descendants collect { case ccd: CaseClassDef => ccd }
-
     def isInductive(implicit s: Symbols): Boolean = {
       def induct(tpe: Type, seen: Set[ClassDef]): Boolean = tpe match {
         case ct: ClassType =>
@@ -206,7 +203,7 @@ trait Definitions { self: Trees =>
       }
 
       if (this == root && !this.isAbstract) false
-      else ccDescendants.exists { ccd =>
+      else descendants.exists { ccd =>
         ccd.fields.exists(vd => induct(vd.getType, Set(root)))
       }
     }
@@ -275,7 +272,6 @@ trait Definitions { self: Trees =>
 
   case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
     def descendants: Seq[TypedClassDef] = cd.descendants.map(_.typed(tps))
-    def ccDescendants: Seq[TypedCaseClassDef] = cd.ccDescendants.map(_.typed(tps))
   }
 
   case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {

src/main/scala/inox/ast/Expressions.scala

@@ -276,7 +276,7 @@ trait Expressions { self: Trees =>
     // Hacky, but ok
     def optionType(implicit s: Symbols) = s.getFunction(id, tps).returnType.asInstanceOf[ClassType]
     def optionChildren(implicit s: Symbols): (ClassType, ClassType) = {
-      val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].ccDescendants.sortBy(_.fields.size)
+      val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].descendants.sortBy(_.fields.size)
       val Seq(noneType, someType) = children.map(_.toType)
       (noneType, someType)
     }

src/main/scala/inox/ast/GenTreeOps.scala

@@ -232,7 +232,7 @@ trait GenTreeOps {
 
     val Deconstructor(es, builder) = e
     val newEss = es.map(rec)
-    val newVs: Seq[SubTree] = leon.utils.SeqUtils.cartesianProduct(newEss).map { newEs =>
+    val newVs: Seq[SubTree] = SeqUtils.cartesianProduct(newEss).map { newEs =>
       if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
         builder(newEs).copiedFrom(e)
       } else {

src/main/scala/inox/ast/SymbolOps.scala

@@ -447,7 +447,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
     }
 
     val tcds = tcd match {
-      case tacd: TypedAbstractClassDef => tacd.ccDescendants
+      case tacd: TypedAbstractClassDef => tacd.descendants
       case tccd: TypedCaseClassDef => Seq(tccd)
     }
 
@@ -476,7 +476,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
 
       val tccd @ TypedCaseClassDef(cd, tps) = tcd match {
         case tacd: TypedAbstractClassDef =>
-          tacd.ccDescendants.filter(hasInstance(_)).sortBy(_.fields.size).head
+          tacd.descendants.filter(hasInstance(_)).sortBy(_.fields.size).head
         case tccd: TypedCaseClassDef => tccd
       }
 
@@ -534,7 +534,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
         case Some(tccd: TypedCaseClassDef) =>
           cartesianProduct(tccd.fieldsTypes map valuesOf) map (CaseClass(ct, _))
         case Some(accd: TypedAbstractClassDef) =>
-          interleave(accd.ccDescendants.map(tccd => valuesOf(tccd.toType)))
+          interleave(accd.descendants.map(tccd => valuesOf(tccd.toType)))
         case None => throw ClassLookupException(ct.id)
       }
     }

src/main/scala/inox/ast/TypeOps.scala

@@ -245,17 +245,17 @@ trait TypeOps {
               Set(tpe) ++ (tpe match {
                 case ct: ClassType => ct.tcd match {
                   case tccd: TypedCaseClassDef => tccd.fieldsTypes
-                  case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.ccDescendants).map(_.toType)
+                  case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.descendants).map(_.toType)
                 }
                 case _ => Set.empty
               })
             )
-          })(accd.ccDescendants.map(_.toType).toSet)
+          })(accd.descendants.map(_.toType).toSet)
 
           if (possibleChildTypes(accd.toType)) {
             None
           } else {
-            cards(accd.ccDescendants.map(_.toType)).map(_.sum)
+            cards(accd.descendants.map(_.toType)).map(_.sum)
           }
       }
       case _ => None

src/main/scala/inox/solvers/SolverUnsupportedError.scala

-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Common.Tree
-
-object SolverUnsupportedError {
-  def msg(t: Tree, s: Solver, reason: Option[String]) = {
-    s"(of ${t.getClass}) is unsupported by solver ${s.name}" + reason.map(":\n  " + _ ).getOrElse("")
-  }
-}
-
-case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
-  extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.context)