diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7f9a8b0547d1b0f3a62769bd3ffbb73d236f2451..baf62236d14a2289cc4393500ecffdb77f0895df 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -58,10 +58,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       case _ =>
     }
 
-    def synthesizeAll(program: Program): Map[Choose, Solution] = {
+    def synthesizeAll(program: Program): Map[Choose, (FunDef, Solution)] = {
       def noop(u:Expr, u2: Expr) = u
 
-      var solutions = Map[Choose, Solution]()
+      var solutions = Map[Choose, (FunDef, Solution)]()
 
       def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
         case ch @ Choose(vars, pred) =>
@@ -78,7 +78,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
                                       timeoutMs)
           val sol = synth.synthesize()
 
-          solutions += ch -> sol
+          solutions += ch -> (f, sol)
 
           a
         case _ =>
@@ -110,16 +110,16 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
     def simplify(e: Expr): Expr = simplifiers.foldLeft(e){ (x, sim) => sim(x) }
 
     val chooseToExprs = solutions.map {
-      case (ch, sol) => (ch, simplify(sol.toExpr))
+      case (ch, (fd, sol)) => (ch, (fd, simplify(sol.toExpr)))
     }
 
     if (inPlace) {
       for (file <- ctx.files) {
-        new FileInterface(ctx.reporter, file).updateFile(chooseToExprs)
+        new FileInterface(ctx.reporter, file).updateFile(chooseToExprs.mapValues(_._2))
       }
     } else {
-      for ((chs, ex) <- chooseToExprs) {
-        ctx.reporter.info("-"*32+" Synthesis of: "+"-"*32)
+      for ((chs, (fd, ex)) <- chooseToExprs) {
+        ctx.reporter.info("-"*32+" In "+fd.id.toString+", synthesis of: "+"-"*32)
         ctx.reporter.info(chs)
         ctx.reporter.info("-"*35+" Result: "+"-"*35)
         ctx.reporter.info(ScalaPrinter(ex))
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 97fc75e77ffbd1f82231908ad537cd8b0c0baf26..78ca68e29103e5b327316a4cf1dd0aaa39391f50 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -61,7 +61,7 @@ class Synthesizer(val context : LeonContext,
     reporter.info("Finished in "+diff+"ms")
 
     if (generateDerivationTrees) {
-      new AndOrGraphDotConverter(search.g, firstOnly).writeFile("derivation.dot")
+      new AndOrGraphDotConverter(search.g, firstOnly).writeFile("derivation"+AndOrGraphDotConverterCounter.next()+".dot")
     }
 
     res match {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 03bb85e401eaad2b8cf0b2fa8fa7c805c5ad8f32..931e276bde7482b3ff25110d2a1ed8804f1c2cac 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -1,6 +1,5 @@
 package leon.synthesis.search
 
-
 class AndOrGraphDotConverter[AT <: AOAndTask[S],
                              OT <: AOOrTask[S],
                              S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
@@ -116,3 +115,13 @@ class AndOrGraphDotConverter[AT <: AOAndTask[S],
     out.close()
   }
 }
+
+object AndOrGraphDotConverterCounter {
+  private var nextId = 0;
+  def next() = {
+    nextId += 1
+    nextId
+  }
+}
+
+