Correctly extract methods from single case-classes

src/main/scala/leon/frontends/scalac/CodeExtraction.scala

@@ -415,32 +415,38 @@ trait CodeExtraction extends ASTExtractors {
 
     private def extractMethodDefs(defs: List[Tree]) = {
       // We collect defined function bodies
-      for (d <- defs) d match {
-        case ExAbstractClass(_, csym, tmpl) =>
-          val cd = classesToClasses(csym)
+      def extractFromClass(csym: Symbol, tmpl: Template) {
+        val cd = classesToClasses(csym)
 
-          val ctparams = csym.tpe match {
-            case TypeRef(_, _, tps) =>
-              extractTypeParams(tps).map(_._1)
-            case _ =>
-              Nil
-          }
+        val ctparams = csym.tpe match {
+          case TypeRef(_, _, tps) =>
+            extractTypeParams(tps).map(_._1)
+          case _ =>
+            Nil
+        }
 
-          val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
+        val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
 
-          for (d <- tmpl.body) d match {
-            case ExFunctionDef(sym, tparams, params, _, body) =>
-              val fd = defsToDefs(sym)
+        for (d <- tmpl.body) d match {
+          case ExFunctionDef(sym, tparams, params, _, body) if !sym.isSynthetic && !sym.isAccessor =>
+            val fd = defsToDefs(sym)
 
-              val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
+            val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
 
-              if(body != EmptyTree) {
-                extractFunBody(fd, params, body)(DefContext(tparamsMap))
-              }
+            if(body != EmptyTree) {
+              extractFunBody(fd, params, body)(DefContext(tparamsMap))
+            }
 
-            case _ =>
+          case _ =>
 
-          }
+        }
+      }
+      for (d <- defs) d match {
+        case ExAbstractClass(_, csym, tmpl) =>
+          extractFromClass(csym, tmpl)
+
+        case ExCaseClass(_, csym, _, tmpl) =>
+          extractFromClass(csym, tmpl)
 
         case _ =>
       }