diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b715078c68f791c3201d69242209d2e2503b2eeb..b463a2725dfea5d8873952196c05fab5b13843f2 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -10,7 +10,7 @@ import purescala.Extractors._
 
 case object UnusedInput extends NormalizingRule("UnusedInput") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)
+    val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)
 
     if (!unused.isEmpty) {
       val sub = p.copy(as = p.as.filterNot(unused))