fix bug in folding of w comparisons

The casting to uint32_t made the code for comparing
two signed words invalid.  Interestingly, this can
be fixed by casting to int32_t instead.  Because
sign extension is monotonic, all the unsigned
comparisons remain valid.

CVC4 can even check that for us:

x, y : BITVECTOR(32);
QUERY BVLT(SX(x, 64), SX(y, 64)) <=> BVLT(x, y);
QUERY BVLE(SX(x, 64), SX(y, 64)) <=> BVLE(x, y);
QUERY BVGT(SX(x, 64), SX(y, 64)) <=> BVGT(x, y);
QUERY BVGE(SX(x, 64), SX(y, 64)) <=> BVGE(x, y);

0 files changed, 0 insertions, 0 deletions