diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 9346b5530552316073b2b17688c537d04873d986..fd210b24b6bec83bedfac95921cf3b125d2b3dbd 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -85,6 +85,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       case _ =>
     }
 
+    if (options.manualSearch) {
+      options = options.copy(rules = rules.AsChoose +: options.rules)
+    }
+
     options
   }
 
diff --git a/src/main/scala/leon/synthesis/rules/AsChoose.scala b/src/main/scala/leon/synthesis/rules/AsChoose.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e7b1986bd01efdc421b4c623f6727f608e92abb6
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/AsChoose.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+case object AsChoose extends Rule("As Choose") {
+  def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+      Some(new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
+        def apply(sctx: SynthesisContext) = {
+          RuleSuccess(Solution.choose(p))
+        }
+      })
+  }
+}
+