Assert needed to prove set cardinality of intersection over union

[viper-admin]

Created by @mschwerhoff on 2016-01-13 13:17

#!text

method test01(xs: Set[Int], ys: Set[Int], z: Int) {
	inhale |xs intersection ys| == 0
	inhale |xs intersection Set(z)| == 0
	exhale |xs intersection (ys union Set(z))| == 0 // Unexpectedly fails
}

method test02(xs: Set[Int], ys: Set[Int], z: Int) {
	inhale |xs intersection ys| == 0
	inhale |xs intersection Set(z)| == 0

  // Allows proving the final exhale
	assert    xs intersection (ys union Set(z))
	       == (xs intersection ys) union (xs intersection Set(z))

	exhale |xs intersection (ys union Set(z))| == 0
}