more examples and a bug

testcases/MultiBug.scala

+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))
+
+}

testcases/MultiExample.scala

+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)
+*/
+
+}