diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 20c8c5ae0e0e5949fe1e3e50132d172c0bc7d2bc..8a38fd562998ef414ce1ec7743f98eeb61e3d4e4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -164,8 +164,9 @@ trait SMTLIBTarget {
       // We expect a RawArrayValue with keys in from and values in Option[to],
       // with default value == None
       require(from == r.keyTpe && r.default == OptionManager.mkLeonNone(to))
-      val elems = r.elems.mapValues {
-        case CaseClass(leonSome, Seq(x)) => x
+      val elems = r.elems.flatMap {
+        case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
+        case (k, _) => None
       }.toSeq
       finiteMap(elems, from, to)