diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index f11526f3c2c7c1af909909cce4120c9621c9962c..184714e7b2b90fd9e220c75324fbc96479590175 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -14,8 +14,7 @@ class ParallelSearch(synth: Synthesizer,
 
   def initWorkerContext(wr: ActorRef) = {
     val reporter = new SilentReporter
-    // TODO FIXME : the proper LeonContext should make its way here.
-    val solver = new FairZ3Solver(LeonContext(reporter = reporter))
+    val solver = new FairZ3Solver(synth.context)
     solver.setProgram(synth.program)
 
     SynthesisContext(solver = solver, reporter = synth.reporter)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 2901bb3827846116cc7f2021974b7c6c6823e141..7f9a8b0547d1b0f3a62769bd3ffbb73d236f2451 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -66,7 +66,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
         case ch @ Choose(vars, pred) =>
           val problem = Problem.fromChoose(ch)
-          val synth = new Synthesizer(ctx.reporter,
+          val synth = new Synthesizer(ctx,
                                       mainSolver,
                                       p,
                                       problem,
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 51444a16b17b42e70acf0b48a23fcb204261a082..b669335b96b9427e65413df5e4bab79d9940f61a 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -15,7 +15,7 @@ import collection.mutable.PriorityQueue
 
 import synthesis.search._
 
-class Synthesizer(val reporter: Reporter,
+class Synthesizer(val context : LeonContext,
                   val solver: Solver,
                   val program: Program,
                   val problem: Problem,
@@ -25,6 +25,8 @@ class Synthesizer(val reporter: Reporter,
                   parallel: Boolean                = false,
                   firstOnly: Boolean               = false,
                   timeoutMs: Option[Long]          = None) {
+  protected[synthesis] val reporter = context.reporter
+
   import reporter.{error,warning,info,fatalError}
 
   var continue = true