There are several C-Functions that allow you to extract different types of values, depending on the expected size of the numerals: Z3_get_numeral_int
, Z3_get_numeral_uint
, Z3_get_numeral_uint64
, Z3_get_numeral_int64
. For numbers that don't fit into those basic types, we can use the Z3_get_numeral_string
function to get a string representation that can be parsed into your preferred big-int representation.
Note that these functions are C-functions, not C++ functions, but those two APIs mix nicely. (See e.g, also z3 C++ API & ite).