diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 00c8af3a299a2d8fe4c199a26f2f2f1bca7b393a..e835637a49d32d5c2035e3925186134c15c4673f 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -10,6 +10,7 @@ object Rules {
     new OnePoint(synth),
     new Ground(synth),
     new CaseSplit(synth),
+    new UnusedInput(synth),
     new Assert(synth)
   )
 }
@@ -144,3 +145,22 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
     }
   }
 }
+
+class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
+  def isApplicable(p: Problem, parent: Task): List[Task] = {
+    val unused = p.as.toSet -- variablesOf(p.phi)
+
+    if (!unused.isEmpty) {
+        val sub = p.copy(as = p.as.filterNot(unused))
+
+        val onSuccess: List[Solution] => Solution = { 
+          case List(s) => s
+          case _ => Solution.none
+        }
+
+        List(new Task(synth, parent, this, p, List(sub), onSuccess, 300))
+    } else {
+      Nil
+    }
+  }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 12da7a5e30369eff6454d1a9209509b6d08c758a..ca8507b856cca38467c131907e2c8a708bc905c0 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -12,7 +12,7 @@ import collection.mutable.PriorityQueue
 class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   import r.{error,warning,info,fatalError}
 
-  private[this] var solution: Solution = null
+  private[this] var solution: Option[Solution] = None
 
   def synthesize(p: Problem, rules: List[Rule]): Solution = {
 
@@ -26,7 +26,9 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
 
     workList += rootTask
 
-    while (!workList.isEmpty) {
+    solution = None
+
+    while (!workList.isEmpty && solution.isEmpty) {
       val task = workList.dequeue()
 
       task.subProblems match {
@@ -59,7 +61,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
 
     }
 
-    solution
+    solution.getOrElse(Solution.none)
   }
 
   def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
@@ -79,7 +81,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
     task match {
       case rt: RootTask =>
         info(" SUCCESS!")
-        this.solution = solution
+        this.solution = Some(solution)
       case t: Task =>
         info(" => Solved "+task.problem+" ⊢  "+solution)
         t.parent.subSucceeded(t.problem, solution)