Suggestion: integer division and linearization could be more precise

[rmonat]

Let us consider this simple program:

int m = rand(2, 9);
int y = rand(0, 2020);
int y2 = y + ((m + 1) / 12);

The relational numerical domain is able to infer that 12y + m ≤ 12y2 + 11 /\ 12y2 ≤ 12y + m + 1. I would have expected y2 = y since m+1 < 12 => (m+1)/12 = 0 over integers.

I guess the linearization could be improved in that case.