How an infinite integer is represented in z3 ?

[L-Jun-Jie]

I want to define a 128 bit integer or rational number inside z3. I observed that there is rational class in z3, so I want to use it to define a 128 bit number. But several of its constructors don't seem to be able to initialize a 128-bit number.
My definition is as follows,
const rational pos_inf_128("2e128");
const rational neg_inf_128("-2e128");
After running it a segmentation error occurs, it seems that mpz doesn't support 128-bit number definitions.
What should I do? Thanks.