If-else clause with some code and then returns

[wmanshu]

  @payable
  func placeBid(implicit value : inout Wei) -> Bool
  mutates (Wei.rawValue, highestBid, highestBidder)
  pre (value.rawValue > 0)
  pre (dictContains(pendingReturns, highestBidder) == true)
  post (returns(value.rawValue > highestBid.rawValue))

  {
    if value.rawValue <= highestBid.rawValue {
      return false
    } else {
    highestBid.transfer(source: &value)
    highestBidder = caller
    return true
  }
  }

The is-else problem before was fixed, however, it still cannot work in this case: If there are some other code before the return statement.

[mrRachar]

Is this an issue with the Boogie verification or in solidity?

[wmanshu]

Is this an issue with the Boogie verification or in solidity?

It's with Boogie.