diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 38f1fce44dd79089166c566a11b17e706b0f3215..7d0d94458291b71381d8719a25e13751ca3cdd9f 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -98,11 +98,6 @@ object ArrayTransformation extends Pass {
       IfExpr(rc, rt, re).setType(rt.getType)
     }
 
-    case c @ Choose(args, body) =>
-      val body2 = transform(body)
-
-      Choose(args, body2).setType(c.getType).setPosInfo(c)
-
     case m @ MatchExpr(scrut, cses) => {
       val scrutRec = transform(scrut)
       val csesRec = cses.map{
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index 127e862cfaa6a18faa9ca6a73b93eacb2fb4cac2..d3cd29907c5cd8c30fb574d06ddd1682e5bfa59a 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -257,9 +257,9 @@ object ImperativeCodeElimination extends Pass {
         val (argVal, argScope, argFun) = toFunction(a)
         (recons(argVal).setType(u.getType), argScope, argFun)
       }
-
       case (t: Terminal) => (t, (body: Expr) => body, Map())
 
+
       case _ => sys.error("not supported: " + expr)
     }
     //val codeRepresentation = res._2(Block(res._3.map{ case (id1, id2) => Assignment(id1, id2.toVariable)}.toSeq, res._1))
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 584caaa6fcc7a074982bedd80e91d41901f6af12..9af1b41e731e32ff4b25942c4ec4f6ac63f91b0a 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -4,9 +4,6 @@ import scala.tools.nsc.{Global,Settings=>NSCSettings,SubComponent,CompilerComman
 
 import purescala.Definitions.Program
 
-import synthesis.Synthesizer
-import purescala.ScalaPrinter
-
 object Main {
   import leon.{Reporter,DefaultReporter,Analysis}
 
@@ -35,10 +32,11 @@ object Main {
 
   private def defaultAction(program: Program, reporter: Reporter) : Unit = {
     Logger.debug("Default action on program: " + program, 3, "main")
-    //val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
-    //val program2 = passManager.run(program)
-    assert(program.isPure)
-    val program2 = new Synthesizer().synthesizeAll(program)
+    val passManager = new PassManager(Seq(ArrayTransformation, EpsilonElimination, ImperativeCodeElimination, /*UnitElimination,*/ FunctionClosure, /*FunctionHoisting,*/ Simplificator))
+    val program2 = passManager.run(program)
+    assert(program2.isPure)
+    val analysis = new Analysis(program2, reporter)
+    analysis.analyse
   }
 
   private def runWithSettings(args : Array[String], settings : NSCSettings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 3258b1062a193136efb4e35e4c3b0927910e6e35..a0783f8c3a1f4860bd1acb5b9f2e7f8af05bffd4 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -60,7 +60,7 @@ class Synthesizer(rules: List[Rule]) {
     solution
   }
 
-  def test1 = {
+  def test() {
     import purescala.Common._
     import purescala.Trees._
     import purescala.TypeTrees._
@@ -73,7 +73,6 @@ class Synthesizer(rules: List[Rule]) {
   }
 
   def synthesizeAll(p: Program): Program = {
-    test1
     p
   }
 }