Error at WeiAccounting trigger

[wmanshu]

In KotET.flint, contract ValidKotET, function dethrone
pastKings[king] = Wei(&pot, calculateCompensation())

cause an error:

Warning in /flint/stdlib/WeiAccounting.inv:
  This is the failing pre-condition
    Caused by WeiAccounting trigger at line 2, column 3:
    totalValue_Wei == receivedValue_Wei - sentValue_Wei

However in a simpler contract, KotET, we also have dethrone function, these two are similar except the line above. Doesn't have any problem.

  public func dethrone(implicit value: Wei)
    mutates (Wei.rawValue, king, claimPrice, pot, owner)

  {
    if value.rawValue < claimPrice {
      fatalError()
    }

    let oldKing: Address = king
    let compensation: Wei = Wei(&pot, calculateCompensation())

    self.claimPrice = calculateNewPrice(bid: value.rawValue)
    self.king = caller
    pot.transfer(source: &value)
    send(oldKing, &compensatiosn)
  }

func calculateCompensation() -> Int
  post (returns (pot.rawValue))
  {
    return pot.getRawValue()
  }