diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 3d8df24e1c00cd11beda6feec4b80be51229bcf3..d469f0ce18be11333dbadc3b9237d5774e48029a 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -270,10 +270,15 @@ trait ASTExtractors {
 
     object ExObjectDef {
       /** Matches an object with no type parameters, and regardless of its
-       * visibility. Does not match on the automatically generated companion
+       * visibility. Does not match on case objects or the automatically generated companion
        * objects of case classes (or any synthetic class). */
       def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
-        case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic => {
+        case ClassDef(_, name, tparams, impl) if
+          (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) &&
+          tparams.isEmpty &&
+          !cd.symbol.isSynthetic &&
+          !cd.symbol.isCaseClass
+        => {
           Some((name.toString, impl))
         }
         case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9e209b5d54f7ba0c02b8ee6c78b4757a9187b2f0..44125a3700d1cb1632518b274d85c62a33e4e207 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -858,7 +858,10 @@ trait CodeExtraction extends ASTExtractors {
         case ExFieldDef(_,_,_) =>
         case ExLazyFieldDef() => 
         case ExFieldAccessorFunction() => 
-        case d if isIgnored(d.symbol) || (d.symbol.isImplicit && d.symbol.isSynthetic) =>
+        case d if // Various synthetic junk
+          isIgnored(d.symbol) ||
+          (d.symbol.isImplicit && d.symbol.isSynthetic ) ||
+          (d.symbol.isMethod && d.symbol.isSynthetic) =>
         case tree =>
           println(tree)
           outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");