diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index f62a7bdcd315aca1d370d92d233678ac0a2a68be..943a5a67f094aea19f1c3903da6b0a32b19e10ec 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -30,7 +30,7 @@ case object Focus extends PreprocessingRule("Focus") {
         
     }
 
-    val fd      = hctx.ci.fd
+    val fd      = hctx.functionContext
     val program = hctx.program
 
     val evaluator = new DefaultEvaluator(hctx, program)
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index 225495cac44b4fdbd4e3e356ef2320ece1619ba9..564c630fcb199b776805f17fd6f80c5e8752e3d7 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -24,11 +24,11 @@ class Search(val ctx: LeonContext, ci: SourceInfo, p: Problem, val strat: Strate
       n match {
         case an: AndNode =>
           ctx.timers.synthesis.applications.get(an.ri.asString(sctx)).timed {
-            an.expand(new SearchContext(sctx, ci, an, this))
+            an.expand(new SearchContext(sctx, ci.source, an, this))
           }
 
         case on: OrNode =>
-          on.expand(new SearchContext(sctx, ci, on, this))
+          on.expand(new SearchContext(sctx, ci.source, on, this))
       }
     }
   }
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 201dcaf21d148652cc73dbcf1cbb7aedb1707dfd..63683d9278e0219eaeb32c5755e0c8ed25f79836 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -4,6 +4,7 @@ package leon
 package synthesis
 
 import graph._
+import purescala.Expressions.Expr
 
 /**
  * This is context passed down rules, and include search-wise context, as well
@@ -11,7 +12,7 @@ import graph._
  */
 class SearchContext (
   sctx: SynthesisContext,
-  val ci: SourceInfo,
+  val source: Expr,
   val currentNode: Node,
   val search: Search
 ) extends SynthesisContext(
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 913e54a49d942ec6312b2af0b56507316b35ae9b..32bf63486906173e5da2c8b5b67cc69f5742ce09 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -284,7 +284,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
             .getOrElse(hctx.reporter.fatalError("Unable to get outer solution"))
         }
 
-        val program0 = addFunDefs(hctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
+        val program0 = addFunDefs(hctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.functionContext)
 
         cTreeFd.body = None
 
@@ -295,11 +295,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
         )
 
         replaceFunDefs(program0){
-          case fd if fd == hctx.ci.fd =>
+          case fd if fd == hctx.functionContext =>
             val nfd = fd.duplicate()
 
             nfd.fullBody = postMap {
-              case src if src eq hctx.ci.source =>
+              case src if src eq hctx.source =>
                 Some(outerSolution.term)
 
               case _ => None
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
index fb3f1ecaeb07a4371503e6fcd744598bf3205190..c0c724c81580221a099e246332c7d3182b19d3f4 100644
--- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
@@ -86,7 +86,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
     val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender)))
     val orNode = search.g.root
     if (!orNode.isExpanded) {
-      val hctx = new SearchContext(synth.sctx, synth.ci, orNode, search)
+      val hctx = new SearchContext(synth.sctx, synth.ci.source, orNode, search)
       orNode.expand(hctx)
     }
     val andNodes = orNode.descendants.collect {
@@ -104,7 +104,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
     
     val solutions = (search.traversePath(path) match {
       case Some(an: AndNode) =>
-        val hctx = new SearchContext(synth.sctx, synth.ci, an, search)
+        val hctx = new SearchContext(synth.sctx, synth.ci.source, an, search)
         an.ri.apply(hctx)
       case _ => throw new Exception("Was not an and node")
     }) match {
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index c2f818a78bd4f673b939ef48349d9a54eda8118b..cedfa529f3770581eb2541a13c37df18e8c371ba 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -104,7 +104,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
             val sctx = synthesizer.sctx
             try {
               val search = synthesizer.getSearch
-              val hctx = new SearchContext(sctx, ci, search.g.root, search)
+              val hctx = new SearchContext(sctx, ci.source, search.g.root, search)
               val problem = ci.problem
               info(j.info("synthesis "+problem.asString(sctx)))
               val apps = decompRules flatMap { _.instantiateOn(hctx, problem)}