Thanks for this detailed writeup! The distinction between require and assert should also get clearer with the introduction of the SMT checker for assert (currently experimental with pragma experimental SMTChecker;). Note that you should not use assert blindly for overflow checking but only if you think that previous checks (either using ifor require) would make an overflow impossible.