title: Casting a Z3 integer expression to a C/C++ int
body: <p>I'm new to Z3 and searched for the answer to my question here and on Google. Unfortunately, I was not successful.</p>
  
  <p>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.</p>
  
  <p>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>.</p>
  
  <pre><code>z3::expr args[] = {c.int_val(0), c.int_val(0)};
  z3::expr result = m.eval(d(2, args));
  </code></pre>
  
  <p>The check</p>
  
  <pre><code>result.is_int();
  </code></pre>
  
  <p>returns <em>true</em>.</p>
  
  <p>My (hopefully not too stupid) question is how to cast the returned expression to a C/C++ int?</p>
  
  <p>Help is very appreciated. Thank you!</p>