Как читать строки smtlib2 с помощью Z3 C++ API?

Z3 C++ API явно не предоставляет эту функциональность как часть класса expr. Однако C++ API можно использовать вместе с C API, т. е. для этого можно использовать функцию Z3_parse_smtlib_string (или ..._file). Обратите внимание, что эта функция возвращает объект Z3_ast, который необходимо преобразовать в объект expr, чтобы вернуться в «мир» C++.

Простой пример:

#include <z3++.h>

...

context ctx;
Z3_ast a = Z3_parse_smtlib2_file(ctx, "test.smt2", 0, 0, 0, 0, 0, 0);    
expr e(ctx, a);
std::cout << "Result = " << e << std::endl;

Поскольку функции Z3_parse_smtlib2_* не выполняют проверку ошибок, при ошибках не будет выдаваться исключение. Это может быть достигнуто с помощью вызовов context::check_error().