Skip to content

Commit 5ff600a

Browse files
committed
Remove filtering in ChooseEncoder
1 parent aa397a2 commit 5ff600a

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

src/main/scala/inox/solvers/unrolling/ChooseEncoder.scala

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -25,13 +25,9 @@ trait ChooseEncoder extends transformers.ProgramTransformer {
2525

2626
val newFds = sourceProgram.symbols.functions.values.toList.map { fd =>
2727
def rec(e: Expr, params: Seq[ValDef]): Expr = e match {
28-
case l: Let =>
29-
val free = exprOps.variablesOf(l)
30-
l.copy(body = rec(l.body, params.filter(vd => free(vd.toVariable)) :+ l.vd)).copiedFrom(l)
28+
case l: Let => l.copy(body = rec(l.body, params :+ l.vd)).copiedFrom(l)
3129

32-
case l: Lambda =>
33-
val free = exprOps.variablesOf(l)
34-
l.copy(body = rec(l.body, params.filter(vd => free(vd.toVariable)) ++ l.params)).copiedFrom(l)
30+
case l: Lambda => l.copy(body = rec(l.body, params ++ l.params)).copiedFrom(l)
3531

3632
case c: Choose =>
3733
val (substMap, freshParams) = params.foldLeft((Map[ValDef, Expr](), Seq[ValDef]())) {

0 commit comments

Comments
 (0)