diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index ec3c9738a9cacab212d8cab6054bcad88c84afe5..2d6ec3191621cf54fe251effe8ac1033b6703ff1 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -20,7 +20,7 @@ trait ASTExtractors {
     rootMirror.getClassByName(newTermName(str))
   }
 
-  def annotationsOf(s: Symbol): Set[String] = {
+  def annotationsOf(s: Symbol): Map[String, Seq[Option[Any]]] = {
     val actualSymbol = s.accessedOrSelf
 
     (for {
@@ -28,8 +28,12 @@ trait ASTExtractors {
       name = a.atp.safeToString.replaceAll("\\.package\\.", ".")
       if (name startsWith "leon.annotation.")
     } yield {
-      name.split("\\.", 3)(2)
-    }).toSet
+      val args = a.args.map {
+        case Literal(x) => Some(x.value)
+        case _ => None
+      }
+      (name.split("\\.", 3)(2), args)
+    }).toMap
   }
 
   protected lazy val tuple2Sym          = classFromName("scala.Tuple2")
@@ -406,7 +410,7 @@ trait ASTExtractors {
         case DefDef(_, name, tparams, vparamss, tpt, rhs) if name != nme.CONSTRUCTOR && !dd.symbol.isAccessor =>
           if (dd.symbol.isSynthetic && dd.symbol.isImplicit && dd.symbol.isMethod) {
             // Check that the class it was generated from is not ignored
-            if (annotationsOf(tpt.symbol)("ignore")) {
+            if (annotationsOf(tpt.symbol).isDefinedAt("ignore")) {
               None
             } else {
               Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index a95b760ca1384d3815fd567b999ed1750ffdd4fc..cda2d5fae7b872fa91011de9a4efe70694a68449 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -632,7 +632,7 @@ trait CodeExtraction extends ASTExtractors {
 
       fd.setPos(sym.pos)
 
-      fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
+      fd.addFlags(annotationsOf(sym).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
 
       if (sym.isImplicit) {
         fd.addFlag(IsInlined)
@@ -667,7 +667,7 @@ trait CodeExtraction extends ASTExtractors {
       fd.setPos(sym.pos)
       fd.addFlag(IsField(isLazy))
 
-      fd.addFlags(annotationsOf(sym).map(FunctionFlag.fromName))
+      fd.addFlags(annotationsOf(sym).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
 
       defsToDefs += sym -> fd
 
@@ -1082,7 +1082,7 @@ trait CodeExtraction extends ASTExtractors {
 
           val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
 
-          fd.addFlags(annotationsOf(d.symbol).map(FunctionFlag.fromName))
+          fd.addFlags(annotationsOf(d.symbol).map { case (name, args) => FunctionFlag.fromName(name, args) }.toSet)
 
           val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
 
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index b5cffb4d752dcb9cd21b00fe96ca66e6139df286..fde6f3de7679891ce596a1447736695a30614310 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -305,16 +305,16 @@ object Definitions {
   sealed abstract class FunctionFlag
 
   object FunctionFlag {
-    def fromName(name: String): FunctionFlag = name match {
+    def fromName(name: String, args: Seq[Option[Any]]): FunctionFlag = name match {
       case "inline" => IsInlined
-      case _ => Annotation(name)
+      case _ => Annotation(name, args)
     }
   }
 
   // Whether this FunDef was originally a (lazy) field
   case class IsField(isLazy: Boolean) extends FunctionFlag
   // Compiler annotations given in the source code as @annot
-  case class Annotation(annot: String) extends FunctionFlag
+  case class Annotation(annot: String, args: Seq[Option[Any]]) extends FunctionFlag
   // If this class was a method. owner is the original owner of the method
   case class IsMethod(owner: ClassDef) extends FunctionFlag
   // If this function represents a loop that was there before XLangElimination
@@ -401,7 +401,8 @@ object Definitions {
 
     def flags = flags_
 
-    def annotations: Set[String] = flags_ collect { case Annotation(s) => s }
+    def annotations: Set[String] = extAnnotations.keySet
+    def extAnnotations: Map[String, Seq[Option[Any]]] = flags_.collect { case Annotation(s, args) => s -> args }.toMap
     def canBeLazyField    = flags.contains(IsField(true))  && params.isEmpty && tparams.isEmpty
     def canBeStrictField  = flags.contains(IsField(false)) && params.isEmpty && tparams.isEmpty
     def canBeField        = canBeLazyField || canBeStrictField