SMT2 back-end float to bit-vector conversion of multiply hangs

Non-urgent, documented for completeness and so we don't forget rather than for an urgent fix.

$ cat path.c
#include <assert.h>

int main (void) {
        float f;

        assert(f * f > 28);

        return 0;
}

$ cbmc path.c --smt2 --outfile -

Works with --fpa as well.
