From 4e61f65e88fa5fac53597d8091295416aec70d47 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 21 Jan 2015 17:07:39 +0100
Subject: [PATCH] Look in ws as well
---
src/main/scala/leon/synthesis/rules/UnusedInput.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b715078c6..b463a2725 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))
--
GitLab