diff --git a/testcases/verification/map/BasicMap.scala b/testcases/verification/map/BasicMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2cb3a907e24c66ec139239d91ee017aee5019bdd
--- /dev/null
+++ b/testcases/verification/map/BasicMap.scala
@@ -0,0 +1,17 @@
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+object BasicMap {
+
+  def insert(m: Map[BigInt, BigInt], key: BigInt, value: BigInt): Map[BigInt, BigInt] = {
+    require(!m.isDefinedAt(key))
+    m + (key -> value)
+  } ensuring(res => res(key) == value)
+
+  def unionWorks(m1: Map[BigInt, BigInt], m2: Map[BigInt, BigInt], key: BigInt): Boolean = {
+    require(m1.isDefinedAt(key) || m2.isDefinedAt(key))
+    (m1 ++ m2).isDefinedAt(key)
+  }.holds
+  
+}