cannot verify when changing two elements in a dictionary in one function

[wmanshu]

public func transfer1(to: Address, value: Int) 
    mutates (balances)
    post (balances[to] == prev(balances[to]) + prev(value))
  {
    balances[to] += value
  }

public func transfer2(to: Address, value: Int) 
    mutates (balances)
    post (balances[caller] == prev(balances[caller]) - prev(value))
  {
    balances[caller] -= value
  }

public func transfer3(to: Address, value: Int) 
    mutates (balances)
    post (balances[to] == prev(balances[to]) + prev(value))
    post (balances[caller] == prev(balances[caller]) - prev(value))
  {
    balances[caller] -= value
    balances[to] += value
  }

transfer1 and transfer2 can pass the verifier. However, if we combine them together, the transfer3 cannot be verified:

Could not verify post-condition holds by end of function at line 68, column 10:
  public func transfer3(to: Address, value: Int)

[wmanshu]

Sloved by adding pre-condtion