diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 6ab9422e8f2bd4ece1f6451f3cc92def84905247..2d88f4f342e422ba3c61698d06be6cb6d05cb5c1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -91,7 +91,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
 
   def encodeMapType(tpe: TypeTree): TypeTree = tpe match {
     case MapType(from, to) =>
-      TupleType(Seq(SetType(from), RawArrayType(from, to)))
+      tupleTypeWrap(Seq(SetType(from), RawArrayType(from, to)))
     case _ => sys.error("Woot")
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 8a5b486c6dbda3fd52f4bc2e97e20a259fa59f67..3566b165b2ddab9fa977f6ed2dd6c66c646ff78c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -57,7 +57,7 @@ trait SMTLIBTarget {
 
   def normalizeType(t: TypeTree): TypeTree = t match {
     case ct: ClassType if ct.parent.isDefined => ct.parent.get
-    case tt: TupleType => TupleType(tt.bases.map(normalizeType))
+    case tt: TupleType => tupleTypeWrap(tt.bases.map(normalizeType))
     case _ =>   t
   }
 
@@ -435,7 +435,7 @@ trait SMTLIBTarget {
        * ===== Everything else =====
        */
       case ap @ Application(caller, args) =>
-        ArraysEx.Select(toSMT(caller), toSMT(Tuple(args)))
+        ArraysEx.Select(toSMT(caller), toSMT(tupleWrap(args)))
 
       case e @ UnaryOperator(u, _) =>
         e match {