Cannot prove properties of multiset intersection

[viper-admin]

method test06(B: Multiset[Int], n: Int, x: Int)
  requires |B| == n
{
  var B1: Multiset[Int] := B intersection B
  assert |B1| == n // fails
  assert B1 == B   // fails
}

method test08(B: Multiset[Int], n: Int, x: Int, y: Int)
  requires |B| == n
{
  var B1: Multiset[Int] := B intersection Multiset(x, y)
  assert (x in B1) == (x in B) // holds
  assert |B1| <= 2             // fails
}

My guess is that the axiomatisation is insufficient.

[viper-admin]

@alexanderjsummers commented on 2014-09-12 09:14

see also Carbon issue 28