diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index d81b8eea718d40639c0ff5edce6bdc57c0837f83..9130639d52a147389144825125051e604e93e2fb 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -34,8 +34,8 @@ case class NoopPhase[T]() extends LeonPhase[T, T] {
   override def run(ctx: LeonContext)(v: T) = v
 }
 
-case class ExitPhase[T]() extends LeonPhase[T, Unit] {
+case class ExitPhase[T]() extends LeonPhase[T, PipelineControl] {
   val name = "end";
   val description = "end"
-  override def run(ctx: LeonContext)(v: T) = ()
+  override def run(ctx: LeonContext)(v: T) = PipelineControl(restart = false)
 }
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 0f44ffb74e0bebe72f37cd742c032641721c79de..d6727014440d1032e40944c73f2a8944052c6998 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -92,7 +92,7 @@ object Main {
 
   implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
 
-  def computePipeLine(settings: Settings): Pipeline[List[String], Unit] = {
+  def computePipeLine(settings: Settings): Pipeline[List[String], PipelineControl] = {
     import purescala.Definitions.Program
 
     val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
@@ -107,28 +107,22 @@ object Main {
         NoopPhase[Program]()
       }
 
-    val pipeSynthesis: Pipeline[Program, Program] =
+    val pipeAction: Pipeline[Program, PipelineControl]=
       if (settings.synthesis) {
         synthesis.SynthesisPhase
+      } else if (settings.analyze) {
+        AnalysisPhase andThen
+        ExitPhase[Program]()
       } else {
-        NoopPhase[Program]()
-      }
-
-    val pipeAnalysis: Pipeline[Program, Program] =
-      if (settings.analyze) {
-        AnalysisPhase
-      } else {
-        NoopPhase[Program]()
+        ExitPhase[Program]()
       }
 
     pipeBegin followedBy
     pipeTransforms followedBy
-    pipeSynthesis followedBy
-    pipeAnalysis andThen
-    ExitPhase()
+    pipeAction
   }
 
-  def main(args : Array[String]) : Unit = {
+  def main(args : Array[String]) {
     val reporter = new DefaultReporter()
 
     // Process options
@@ -137,7 +131,11 @@ object Main {
     // Compute leon pipeline
     val pipeline = computePipeLine(ctx.settings)
 
-    // Run phases
-    pipeline.run(ctx)(args.toList)
+    var exec = PipelineControl()
+    do {
+      exec = pipeline.run(ctx)(args.toList)
+    } while(exec.restart)
+
+    sys.exit(exec.exitcode)
   }
 }
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 477a08c31250ba1996ddccd59262631fe75499c1..ce2677d41eafe2a5aa397d159e0556a287bf373c 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -24,3 +24,5 @@ class PipeNil[T]() extends Pipeline[T,T] {
     "|"
   }
 }
+
+case class PipelineControl(exitcode: Int = 0, restart: Boolean = false)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f887def32d1bce83dfe59f99cda889eea298ac67..bf7a62e7eac26b26f8f079034b502cb271cffc6b 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,17 +3,35 @@ package synthesis
 
 import purescala.Definitions.Program
 
-object SynthesisPhase extends TransformationPhase {
+object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
   val name        = "Synthesis"
   val description = "Synthesis"
 
-  def apply(ctx: LeonContext, p: Program): Program = {
+  def run(ctx: LeonContext)(p: Program): PipelineControl = {
     val quietReporter = new QuietReporter
     val solvers  = List(
       new TrivialSolver(quietReporter),
       new FairZ3Solver(quietReporter)
     )
 
-    new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+    val newProgram = new Synthesizer(ctx.reporter, solvers).synthesizeAll(p)
+
+    detectEditor match {
+      case Some(program) => 
+        openEditor(program, "/home/ekneuss/plop")
+        PipelineControl(restart = false)
+      case None =>
+        ctx.reporter.fatalError("Cannot open editor, $EDITOR / $VISUAL missing")
+        PipelineControl(restart = false)
+    }
+  }
+
+  def detectEditor: Option[String] = {
+    Option(System.getenv("EDITOR")) orElse Option(System.getenv("VISUAL"))
+  }
+
+  def openEditor(program: String, path: String) {
+    val p = sys.process.Process(program+" "+path)
+    p !<
   }
 }
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 99cc012878aa495e9f41c064e221b5dafa99c71a..729ef93365bd3e8a916b9a2b4ad5f34b2691ec19 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -15,7 +15,8 @@ object SynthesisProceduresToolkit {
 
   def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
 
-  def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3,  x4)) || (a1 == a3 && x1 == x3))
+  def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) =>
+    Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3,  x4)) || (a1 == a3 && x1 == x3))
 
   abstract class Nat
   case class Z() extends Nat