diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala index 37e41c6aaacf40e3823d4ee7b6661db7435d4503..2ad8b4f2b3ce8696880728b36bcd2b877e83684e 100644 --- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala +++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala @@ -287,14 +287,16 @@ trait TemplateGenerator { self: Templates => case _ => (Seq.empty, e) } - !l.getType.isInstanceOf[FunctionType] && (extractBody(struct) match { - case (params, ApplicationExtractor(caller: Variable, args)) => - (params.map(_.toVariable) == args) && (deps.get(caller) match { + extractBody(struct) match { + case (params, app @ ApplicationExtractor(caller: Variable, args)) => + !app.getType.isInstanceOf[FunctionType] && + (params.map(_.toVariable) == args) && + (deps.get(caller) match { case Some(_: Application | _: FunctionInvocation | _: Variable) => true case _ => false }) case _ => false - }) + } } val depsByScope: Seq[(Variable, Expr)] = {