title: Z3/Python getting python values from model
body: <p>How can I get real python values from a Z3 model? </p>
  
  <p>E.g.</p>
  
  <pre><code>p = Bool('p')
  x = Real('x')
  s = Solver()
  s.add(Or(x &lt; 5, x &gt; 10), Or(p, x**2 == 2), Not(p))
  s.check()
  print s.model()[x]
  print s.model()[p]
  </code></pre>
  
  <p>prints </p>
  
  <pre><code>-1.4142135623?
  False
  </code></pre>
  
  <p>but those are Z3 objects and not python float/bool objects. </p>
  
  <p>I know that I can check boolean values using <code>is_true</code>/<code>is_false</code>, but how can I elegantly convert ints/reals/... back to usable values (without going through strings and cutting away this extra <code>?</code> symbol, for example). </p>