diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c80d777480f66d795f2bc15eef0a3010452394fb..c0fd0d23603d0d55ad7f2ca0c12c80ee03a721ba 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1290,12 +1290,6 @@ object ExprOps {
     }
   }
 
-  class ChooseCollectorWithPaths extends CollectorWithPaths[(Choose,Expr)] {
-    def collect(e: Expr, path: Seq[Expr]) = e match {
-      case c: Choose => Some(c -> and(path: _*))
-      case _ => None
-    }
-  }
 
   def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
     CollectorWithPaths(f).traverse(expr)
@@ -1319,11 +1313,6 @@ object ExprOps {
       es.map(formulaSize).sum+1
   }
 
-  /** Return a list of all [[purescala.Expressions.Choose Choose]] construct inside the expression */
-  def collectChooses(e: Expr): List[Choose] = {
-    new ChooseCollectorWithPaths().traverse(e).map(_._1).toList
-  }
-
   /** Returns true if the expression is deterministic / does not contain any [[purescala.Expressions.Choose Choose]] or [[purescala.Expressions.Hole Hole]]*/
   def isDeterministic(e: Expr): Boolean = {
     preTraversal{
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index fc8a9bbd8efce032576c897a4812f5a266173f5e..4bb10d38c9ffc7a7667d165b84e4f65c1edc9e0c 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -19,6 +19,14 @@ case class SourceInfo(fd: FunDef,
 }
 
 object SourceInfo {
+
+  class ChooseCollectorWithPaths extends CollectorWithPaths[(Choose,Expr)] {
+    def collect(e: Expr, path: Seq[Expr]) = e match {
+      case c: Choose => Some(c -> and(path: _*))
+      case _ => None
+    }
+  }
+
   def extractFromProgram(ctx: LeonContext, prog: Program): List[SourceInfo] = {
     val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
 
@@ -49,7 +57,7 @@ object SourceInfo {
     // We are synthesizing, so all examples are valid ones
     val functionEb = eFinder.extractFromFunDef(fd, partition = false)
 
-    for ((ch, path) <- new ChooseCollectorWithPaths().traverse(fd.fullBody)) yield {
+    for ((ch, path) <- new ChooseCollectorWithPaths().traverse(fd)) yield {
       val outerEb = if (path == BooleanLiteral(true)) {
         functionEb
       } else {