frem bitblaster gives incorrect result for (frem 3.0 2.0)

[nunoplopes]

(declare-const C (_ BitVec 8))
(assert (bvuge C #x80))
(assert (bvule C #x80))

(push)
(assert (= (fp.rem (fp #b0 C #b10000000000000000000000)
                       (fp #b0 #x80 #b00000000000000000000000))
               (fp #b0 #x7f #b00000000000000000000000)))
(check-sat)
(pop)

(assert (= (fp.rem (fp #b0 #x80 #b10000000000000000000000)
                       (fp #b0 #x80 #b00000000000000000000000))
               (fp #b0 #x7f #b00000000000000000000000)))
(check-sat)
(simplify (fp.rem (fp #b0 #x80 #b10000000000000000000000)
                       (fp #b0 #x80 #b00000000000000000000000)))

gives:

sat
unsat
(fp #b1 #x7f #b00000000000000000000000)

The 2 formulas are the same; but the first goes to the bitblaster, while the second uses the rewriter.
Talking with Christoph M. Wintersteiger (@wintersteiger), we agree the rewriter is correct (-1.0) and the bitblaster is wrong (1.0). x86's frem agrees with the rewriter.
Logging this issue so we don't forget.

P.S.: It would be nice to have fmod as well, though it seems the SMT standard only supports frem as well..

[wintersteiger]

Fixed, many thanks! That was indeed yet another bug in the FP->BV converter.