diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index bfc097c3721832acc6d5dfca5e998cf5938323c9..d8910012fe052f24fc63715642d3334f24d85fb9 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -445,12 +445,13 @@ trait ASTExtractors {
           case ValDef(mods, name, tpt, rhs) if (
             !sym.isCaseAccessor && !sym.isParamAccessor && 
             !sym.isLazy && !sym.isSynthetic && !sym.isAccessor 
-          ) =>        
+          ) =>
             // Since scalac uses the accessor symbol all over the place, we pass that instead:
             Some( (sym.getterIn(sym.owner),tpt.tpe,rhs) )
           // Unimplemented fields
-          case DefDef(_, name, _, _, tpt, _) if (
-            sym.isStable && sym.isAccessor && sym.name != nme.CONSTRUCTOR
+          case df@DefDef(_, name, _, _, tpt, _) if (
+            sym.isStable && sym.isAccessor && sym.name != nme.CONSTRUCTOR &&
+            sym.accessed == NoSymbol // This is to exclude fields with implementation
           ) =>
             Some( (sym, tpt.tpe, EmptyTree))
           case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 87418d2dd670e3ea30d24fcb058500fee53a78a2..62627f8c801346c490dd7a4ff4d4d7dcf5e4b628 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -290,11 +290,16 @@ trait CodeExtraction extends ASTExtractors {
             case ExFieldDef(sym, _, _) =>
               Some(defineFieldFunDef(sym, false)(DefContext()))
 
-            case ExCaseClassSyntheticJunk() => None
-            case ExConstructorDef() => None
-            case ExLazyFieldDef() => None
-            case ExFieldAccessorFunction() => None
-            case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+            // All these are expected, but useless
+            case ExCaseClassSyntheticJunk()
+               | ExConstructorDef()
+               | ExLazyFieldDef()
+               | ExFieldAccessorFunction() =>
+              None
+            case d if (d.symbol.isImplicit && d.symbol.isSynthetic) =>
+              None
+
+            // Everything else is unexpected
             case tree =>
               println(tree)
               outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
@@ -302,9 +307,11 @@ trait CodeExtraction extends ASTExtractors {
 
           Some(LeonModuleDef(id, leonDefs, id.name == "package"))
 
-        case ExCaseClassSyntheticJunk() => None
-        case ExConstructorDef() => None
+        // Expected, but useless
+        case ExCaseClassSyntheticJunk() | ExConstructorDef() => None
         case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+
+        // Unexpected
         case tree =>
           println(tree)
           outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");