Fix inverted zero-divisor check in base MaySignedOverflow

[karoliineh]

The division case in MaySignedOverflow computed whether the divisor may contain zero with inverted logic. This caused nonzero divisors to be treated as possibly zero and vice versa.

Found when looking through sv-comp tasks, but I couldn't construct a good regression to expose it.

[michael-schwarz]

This could potentially have a non-trivial impact on the relational analyses that only keep relationships where things don't overflow.

[sim642]

Found when looking through sv-comp tasks, but I couldn't construct a good regression to expose it.

This could potentially have a non-trivial impact on the relational analyses that only keep relationships where things don't overflow.

Indeed, I think the query is just used for helper information for relational analyses, not for the no-overflow verdicts (which are set directly within the int domains).
Our SV-COMP conf uses assume_none, so I'm not sure it matters there, but in general it might.

If I were to guess, the reason this hasn't come up before is because the relational analyses probably can't handle division anyway. Or maybe divisions by non-zero constants at best.