Moved termination regression back to fairz3

src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala

@@ -160,7 +160,7 @@ trait AbstractZ3Solver extends Solver {
     val defs = for ((_, DataType(sym, cases)) <- adts) yield {(
       sym.uniqueName,
       cases.map(c => c.sym.uniqueName),
-      cases.map(c => c.fields.map{ case(id, tpe) => (id.uniqueName, typeToSortRef(tpe))})
+      cases.map(c => c.fields.map { case(id, tpe) => (id.uniqueName, typeToSortRef(tpe))})
     )}
 
     val resultingZ3Info = z3.mkADTSorts(defs)

src/main/scala/leon/termination/StructuralSize.scala

@@ -205,20 +205,21 @@ trait StructuralSize {
         case ct: ClassType =>
           val root = ct.root
           val fd = outerCache.getOrElse(root.classDef.typed, {
-            val id = FreshIdentifier("x", root.classDef.typed, true)
+            val tcd = root.classDef.typed
+            val id = FreshIdentifier("x", tcd, true)
             val fd = new FunDef(FreshIdentifier("outerSize", alwaysShowUniqueID = true),
               root.classDef.tparams,
               Seq(ValDef(id)),
               IntegerType)
-            outerCache(root.classDef.typed) = fd
+            outerCache(tcd) = fd
 
-            fd.body = Some(MatchExpr(Variable(id), root.knownCCDescendants map { cct =>
+            fd.body = Some(MatchExpr(Variable(id), tcd.knownCCDescendants map { cct =>
               val args = cct.fields.map(_.id.freshen)
               purescala.Extractors.SimpleCase(
                 CaseClassPattern(None, cct, args.map(id => WildcardPattern(Some(id)))),
                 args.foldLeft[Expr](InfiniteIntegerLiteral(1)) { case (e, id) =>
                   plus(e, id.getType match {
-                    case ct: ClassType if dependencies(root)(ct.root) => outerSize(Variable(id))
+                    case ct: ClassType if dependencies(tcd)(ct.root) => outerSize(Variable(id))
                     case _ => InfiniteIntegerLiteral(0)
                   })
                 })
@@ -229,7 +230,7 @@ trait StructuralSize {
             fd
           })
 
-          FunctionInvocation(fd.typed(ct.tps), Seq(e))
+          FunctionInvocation(fd.typed(root.tps), Seq(e))
 
         case _ => InfiniteIntegerLiteral(0)
       })

src/test/scala/leon/regression/termination/TerminationSuite.scala

@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
 
   private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
     for(f <- files) {
-      mkTest(f, Seq("--solvers=smt-z3"), forError)(block)
+      mkTest(f, Seq(), forError)(block)
     }
   }