As I noted in #1804:
domain tests don't check the overflow flags of abstract operator results. Moreover, when the concrete operator calculates the overflowed value, it's forced into bounds by the abstraction before leq check.
Also, the current concrete value generators are unlikely to generate ikind bounds, so #1803 wouldn't have been caught most likely.