diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2ac6b102e03b7b7d1284fd38356f394df579f358..d31c7a3929c82072e410cbdb766fdf493aee1654 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -449,9 +449,11 @@ object TreeOps {
    * Note that the code is simple but far from optimal (many traversals...)
    */
   def simplifyLets(expr: Expr) : Expr = {
+
     def simplerLet(t: Expr) : Option[Expr] = t match {
 
-      case letExpr @ Let(i, t: Terminal, b) if !containsChoose(b) => Some(replace(Map((Variable(i) -> t)), b))
+      case letExpr @ Let(i, t: Terminal, b) if !containsChoose(b) =>
+        Some(replace(Map((Variable(i) -> t)), b))
 
       case letExpr @ Let(i,e,b) if !containsChoose(b) => {
         val occurences = treeCatamorphism[Int]((e:Expr) => e match {
@@ -468,7 +470,6 @@ object TreeOps {
       }
 
       case letTuple @ LetTuple(ids, Tuple(exprs), body) if !containsChoose(body) =>
-
         var newBody = body
 
         val (remIds, remExprs) = (ids zip exprs).filter { 
@@ -501,15 +502,24 @@ object TreeOps {
           Some(LetTuple(remIds, Tuple(remExprs), newBody))
         }
 
+      case l @ LetTuple(ids, tExpr: Terminal, body) if !containsChoose(body) =>
+        val substMap : Map[Expr,Expr] = ids.map(Variable(_) : Expr).zipWithIndex.toMap.map {
+          case (v,i) => (v -> TupleSelect(tExpr, i + 1).setType(v.getType))
+        }
+
+        Some(replace(substMap, body))
+
       case l @ LetTuple(ids, tExpr, body) if !containsChoose(body) =>
-        val TupleType(types) = tExpr.getType
         val arity = ids.size
-        // A map containing vectors of the form (0, ..., 1, ..., 0) where the one corresponds to the index of the identifier in the
-        // LetTuple. The idea is that we can sum such vectors up to compute the occurences of all variables in one traversal of the
-        // expression.
         val zeroVec = Seq.fill(arity)(0)
         val idMap   = ids.zipWithIndex.toMap.mapValues(i => zeroVec.updated(i, 1))
 
+        // A map containing vectors of the form (0, ..., 1, ..., 0) where
+        // the one corresponds to the index of the identifier in the
+        // LetTuple. The idea is that we can sum such vectors up to compute
+        // the occurences of all variables in one traversal of the
+        // expression.
+
         val occurences : Seq[Int] = treeCatamorphism[Seq[Int]]((e : Expr) => e match {
           case Variable(x) => idMap.getOrElse(x, zeroVec)
           case _ => zeroVec
@@ -531,6 +541,7 @@ object TreeOps {
 
       case _ => None
     }
+
     searchAndReplaceDFS(simplerLet)(expr)
   }
 
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 63abcb42aee7a04212fcb97e5dea7175038d715e..c402b865cd2e22da46f52936492f7a9044acd8b4 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -66,7 +66,6 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
   // This is fixed.
   protected[leon] val z3cfg = new Z3Config(
     "MODEL" -> true,
-    "MBQI" -> false,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
   )
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 78b75ee5eefdf13907ea1e7d068c9341bc0744fc..d9f2696caa0f8fe463b68728cb9bf7c5a8105d77 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -31,7 +31,6 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
   // this is fixed
   protected[leon] val z3cfg = new Z3Config(
     "MODEL" -> true,
-    "MBQI" -> false,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
   )