[C] False positive result for some solver backends

[Costandre97]

For the following program, I get differing results when using z3/cvc5 as backend compared to mathsat/yices/cvc4:

int g;
int main() {
    int x = 2147483647,  y;
    __CPROVER_assume(y >= x);
    __CPROVER_assert(__builtin_smul_overflow(5, y, &g), "overflow");
}

cbmc --z3 test.c yields [main.assertion.1] line 5 overflow: SUCCESS (same for CVC5)
while other solvers yield cbmc --mathsat test.c yields [main.assertion.1] line 5 overflow: FAILURE.
If I'm not mistaken the correct result should be the one yielded by Z3 (i.e. SUCCESS).
The issue seems to be in the encoding rather than the solvers; when dumping the smt files with --outfile cvc4 returns UNSAT
on the formula produced for Z3, while Z3 yields SAT on the formula produced for cvc4.

Version: CBMC built from 147a1e3 (latest)