diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index d6fbc999a8ad910cd77f445722c28c8699fcd066..2d2ea4143433a0d99b311dfff41e17dfb8a95294 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -52,7 +52,7 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
       ,
         if (Settings.synthesis)
           List(
-            new SynthesisPhase(leonReporter)
+            SynthesisPhase
           )
         else
           Nil
@@ -71,7 +71,8 @@ class AnalysisComponent(val global: Global, val leonReporter: Reporter, val plug
       //global ref to freshName creator
       fresh = unit.fresh
 
-      var ac = LeonContext(program = extractCode(unit))
+      var ac = LeonContext(program = extractCode(unit),
+                           reporter = leonReporter)
 
       if(Settings.stopAfterExtraction) {
         leonReporter.info("Extracted program for " + unit + ": ")
diff --git a/src/main/scala/leon/plugin/LeonContext.scala b/src/main/scala/leon/plugin/LeonContext.scala
index 29274a5fdd6d602007ce2be7956b79566f37dd2c..0c6ebabdd2d4eafc77607a8591e3852149038353 100644
--- a/src/main/scala/leon/plugin/LeonContext.scala
+++ b/src/main/scala/leon/plugin/LeonContext.scala
@@ -4,6 +4,7 @@ package plugin
 import purescala.Definitions.Program
 
 case class LeonContext(
-  val program: Program
+  val program: Program,
+  val reporter: Reporter
 )
 
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 84a63890547fc80478b3187d9fa2f8423a5dae3d..5666d15c896210d24a2c48ca64082e96fec5b318 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,19 +1,22 @@
 package leon
 package synthesis
 
+import plugin.LeonContext
 import purescala.Definitions.Program
 
-class SynthesisPhase(reporter: Reporter) extends plugin.TransformationPhase {
+object SynthesisPhase extends plugin.LeonPhase {
   val name        = "Synthesis"
   val description = "Synthesis"
 
-  def apply(program: Program): Program = {
+  def run(ctx: LeonContext): LeonContext = {
     val quietReporter = new QuietReporter
     val solvers  = List(
       new TrivialSolver(quietReporter),
       new FairZ3Solver(quietReporter)
     )
 
-    new Synthesizer(reporter, solvers).synthesizeAll(program)
+    val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(ctx.program)
+
+    ctx.copy(program = newProgram)
   }
 }