diff --git a/build.sbt b/build.sbt
index 75b810dd1e71a27069d7198d63fdc0a52f1866f7..14d73203e7920e3f21f24292a3bc076882a52b3d 100644
--- a/build.sbt
+++ b/build.sbt
@@ -39,6 +39,7 @@ javaOptions in Test ++= Seq("-Xss32M", "-Xmx4G", "-XX:MaxPermSize=128M")
 
 parallelExecution in Test := false
 
-testOptions in Test := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument("-oDF"))
+testOptions in (Test, run) := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument("-oDF"))
+testOptions in (Test, testOnly) := Seq(Tests.Argument("-oDF"))
 
 sourcesInBase in Compile := false
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index 658a4b532a7ca8c0f2b8368f6876e23f08e2f9fb..f2fb6f47b92b47c1536091fee455b09cc62ccb12 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -4,6 +4,7 @@ package leon
 package synthesis
 package utils
 
+import purescala.DefOps.funDefsFromMain
 import purescala.Definitions._
 
 object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[FunDef, Seq[ChooseInfo]])] {
@@ -12,7 +13,7 @@ object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[
 
   def run(ctx: LeonContext)(p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
     // Look for choose()
-    val results = for (f <- p.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) yield {
+    val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id.toString) if f.body.isDefined) yield {
       f -> ChooseInfo.extractFromFunction(p, f)
     }
 
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 6978a3fa8132194d7071118bccbc4d8cdd8a3b73..a5cf9ef81abc19a7f31b5f3b0987181c92eda553 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -118,68 +118,6 @@ class SynthesisSuite extends LeonTestSuite {
       }
   }
 
-//  def synthesizeWith(search: SearchContext, p: Problem, ss: Apply): Solution = {
-//    val apps = hctx.sctx.rules flatMap { _.instantiateOn(hctx, p)}
-//
-//    def matchingDesc(app: RuleInstantiation, ss: Apply): Boolean = {
-//      import java.util.regex.Pattern;
-//      val pattern = Pattern.quote(ss.desc).replace("*", "\\E.*\\Q")
-//      app.toString.matches(pattern)
-//    }
-//
-//    apps.filter(matchingDesc(_, ss)) match {
-//      case app :: Nil =>
-//        app.apply(hctx) match {
-//          case RuleClosed(sols) =>
-//            assert(sols.nonEmpty)
-//            assert(ss.andThen.isEmpty)
-//            sols.head
-//
-//          case RuleExpanded(sub) =>
-//            val subSols = (sub zip ss.andThen) map { case (p, ss) => synthesizeWith(hctx, p, ss) }
-//            app.onSuccess(subSols).get
-//        }
-//
-//      case Nil =>
-//        throw new AssertionError("Failed to find "+ss.desc+". Available: "+apps.mkString(", "))
-//
-//      case xs =>
-//        throw new AssertionError("Ambiguous "+ss.desc+". Found: "+xs.mkString(", "))
-//    }
-//  }
-//
-//  def synthesize(title: String)(program: String)(strategies: PartialFunction[String, Apply]) {
-//    forProgram(title)(program) {
-//      case (hctx, fd, p) =>
-//        strategies.lift.apply(fd.id.toString) match {
-//          case Some(ss) =>
-//            synthesizeWith(hctx, p, ss)
-//
-//          case None =>
-//            assert(false, "Function "+fd.id.toString+" not found")
-//        }
-//    }
-//  }
-//
-//
-//  def assertAllAlternativesSucceed(hctx: SearchContext, rr: Traversable[RuleInstantiation]) {
-//    assert(!rr.isEmpty)
-//
-//    for (r <- rr) {
-//      assertRuleSuccess(hctx, r)
-//    }
-//  }
-//
-//  def assertRuleSuccess(hctx: SearchContext, rr: RuleInstantiation): Option[Solution] = {
-//    rr.apply(hctx) match {
-//      case RuleClosed(sols) if sols.nonEmpty =>
-//        sols.headOption
-//      case _ =>
-//        assert(false, "Rule did not succeed")
-//        None
-//    }
-//  }
-
   forProgram("Ground Enum", SynthesisSettings(selectedSolvers = Set("enum")))(
     """
 import leon.annotation._