Как использовать модельно-ориентированную проекцию Z3 из C/C++?

Question

Я хочу использовать модельно-ориентированную проекцию, которая поставляется с Z3 / Spacer из C / C++, я заметил Z3_qe_model_project в "z3_spacer.h", однако после нескольких экспериментов я так и не понял, как его использовать, так как по нему нет документации.

Возникает вопрос: как использовать модельно-ориентированную проекцию Z3 из C / C++?