diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 2b89efb9abbf96111e68338256399569a075027f..49174d46989189cc12e45bfea7f0658a4fcc63ef 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -543,13 +543,16 @@ trait CodeExtraction extends Extractors {
       case ExMapApply(m,f) => {
         val rm = rec(m)
         val rf = rec(f)
-        MapGet(rm, rf).setType(rm.getType match {
+        val tpe = rm.getType match {
           case MapType(_,toType) => toType
           case _ => {
             if (!silent) unit.error(tree.pos, "apply on non-map expression")
             throw ImpureCodeEncounteredException(tree)
           }
-        })
+        }
+        val mg = MapGet(rm, rf).setType(tpe)
+        val ida = MapIsDefinedAt(rm, rf)
+        IfExpr(ida, mg, Error("key not found for map access").setType(tpe)).setType(tpe)
       }
       case ExMapIsDefinedAt(m,k) => {
         val rm = rec(m)
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index 0b4cb19243b893f05260b7f19631e2c7232d6793..e4797d1beb5dc57e7244208058cb55b9c717e570 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -155,8 +155,37 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
       toRet
     }
 
+    def generateMapAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+      val toRet = if (function.hasBody) {
+        val cleanBody = matchToIfThenElse(function.body.get)
+
+        val allPathConds = collectWithPathCondition((t => t match {
+          case Error("key not found for map access") => true
+          case _ => false
+        }), cleanBody)
+
+        def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
+          Not(And(matchToIfThenElse(function.precondition.get), And(conds)))
+        } else {
+          Not(And(conds))
+        }
+
+        allPathConds.map(pc =>
+          new VerificationCondition(
+            withPrecIfDefined(pc._1),
+            function,
+            VCKind.MapAccess,
+            this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+        ).toSeq
+      } else {
+        Seq.empty
+      }
+
+      toRet
+    }
+
     def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
-      Seq.empty
+      generateMapAccessChecks(function)
     }
 
     // prec: there should be no lets and no pattern-matching in this expression
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index d40e54ed876be6138425bac783cb751d2974fc17..c1a61b6981a8c016b9a4a20c1908e653e8738c95 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -886,11 +886,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         }
         case mg @ MapGet(m,k) => m.getType match {
           case MapType(fromType, toType) =>
-            val errorAST = z3.mkFreshConst("errorValue", typeToSort(toType))
-            // exprToZ3Id += (e -> errorAST)
-            // z3IdToExpr += (errorAST -> e)
             val selected = z3.mkSelect(rec(m), rec(k))
-            z3.mkITE(z3.mkDistinct(selected, mapRangeNoneConstructors(toType)()), mapRangeValueSelectors(toType)(selected), errorAST)
+            mapRangeValueSelectors(toType)(selected)
           case errorType => scala.Predef.error("Unexpected type for map: " + (ex, errorType))
         }
         case MapUnion(m1,m2) => m1.getType match {
diff --git a/src/purescala/VerificationCondition.scala b/src/purescala/VerificationCondition.scala
index b62c5f176f1bf3cfd534a1599c8c4f6d92be7a7a..7c6710fa2c1ae1b30109ddc16a832d6316bbe8ff 100644
--- a/src/purescala/VerificationCondition.scala
+++ b/src/purescala/VerificationCondition.scala
@@ -48,4 +48,5 @@ object VCKind extends Enumeration {
   val Precondition = Value("precond.")
   val Postcondition = Value("postcond.")
   val ExhaustiveMatch = Value("match.")
+  val MapAccess = Value("map acc.")
 }