diff --git a/src/main/scala/leon/Annotations.scala b/src/main/scala/leon/Annotations.scala
index 0831c8ff81ae212d6e0fd10d5a847c77c88186f4..85e8c00e0379c42f000b61ac14861190bb46963a 100644
--- a/src/main/scala/leon/Annotations.scala
+++ b/src/main/scala/leon/Annotations.scala
@@ -3,4 +3,5 @@ package leon
 object Annotations {
   class induct extends StaticAnnotation
   class axiomatize extends StaticAnnotation
+  class main extends StaticAnnotation
 }
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 5a27d30b7292db35109c5d2aa29d8dfda197072f..5aeb487141d3ccb2f40ff084a1fcf7d65049f723 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -19,6 +19,8 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
   def analyse(program: Program) {
     z3Solver.setProgram(program)
     reporter.info("Running test generation")
+    program.definedFunctions.foreach(fd => println(fd.annotations))
+
     val testcases = generateTestCases(program)
 
     val topFunDef = program.definedFunctions.find(fd => fd.body.exists(body => body match {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index b89dc39dbf82d5f7443194c6beb79cb551acc0cf..57aa0af64197fd6dc9917fe190fef73adf6bfa96 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -203,6 +203,7 @@ trait CodeExtraction extends Extractors {
               a.atp.safeToString match {
                 case "leon.Annotations.induct" => funDef.addAnnotation("induct")
                 case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+                case "leon.Annotations.main" => funDef.addAnnotation("main")
                 case _ => ;
               }
             }