Full name of submitter (unless configured in github; will be published with the issue): Jim X
[intro.execution] p11 and p12 introduce the wording function invocation, which sounds like to have a different meaning with function call. [expr.call] p1 describes what a function call is; however, we don't define what function invocation is, which leaves the question of which evaluations occur within a function invocation for [intro.execution] p12. [intro.execution] p11 seems to be relevant but not explicit.
Suggested Resolution:
When invoking a function f (whether or not the function is inline), every argument expression and the postfix expression designating f are sequenced before every precondition assertion of f ([dcl.contract.func]), which in turn are sequenced before every expression or statement in the body of f, which in turn are sequenced before every postcondition assertion of f. These evaluations all occur within the function invocation f.