In particular, it seems that you can't write a precondition before such a return, and so this would encourage you to omit the precondition so you could omit the "return" keyword.
Also, it encourages you to write complex expressions rather than splitting them up into subexpressions via constant declarations so that you could omit the "return".
I think a better approach would be to allow you to omit the "return" if there is only one return in the function.