[nhc-bugs] More on integer division