Bit-vector value in decimal

Question

Using C++ APIs, how can you extract the decimal value of a bit-vector constant from a model.

Answer 1

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).