diff --git a/demo/Maps.scala b/demo/Maps.scala
index 79554aa5d72dcf5d0cefc09e053c92bbbf7e9fe9..96fe09f9411afb98c2e937a14d6284f7ac41865e 100644
--- a/demo/Maps.scala
+++ b/demo/Maps.scala
@@ -19,6 +19,10 @@ object Maps {
   // - solver
   // - printer OK
 
+  sealed abstract class List
+  case class Cons(head : Int, tail : List) extends List
+  case class Nil() extends List
+
   def applyTest(m : Map[Int,Int], i : Int) : Int = m(i)
 
   def isDefinedAtTest(m : Map[Int,Int], i : Int) : Boolean = m.isDefinedAt(i)
@@ -45,7 +49,7 @@ object Maps {
       true
   } holds
 
-  def findModel(m : Map[Int,Int]) : Boolean = {
-    m != Map.empty[Int,Int].updated(0, 42)
+  def findModel(m : Map[Int,List]) : Boolean = {
+    m == Map.empty[Int,List].updated(42, Nil()) || m == Map.empty[Int, List]
   } holds
 }
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 48d6cc92a8498c5b34cc2b3d2e04a9eac74ebd19..0af470ffdfc628719e854ce45c3b8bcfe463867f 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -11,6 +11,7 @@ trait Extractors {
   import global.definitions._
 
   private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
+  private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
   private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
   private lazy val optionClassSym = definitions.getClass("scala.Option")
 
@@ -404,7 +405,7 @@ trait Extractors {
     object ExFiniteSet {
       def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
         case Apply(TypeApply(Select(Select(Select(Select(Ident(s), collectionName), immutableName), setName), applyName), theTypeTree :: Nil), args) if (collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && applyName.toString == "apply") => Some((theTypeTree, args))
-        case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), setname), applyName), theTypeTree :: Nil), args) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && "apply".equals(applyName.toString)) => Some((theTypeTree, args))
+        case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), setName), applyName), theTypeTree :: Nil), args) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && setName.toString == "Set" && "apply".equals(applyName.toString)) => Some((theTypeTree, args))
         case _ => None
       }
     }
@@ -426,6 +427,13 @@ trait Extractors {
       }
     }
 
+    // object ExFiniteMap {
+    //   def unapply(tree: Apply): Option[(Tree,Tree,List[Tree])] = tree match {
+    //     case Apply(TypeApply(Select(Select(Select(Select(Ident(s), collectionName), immutableName), mapName), applyName), List(fromTypeTree, toTypeTree)), args) if (collectionName.toString == "collection" && immutableName.toString == "immutable" && mapName.toString == "Map" && applyName.toString == "apply") => Some((fromTypeTree, toTypeTree, args))
+    //     case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), mapName), applyName), List(fromTypeTree, toTypeTree)), args) if (scalaName.toString == "scala" && predefName.toString == "Predef" && mapName.toString == "Map" && applyName.toString == "apply") => Some((fromTypeTree, toTypeTree, args))
+    //     case _ => None
+    //   }
+    // }
 
     object ExUnion {
       def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index e6320c2c729b5ba201b55cf79aa3009bf88be044..e8eb68bd9bae88f4fe2dc7fc1ec771e08ee543b8 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -866,20 +866,20 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
           case MapType(fromType, toType) =>
             val fromSort = typeToSort(fromType)
             val toSort = typeToSort(toType)
-            val constArray = z3.mkConstArray(toSort, mapRangeNoneConstructors(toType)())
+            val constArray = z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
             z3.mkStore(constArray, rec(from), mapRangeSomeConstructors(toType)(rec(to)))
           case errorType => scala.Predef.error("Unexpected type for singleton map: " + (ex, errorType))
         }
         case e @ EmptyMap(fromType, toType) => {
           val fromSort = typeToSort(fromType)
           val toSort = typeToSort(toType)
-          z3.mkConstArray(toSort, mapRangeNoneConstructors(toType)())
+          z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
         }
         case f @ FiniteMap(elems) => f.getType match {
           case MapType(fromType, toType) =>
             val fromSort = typeToSort(fromType)
             val toSort = typeToSort(toType)
-            elems.foldLeft(z3.mkConstArray(toSort, mapRangeNoneConstructors(toType)())){ case (ast, SingletonMap(k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
+            elems.foldLeft(z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())){ case (ast, SingletonMap(k,v)) => z3.mkStore(ast, rec(k), mapRangeSomeConstructors(toType)(rec(v))) }
           case errorType => scala.Predef.error("Unexpected type for finite map: " + (ex, errorType))
         }
         case mg @ MapGet(m,k) => m.getType match {
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala
index 0d42c6aaa27f426c04f81b7e46da17920e12fb21..ebf8611495e5e1ffbf4601ccd5a112f2f9a98ed3 100644
--- a/src/purescala/Z3ModelReconstruction.scala
+++ b/src/purescala/Z3ModelReconstruction.scala
@@ -29,7 +29,7 @@ trait Z3ModelReconstruction {
           case Some(t) => model.getArrayValue(t) match {
             case None => None
             case Some((map, elseValue)) => 
-              assert(elseValue == mapRangeNoneConstructors(vt)())
+              // assert(elseValue == mapRangeNoneConstructors(vt)())
               val singletons = for ((index, value) <- map if z3.getASTKind(value) != mapRangeNoneConstructors(vt)()) yield {
                 z3.getASTKind(value) match {
                   case Z3AppAST(someCons, List(arg)) if someCons == mapRangeSomeConstructors(vt) => SingletonMap(fromZ3Formula(index), fromZ3Formula(arg))