It's interesting that the same issue arose with GNAT, but we had no option to ignore the special case, since one of the official Ada validation test programs tested this case, and indeed as you see below there is a special test:
function q (a, b : integer) return integer is begin return a rem b; end;
generates Source recreated from tree for q (body) --------------------------------------- function q (a : integer; b : integer) return integer is begin [constraint_error when b = 0 "divide by zero"] return integer((if b = -1 then 0 else a rem b)); end q; And indeed this is a nasty hit in efficiency, though in practice the wide spread use of integer types with restricted ranges means that most of the time you know for example that the divisor cannot be negative.