Преобразование целочисленного выражения Z3 в целое число C/C++

Я новичок в Z3 и искал ответ на свой вопрос здесь и в Google. К сожалению, я не добился успеха.

Я использую Z3 4.0 C/C++ API. Я объявил неопределенную функцию d:(Int Int )Int , добавил несколько утверждений и вычислил модель. Пока это работает нормально.

Теперь я хочу извлечь определенные значения функции d , определенные моделью, скажем, d (0,0). Следующий оператор работает, но возвращает выражение, а не значение функции, то есть целое число, из d (0,0).

z3::expr args[] = {c.int_val(0), c.int_val(0)};
z3::expr result = m.eval(d(2, args));

Чек

result.is_int();

возвращает true .

Мой (надеюсь, не слишком глупый )вопрос: как привести возвращаемое выражение к типу C/C++ int?

Помощь очень ценится. Благодарю вас!