diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 29cc186e20d958825dbb76ab7a3808519530ff33..7aa76a9713f7e75ad747eb7e4ba8c88173e63861 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -4,6 +4,7 @@ import purescala.Definitions.Program
 
 case class LeonContext(
   val settings: Settings          = Settings(),
+  val options: List[LeonOption]   = Nil,
   val files: List[String]         = Nil,
   val reporter: Reporter          = new DefaultReporter
 )
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index f2579e5aff59113c1a1ae0d3484278532bc9fd18..0340e7461bad98a088da143df8b7b485d743425f 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -10,4 +10,16 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
   def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
 }
 
-case class LeonOptionDef(name: String, isFlag: Boolean, description: String)
+sealed abstract class LeonOptionDef {
+  val name: String
+  val usageOption: String
+  val usageDesc: String
+  val isFlag: Boolean
+}
+case class LeonFlagOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
+  val isFlag = true
+}
+
+case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
+  val isFlag = false
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b815f5cb9558d70a3d9942e74d7c592eec4dfc47..ace9c2d29bdff42abcd2c4b88b3e52611580740d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -18,11 +18,11 @@ object Main {
   }
 
   lazy val allOptions = allPhases.flatMap(_.definedOptions) ++ Set(
-      LeonOptionDef("synthesis",     true,  "--synthesis          Partial synthesis or choose() constructs"),
-      LeonOptionDef("xlang",         true,  "--xlang              Support for extra program constructs (imperative,...)"),
-      LeonOptionDef("parse",         true,  "--parse              Checks only whether the program is valid PureScala"),
-      LeonOptionDef("debug",         false, "--debug=[1-5]        Debug level"),
-      LeonOptionDef("help",          true,  "--help               This help")
+      LeonFlagOptionDef ("synthesis", "--synthesis",   "Partial synthesis or choose() constructs"),
+      LeonFlagOptionDef ("xlang",     "--xlang",       "Support for extra program constructs (imperative,...)"),
+      LeonFlagOptionDef ("parse",     "--parse",       "Checks only whether the program is valid PureScala"),
+      LeonValueOptionDef("debug",     "--debug=[1-5]", "Debug level"),
+      LeonFlagOptionDef ("help",      "--help",        "This help")
     )
 
   def displayHelp(reporter: Reporter) {
@@ -30,7 +30,7 @@ object Main {
     reporter.info("")
     reporter.info("Leon options are:")
     for (opt <- allOptions.toSeq.sortBy(_.name)) {
-      reporter.info("   "+opt.description)
+      reporter.info("   %-20s %s".format(opt.usageOption, opt.usageDesc))
     }
     sys.exit(1)
   }
@@ -89,7 +89,7 @@ object Main {
       case _ =>
     }
 
-    LeonContext(settings = settings, reporter = reporter, files = files)
+    LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
   }
 
   implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 2967ea34a1032afeb5d553caa3ac2e1d2bc60ddf..269f612b8f53ec60820c05c0b417fb4f4fb7de35 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -421,9 +421,7 @@ object ScalaPrinter {
 
     case e @ Error(desc) => {
       var nsb = sb
-      nsb.append("error(\"" + desc + "\")[")
-      nsb = pp(e.getType, nsb, lvl)
-      nsb.append("]")
+      nsb.append("error(\"" + desc + "\")")
       nsb
     }
 
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ac10811eb7cb361fa07a71b8fb460659cc06a312..898891307057e3a5f4e45b929ab7e36da5c5fdd5 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -7,6 +7,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   val name        = "Synthesis"
   val description = "Synthesis"
 
+  override def definedOptions = Set(
+    LeonFlagOptionDef("inplace", "--inplace", "Debug level")
+  )
+
   def run(ctx: LeonContext)(p: Program): Program = {
     val quietReporter = new QuietReporter
     val solvers  = List(
@@ -14,11 +18,20 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       new FairZ3Solver(quietReporter)
     )
 
+    var inPlace = false
+    for(opt <- ctx.options) opt match {
+      case LeonFlagOption("inplace") =>
+        inPlace = true
+      case _ =>
+    }
+
     val synth = new Synthesizer(ctx.reporter, solvers)
     val solutions = synth.synthesizeAll(p)
 
-    for (file <- ctx.files) {
-      synth.updateFile(new java.io.File(file), solutions)
+    if (inPlace) {
+      for (file <- ctx.files) {
+        synth.updateFile(new java.io.File(file), solutions)
+      }
     }
 
     p