Add Choose ValDef when recursing down choose predicate in ChooseEncoder

jad-hamza · jad-hamza · commit aa397a2734e7 · 2021-04-29T16:00:50.000+02:00
diff --git a/src/main/scala/inox/solvers/unrolling/ChooseEncoder.scala b/src/main/scala/inox/solvers/unrolling/ChooseEncoder.scala
@@ -41,7 +41,7 @@ trait ChooseEncoder extends transformers.ProgramTransformer {
               (substMap + (vd -> nvd.toVariable), vds :+ nvd)
           }
 
-          val newPred = exprOps.replaceFromSymbols(substMap, rec(c.pred, params))
+          val newPred = exprOps.replaceFromSymbols(substMap, rec(c.pred, params :+ c.res))
           val returnType = typeOps.replaceFromSymbols(substMap, c.res.tpe)
 
           val newFd = new FunDef(

Original file line number	Diff line number	Diff line change
`@@ -41,7 +41,7 @@ trait ChooseEncoder extends transformers.ProgramTransformer {`
`41`	`41`	`(substMap + (vd -> nvd.toVariable), vds :+ nvd)`
`42`	`42`	`}`
`43`	`43`
`44`		`- val newPred = exprOps.replaceFromSymbols(substMap, rec(c.pred, params))`
	`44`	`+ val newPred = exprOps.replaceFromSymbols(substMap, rec(c.pred, params :+ c.res))`
`45`	`45`	`val returnType = typeOps.replaceFromSymbols(substMap, c.res.tpe)`
`46`	`46`
`47`	`47`	`val newFd = new FunDef(`