Add let case in ChooseEncoder

Author: jad-hamza

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

@@ -25,6 +25,10 @@ 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: Let =>
+          val free = exprOps.variablesOf(l)
+          l.copy(body = rec(l.body, params.filter(vd => free(vd.toVariable)) :+ l.vd)).copiedFrom(l)
+
         case l: Lambda =>
           val free = exprOps.variablesOf(l)
           l.copy(body = rec(l.body, params.filter(vd => free(vd.toVariable)) ++ l.params)).copiedFrom(l)

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

@@ -164,8 +164,15 @@ trait AbstractUnrollingSolver extends Solver { self =>
 
   def assertCnstr(expression: Expr): Unit = context.timers.solvers.assert.run(try {
     context.timers.solvers.assert.sanity.run {
-      symbols.ensureWellFormed // make sure that the current program is well-formed
-      typeCheck(expression, BooleanType()) // make sure we've asserted a boolean-typed expression
+      try {
+        symbols.ensureWellFormed // make sure that the current program is well-formed
+        typeCheck(expression, BooleanType()) // make sure we've asserted a boolean-typed expression
+      } catch {
+        case _: Throwable =>
+          context.reporter.internalError(
+            "Error while ensuring well-formedness of symbols and expression in `assertCnstr` in `UnrollingSolver`"
+          )
+      }
     }
 
     // Multiple calls to registerForInterrupts are (almost) idempotent and acceptable