diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 11d035724b13e6ecd44fde2e7de40830dbcf3a2c..04892e750e63afc33b5a7a3ba193f1b93797cae6 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -11,11 +11,16 @@ abstract class CostModel(val name: String) {
def solutionCost(s: Solution): Cost
def problemCost(p: Problem): Cost
- def ruleAppCost(r: Rule, app: RuleInstantiation): Cost = new Cost {
+ def ruleAppCost(app: RuleInstantiation): Cost = new Cost {
val subSols = (1 to app.onSuccess.arity).map {i => Solution.simplest }.toList
val simpleSol = app.onSuccess(subSols)
- val value = simpleSol.map(solutionCost(_).value).getOrElse(0)
+ val value = simpleSol match {
+ case Some(sol) =>
+ solutionCost(sol).value
+ case None =>
+ problemCost(app.problem).value
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index cc313e629b377c5489b8b3ff6532d9afee9d0e1e..a80831ec49fd854c3a362eb45f2a11c93a53f4b6 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -37,14 +37,14 @@ object HeuristicInstantiation {
Some(s)
}
- def apply(problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
+ def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {
val builder = new SolutionBuilder(subProblems.size) {
def apply(sols: List[Solution]) = {
Some(onSuccess(sols))
}
}
- new RuleInstantiation(builder) {
+ new RuleInstantiation(problem, rule, builder) {
def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
}
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index f859172129b11be170df760a019f2ff27a91dfee..5ec24b47e4857a6eb953065ca331236cba90744a 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -70,7 +70,7 @@ class ParallelSearch(synth: Synthesizer,
def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
val sub = rules.flatMap { r =>
- r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _))
+ r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
}
if (!sub.isEmpty) {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 3d24a3c2d11e782c7531e623892eac901bed93bd..0ea37eac2f87b3812af71110f2e4da6561d29313 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -44,7 +44,7 @@ object SolutionBuilder {
}
}
-abstract class RuleInstantiation(val onSuccess: SolutionBuilder) {
+abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuccess: SolutionBuilder) {
def apply(sctx: SynthesisContext): RuleApplicationResult
}
@@ -62,14 +62,14 @@ case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
case object RuleApplicationImpossible extends RuleApplicationResult
object RuleInstantiation {
- def immediateDecomp(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleInstantiation(new SolutionCombiner(sub.size, onSuccess)) {
+ def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Solution) = {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, onSuccess)) {
def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
- def immediateSuccess(solution: Solution) = {
- new RuleInstantiation(new SolutionCombiner(0, ls => solution)) {
+ def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(0, ls => solution)) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
}
}
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index d2b658bb2ea4abddfdf2f9d9d8f501ffc8a5f45e..393177e775ef9aa98699f8987fd7373880b44708 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -3,7 +3,11 @@ package synthesis
import synthesis.search._
-case class TaskRunRule(problem: Problem, rule: Rule, app: RuleInstantiation) extends AOAndTask[Solution] {
+case class TaskRunRule(app: RuleInstantiation) extends AOAndTask[Solution] {
+
+ val problem = app.problem
+ val rule = app.rule
+
def composeSolution(sols: List[Solution]): Option[Solution] = {
app.onSuccess(sols)
}
@@ -18,7 +22,7 @@ case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskTryRules, Solution] {
def taskCost(t: AOTask[Solution]) = t match {
case ttr: TaskRunRule =>
- cm.ruleAppCost(ttr.rule, ttr.app)
+ cm.ruleAppCost(ttr.app)
case trr: TaskTryRules =>
cm.problemCost(trr.p)
}
@@ -59,7 +63,7 @@ class SimpleSearch(synth: Synthesizer,
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
- val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(t.p, r, _)) )
+ val sub = rules.flatMap ( r => r.instantiateOn(sctx, t.p).map(TaskRunRule(_)) )
if (!sub.isEmpty) {
Expanded(sub.toList)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index adcbb72a2625d67c79f6adeaa1c6923065737f6e..4cb8f22859770c07f7f80db7bda0e0187ca8514a 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -97,7 +97,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet+newFun, FunctionInvocation(newFun, Variable(origId) :: oas.map(Variable(_))))
}
- Some(HeuristicInstantiation(p, subProblemsInfo.map(_._1).toList, onSuccess))
+ Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index fdcc626c4d258c6e4bb0fb787ac97be52ae5526e..a882fe32b8ac04601a7301bcecfc8ce4fc98c045 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -54,7 +54,7 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
Solution.none
}
- Some(HeuristicInstantiation(p, List(subBase, subGT, subLT), onSuccess))
+ Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index a3ecedd7217d7757e7f324bddaf698c97282fc18..1a957e40250d7cab755d4657463d0a9f04aad9ed 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -36,7 +36,7 @@ case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 8e91394f0fc87b33d9ae9bc7aaa2f5724ee809ba..488df73556f61321eaf64ca21923b505087978b1 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -36,7 +36,7 @@ case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 6b6dac90ffe89417e08eb77abd295d0cf3da4ca9..f1811f073e66e3fc69a7546d9d52be91428dea08 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -24,7 +24,7 @@ case object ADTDual extends Rule("ADTDual") {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index e94abd7f1e93160517b56ba45ec6f23980ff8c5c..4680ca40b79d15d668c78be680933a6d386f825e 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -70,7 +70,7 @@ case object ADTSplit extends Rule("ADT Split.") {
Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases))
}
- Some(RuleInstantiation.immediateDecomp(subInfo.map(_._2).toList, onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess))
case _ =>
None
}}.flatten
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 4522067b810caaa610c4339c2fee3a0e0fab143d..d45d0890321140329fbe0ff4f66e6ff3415ef6ff 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -16,11 +16,11 @@ case object Assert extends Rule("Assert") {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- List(RuleInstantiation.immediateSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
+ List(RuleInstantiation.immediateSuccess(p, this, Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id)))))))
} else {
val sub = p.copy(pc = And(p.pc +: exprsA), phi = And(others))
- List(RuleInstantiation.immediateDecomp(List(sub), {
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), {
case Solution(pre, defs, term) :: Nil => Solution(And(exprsA :+ pre), defs, term)
case _ => Solution.none
}))
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 3850b1d745a3d70bf5e0abdf4c410599df539085..9b3e563152bae312029099fc2d8c15872dc06d3d 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -34,7 +34,7 @@ case object CaseSplit extends Rule("Case-Split") {
Solution.none
}
- RuleInstantiation.immediateDecomp(subs, onSuccess)
+ RuleInstantiation.immediateDecomp(p, this, subs, onSuccess)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 8eafd160fd7b7f473435b6bef9c9316817ab80de..c7f84e483fd78b92415e319d3def1c20faee633a 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -124,7 +124,7 @@ case object CEGIS extends Rule("CEGIS") {
val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
if (exprsA.isEmpty) {
- val res = new RuleInstantiation(SolutionBuilder.none) {
+ val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
def apply(sctx: SynthesisContext) = {
var result: Option[RuleApplicationResult] = None
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 9ca48a9f62eb4c9e9aab867555f3ba039bbf939c..4925f60004acf4e1f604fc47cbfee5a72a3083dc 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -26,7 +26,7 @@ object Disunification {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index bad8bc4c45a0430595499156eeb2a61c80615d6d..603a48a08dc32975a0df514677fe4bee9259a85a 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -48,7 +48,7 @@ case object EqualitySplit extends Rule("Eq. Split.") {
Solution.none
}
- Some(RuleInstantiation.immediateDecomp(List(sub1, sub2), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess))
case _ =>
None
}).flatten
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 6aefe88a8ca64b76fda97f012a3a7c322f6d8507..953ad5b56f6d0a7dfa7b5551be27fb4d8554079a 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -16,10 +16,10 @@ case object Ground extends Rule("Ground") {
sctx.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
- Some(RuleInstantiation.immediateSuccess(sol))
+ Some(RuleInstantiation.immediateSuccess(p, this, sol))
case (Some(false), model) =>
val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
- Some(RuleInstantiation.immediateSuccess(sol))
+ Some(RuleInstantiation.immediateSuccess(p, this, sol))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index eabbfce2e984e913c92dc01b4169a29ed574be78..f74e4478ed7b90c5f658691c5de46dd3e0943b34 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -60,7 +60,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -103,7 +103,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 21f9dced181fb1d55161fb6db1600da6230fc8d8..7fbc67fd601cae132c90a03e9d67ed35a896883f 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -131,7 +131,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val constraints: List[Expr] = for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))
val pre = And(exprNotUsed ++ constraints)
- List(RuleInstantiation.immediateSuccess(Solution(pre, Set(), witness)))
+ List(RuleInstantiation.immediateSuccess(problem, this, Solution(pre, Set(), witness)))
} else {
val involvedVariables = (upperBounds++lowerBounds).foldLeft(Set[Identifier]())((acc, t) => {
@@ -200,7 +200,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(subProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(subProblem), onSuccess))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 24eee3336a644b4298ac0fc6107448761db5b537..7f4fae9da93c2b25459542f890a54c21bf8582d9 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -35,7 +35,7 @@ case object OnePoint extends Rule("One-point") {
case _ => Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(newProblem), onSuccess))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 460a83fe4f9771fb4a4982df4956d5db2ef6889e..953afc7b275df4a4aa5cb3f10f106bf8abd34591 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -38,7 +38,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
case (Some(false), _) =>
- result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
case _ =>
continue = false
@@ -47,7 +47,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
case (Some(false), _) =>
if (predicates.isEmpty) {
- result = Some(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ result = Some(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
continue = false
result = None
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 7c8d2de15faa8ab3ff577dfc56a4c528f5ec654c..381f73f6b7600c9954d45bbc9725e7d610729b44 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -20,7 +20,7 @@ case object UnconstrainedOutput extends Rule("Unconstr.Output") {
Solution.none
}
- List(RuleInstantiation.immediateDecomp(List(sub), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 5c81516197a52b250611c9aad044c39eb1f49898..9b7ea42304e2f6271a888984c5cdb6375a7ab8b3 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -27,7 +27,7 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}
@@ -52,7 +52,7 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- List(RuleInstantiation.immediateSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ List(RuleInstantiation.immediateSuccess(p, this, Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 13ba585abf24ec06d6d07b43405f55435571f48d..b44ad3411529237a12f1dc3acc53db19a5dd3954 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -13,7 +13,7 @@ case object UnusedInput extends Rule("UnusedInput") {
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- List(RuleInstantiation.immediateDecomp(List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
Nil
}