diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index d714bbf81a80c153631946c0bf9758fa4dae8093..2e96db012e589f4d1fda94a8a067deeeef58040a 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -19,7 +19,7 @@ abstract class CostModel(val name: String) {
 }
 
 case class Cost(minSize: Int) extends Ordered[Cost] {
-  def isImpossible = minSize >= 100
+  def isImpossible = minSize >= 200
   
   def compare(that: Cost): Int = {
     this.minSize-that.minSize
@@ -83,7 +83,7 @@ class SizeBasedCostModel(name: String) extends CostModel(name) {
     }   
   }
 
-  def impossible = Cost(100)
+  def impossible = Cost(200)
 }
 
 case object NaiveCostModel extends SizeBasedCostModel("Naive")
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 95877335937746e7c365aa48f11ff1ccc75618c4..b5a701579a407b3d7f5f361f9d46581c0a454395 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -42,10 +42,9 @@ object Rules {
 
     for ((_, rs) <- rulesPrio) {
       val results = rs.flatMap{ r =>
-        val ts = System.currentTimeMillis
-        val res = r.instantiateOn(sctx, problem)
-        println("Instantiating "+r+" ("+(System.currentTimeMillis-ts)+")")
-        res
+        sctx.context.timers.synthesis.instantiations.get(r.toString).timed {
+          r.instantiateOn(sctx, problem)
+        }
       }.toList
 
       if (results.nonEmpty) {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0e2bff86f85aa2d69274233d79973c51b888f436..42656a83a9b2e6f4f883075a0105c672bb27377f 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -39,9 +39,10 @@ class Synthesizer(val context : LeonContext,
   def synthesize(): (Search, Stream[Solution]) = {
     val s = getSearch();
 
+    val sctx = SynthesisContext.fromSynthesizer(this)
+
     val t = context.timers.synthesis.search.start()
 
-    val sctx = SynthesisContext.fromSynthesizer(this)
     val sols = s.search(sctx)
 
     val diff = t.stop()
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 02346a51e358d668a0d15a2a8478feff8c8b3b59..4877c475c5715582ac70051f51191017abc3af91 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -17,8 +17,18 @@ abstract class Search(ctx: LeonContext, p: Problem, costModel: CostModel) extend
 
   val interrupted = new AtomicBoolean(false);
 
-  def doStep(n: Node, sctx: SynthesisContext) = {
-    n.expand(sctx)
+  def doStep(n: Node, sctx: SynthesisContext): Unit = {
+    ctx.timers.synthesis.step.timed {
+      n match {
+        case an: AndNode =>
+          ctx.timers.synthesis.applications.get(an.ri.toString).timed {
+            an.expand(sctx)
+          }
+
+        case on: OrNode =>
+          on.expand(sctx)
+      }
+    }
   }
 
   @tailrec
@@ -95,18 +105,20 @@ class SimpleSearch(ctx: LeonContext, p: Problem, costModel: CostModel, bound: Op
   var counter = 0;
   def findNodeToExpandFrom(from: Node): Option[Node] = {
     counter += 1
-    if (!bound.isDefined || counter <= bound.get) {
-      if (expansionBuffer.isEmpty) {
-        findIn(from)
-      }
+    ctx.timers.synthesis.search.find.timed {
+      if (!bound.isDefined || counter <= bound.get) {
+        if (expansionBuffer.isEmpty) {
+          findIn(from)
+        }
 
-      if (expansionBuffer.nonEmpty) {
-        Some(expansionBuffer.remove(0))
+        if (expansionBuffer.nonEmpty) {
+          Some(expansionBuffer.remove(0))
+        } else {
+          None
+        }
       } else {
         None
       }
-    } else {
-      None
     }
   }
 }
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 8a47d7774d92bae45c7f13a44827e9b5c7b8e7d4..632a6202ae73dee47216af45cdb7a9de66772b34 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -13,7 +13,7 @@ import purescala.Definitions._
 import solvers._
 
 case object ADTSplit extends Rule("ADT Split.") {
-  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 200L))
 
     val candidates = p.as.collect {
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 7ced27bff9fbcbfce0c6af67e4b8e916ebe1c69d..c74c52839159394ebe6cadbe5ff893a2089d1e1d 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -77,7 +77,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
     val useBssFiltering       = sctx.options.cegisUseBssFiltering
     val filterThreshold       = 1.0/2
     val evalParams            = CodeGenParams(maxFunctionInvocations = 2000)
-    val evaluator             = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
+    lazy val evaluator        = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
 
     val interruptManager      = sctx.context.interruptManager
 
@@ -149,7 +149,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
       private var triedCompilation = false
       private var progEvaluator: Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = None
 
-      def canTest() = {
+      def canTest(): Boolean = {
         if (!triedCompilation) {
           progEvaluator = compile()
         }
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index c896759f4433ef6f2a8589521b7a5470d8400894..b2c8b38222836b8c05c4d3e88d4956c3f539fc1c 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -85,6 +85,13 @@ class TimerStorage extends Dynamic {
     this
   }
 
+  def timed[T](b: => T): T = {
+    start
+    val res = b
+    stop
+    res
+  }
+
   def stop() = {
     selfTimer.get.stop
   }