Merge pull request #142 from jad-hamza/let-choose

Add let case in ChooseEncoder

Author: samarion

src/it/scala/inox/tip/TipTestSuite.scala

@@ -39,7 +39,7 @@ class TipTestSuite extends TestSuite with ResourceUtils {
     ctx.options.findOptionOrDefault(optSelectedSolvers).headOption match {
       case Some(solver) => (solver, file.getName) match {
         // Z3 binary will predictably segfault on certain permutations of this problem
-        case ("smt-z3", "MergeSort2.scala-1.tip") => Ignore
+        case ("no-inc:smt-z3" | "smt-z3", "MergeSort2.scala-1.tip") => Ignore
         // use non-linear operators that aren't supported in CVC4
         case ("smt-cvc4", "Instantiation.scala-0.tip") => Skip
         case ("smt-cvc4", "LetsInForall.tip") => Skip

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

@@ -25,9 +25,9 @@ trait ChooseEncoder extends transformers.ProgramTransformer {
 
     val newFds = sourceProgram.symbols.functions.values.toList.map { fd =>
       def rec(e: Expr, params: Seq[ValDef]): Expr = e match {
-        case l: Lambda =>
-          val free = exprOps.variablesOf(l)
-          l.copy(body = rec(l.body, params.filter(vd => free(vd.toVariable)) ++ l.params)).copiedFrom(l)
+        case l: Let => l.copy(body = rec(l.body, params :+ l.vd)).copiedFrom(l)
+
+        case l: Lambda => l.copy(body = rec(l.body, params ++ l.params)).copiedFrom(l)
 
         case c: Choose =>
           val (substMap, freshParams) = params.foldLeft((Map[ValDef, Expr](), Seq[ValDef]())) {
@@ -37,7 +37,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(