diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index cc2d8938e5c1629e9ce27af4bd62d86e5cb2695a..a085755c1dbf8bd3ff649d365fa78b0ae9b410c7 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -511,12 +511,14 @@ trait CodeExtraction extends ASTExtractors {
 
         classesToClasses += sym -> acd
         parent.foreach(_.classDef.registerChild(acd))
+        acd.setAnnotations(annotationsOf(sym))
 
         acd
       } else {
         val ccd = CaseClassDef(id, tparams, parent, sym.isModuleClass).setPos(sym.pos)
         classesToClasses += sym -> ccd
         parent.foreach(_.classDef.registerChild(ccd))
+        ccd.setAnnotations(annotationsOf(sym))
 
         val fields = args.map { case (fsym, t) =>
           val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index cd1948c26598ae9afd5f60e93efa0a2a423b5a40..60d5da277ad76aa49792973fd0665d68e4a3d11a 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -224,6 +224,14 @@ object Definitions {
 
     def methods = _methods
 
+    private var _annotations: Map[String, Seq[Option[Any]]] = Map.empty
+
+    def setAnnotations(annotations: Map[String, Seq[Option[Any]]]) {
+      _annotations = annotations
+    }
+
+    def annotations = _annotations
+
     lazy val ancestors: Seq[ClassDef] = parent.toSeq flatMap { p => p.classDef +: p.classDef.ancestors }
 
     lazy val root = ancestors.lastOption.getOrElse(this)