title: Z3: Extracting existential model-values
body: <p>I'm playing around with Z3's QBVF solver, and wondering if it's possible to extract values from an existential assertion. To wit, let's say I have the following:</p>
  
  <pre><code>(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))
  </code></pre>
  
  <p>This basically says that there is a "least" 16-bit unsigned value. Then, I can say:</p>
  
  <pre><code>(check-sat)
  (get-model)
  </code></pre>
  
  <p>And Z3-3.0 happily responds:</p>
  
  <pre><code>sat
  (model  (define-fun x!0 () (_ BitVec 16)
  #x0000)
  )
  </code></pre>
  
  <p>Which is really cool. But what I want to do is to be able to extract pieces of that model via get-value. Unsurprisingly, none of the following seem to work</p>
  
  <pre><code>(get-value (x))
  (get-value (x!0))
  </code></pre>
  
  <p>In each case Z3 rightly complains there's no such constant. Clearly Z3 has that information as evidenced by the response to the <code>(check-sat)</code> call. Is there any way to access the existential value automatically via <code>get-value</code>, or some other mechanism?</p>
  
  <p>Thanks..</p>