At least in ensure and requires clauses for operations in enhancements, undefined functions are not reported--resulting in simple typos propagating as far as the VC generator and prover.
Log in to post a comment.
