Support for LetTuple in Fairz3

src/main/scala/leon/solvers/z3/FunctionTemplate.scala

@@ -201,6 +201,23 @@ object FunctionTemplate {
           val rb = rec(pathVar, replace(Map(Variable(i) -> Variable(newExpr)), b))
           rb
 
+        case l @ LetTuple(is, e, b) =>
+          val tuple : Identifier = FreshIdentifier("t", true).setType(TupleType(is.map(_.getType)))
+          exprVars += tuple
+          val re = rec(pathVar, e)
+          storeGuarded(pathVar, Equals(Variable(tuple), re))
+
+          val mapping = for ((id, i) <- is.zipWithIndex) yield {
+            val newId = FreshIdentifier("ti", true).setType(id.getType)
+            exprVars += newId
+            storeGuarded(pathVar, Equals(Variable(newId), TupleSelect(Variable(tuple), i+1)))
+
+            (Variable(id) -> Variable(newId))
+          }
+
+          val rb = rec(pathVar, replace(mapping.toMap, b))
+          rb
+
         case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
 
         case i @ Implies(lhs, rhs) =>