Casting a Z3 integer expression to a C/C++ int
===

I'm new to Z3 and searched for the answer to my question here and on Google. Unfortunately, I was not successful.

I'm using the Z3 4.0 C/C++ API. I declared an undefined function <em>d: (Int Int) Int</em>, added some assertions, and computed a model. So far, that works fine.

Now, I want to extract certain values of the function <em>d</em> defined by the model, say <em>d(0,0)</em>. The following statement works, but returns an expression rather than the function value, i.e., an integer, of <em>d(0,0)</em>.

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

The check

    result.is_int();

returns <em>true</em>.

My (hopefully not too stupid) question is how to cast the returned expression to a C/C++ int?

Help is very appreciated. Thank you!