Building a rational AST using the C API

[turibe]

Using the C API, If I have two (large) integer ASTs, can I build a rational AST, similarly to Z3_get_numeral_rational_int64, but without the 64-bit limitation?

Bonus question: Is there a difference between Z3_get_numeral_rational_int64 and Z3_get_numeral_small? It's not clear from the API docs.

[NikolajBjorner]

you can divide them, then simplify, then the result is a numeral.
the default approach is to build a numeral from a string use the division sign / between numerator and denominator.

[turibe]

Thx. Looks like I must convert them to reals (Z3_mk_int2real) before doing the division with Z3_mk_div, otherwise the result is an int.