diff --git a/testcases/MultiBug.scala b/testcases/MultiBug.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1336fa8f59081048c935298033ac2316ee1155d5
--- /dev/null
+++ b/testcases/MultiBug.scala
@@ -0,0 +1,10 @@
+import scala.collection.immutable.Set
+import scala.collection.immutable.Multiset
+
+object MultisetOperations {
+
+  def disjointUnion2(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+    a +++ b
+  } ensuring(res => res.toSet == (a.toSet ++ b.toSet))
+
+}
diff --git a/testcases/MultiExample.scala b/testcases/MultiExample.scala
new file mode 100644
index 0000000000000000000000000000000000000000..732cbaa082f68bb8c8861546103b04b0e20e9f7e
--- /dev/null
+++ b/testcases/MultiExample.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+import scala.collection.immutable.Multiset
+
+object MultisetOperations {
+
+/*
+  def disjointUnion1(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+    a +++ b
+  } ensuring(res => res.size == a.size + b.size)
+
+  def preservedUnderToSet1(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+    a ++ b
+  } ensuring(res => res.toSet == a.toSet ++ b.toSet)
+
+  def preservedUnderToSet2(a: Multiset[Int], b: Multiset[Int]) : Multiset[Int] = {
+    a ** b
+  } ensuring(res => res.toSet == a.toSet ** b.toSet)
+*/
+
+}