From 52242199eec3707be89cfcf02042bd58715dc390 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 4 Nov 2016 13:08:05 +0100
Subject: [PATCH] Small fix in determining lambda normal form during template
generation
---
.../inox/solvers/unrolling/TemplateGenerator.scala | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index 37e41c6aa..2ad8b4f2b 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)] = {
--
GitLab