diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index e9317e344ef060dc093f6f5d05cb61e976c4cae3..cd67adf98d97e0addc052f62e603792fddb10ee7 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -20,9 +20,19 @@ case class ChooseInfo(fd: FunDef,
 
 object ChooseInfo {
   def extractFromProgram(ctx: LeonContext, prog: Program): List[ChooseInfo] = {
+    val functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet }
+
+    def excludeByDefault(fd: FunDef): Boolean = {
+      fd.annotations contains "library"
+    }
+
+    val fdFilter = {
+      import OptionsHelpers._
+      filterInclusive(functions.map(fdMatcher(prog)), Some(excludeByDefault _))
+    }
 
     // Look for choose()
-    val results = for (f <- prog.definedFunctions if f.body.isDefined;
+    val results = for (f <- prog.definedFunctions if f.body.isDefined && fdFilter(f);
                        ci <- extractFromFunction(ctx, prog, f)) yield {
       ci
     }
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ff822ac420879bf2808084d0672691d40f38608f..067a79456b0c32a2927ef8ca2816f4fd69b4461f 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -65,14 +65,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   def run(ctx: LeonContext)(program: Program): Program = {
     val options = processOptions(ctx)
 
-    def excludeByDefault(fd: FunDef): Boolean = { fd.annotations contains "library" }
 
-    val fdFilter = {
-      import OptionsHelpers._
-      filterInclusive(options.functions.map(fdMatcher(program)), Some(excludeByDefault _))
-    }
-
-    val chooses = program.definedFunctions.filter(fdFilter).flatMap(ChooseInfo.extractFromFunction(ctx, program, _))
+    val chooses = ChooseInfo.extractFromProgram(ctx, program)
 
     var functions = Set[FunDef]()
 
diff --git a/src/regression/scala/leon/regression/synthesis/SynthesisSuite.scala b/src/regression/scala/leon/regression/synthesis/SynthesisSuite.scala
index d0c7ecc93e15dc86980485cb433f7f4da34be5a4..b071343259c9e74bc7de0ca6332b30c4c5898bd1 100644
--- a/src/regression/scala/leon/regression/synthesis/SynthesisSuite.scala
+++ b/src/regression/scala/leon/regression/synthesis/SynthesisSuite.scala
@@ -86,7 +86,10 @@ class SynthesisSuite extends regression.LeonTestSuite {
       test(f"Synthesizing ${nextInt()}%3d: [$title]") {
         val ctx = testContext.copy(options = opts ++ testContext.options)
 
-        val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase
+        val pipeline = leon.utils.TemporaryInputPhase andThen
+                       leon.frontends.scalac.ExtractionPhase andThen
+                       PreprocessingPhase andThen
+                       SynthesisProblemExtractionPhase
 
         val (program, results) = pipeline.run(ctx)((List(content), Nil))