Send messes with everything

[mrRachar]

Currently, any methods which contains send will require all fields and variables to be mutating. This is down to the Boogie output generating havocs for all variables in case send affects them, as right now the idea seems to be that as send is external, something bad could happen and thus nothing is certain.

Also, since they mess with everything, nothing can be proven after a send function as values could have been affected in a way which invalidates any pre- or mid-conditions

// Fix with mutates (every, single, thing) despite the function affecting no fields
func myFunc(implicit amount: Wei, account: Address) {
   send(account, &wei)
}