title: What is the correct way to handle quantified formulas with respect to empty models?
body: <p>I'm playing with uninterpreted sorts and functions and cannot quite understand how quantified formulas interact with empty models. Here (also here <a href="http://rise4fun.com/Z3Py/6ets" rel="nofollow">http://rise4fun.com/Z3Py/6ets</a>) are some simple examples that somewhat confuse me:</p>
  
  <ol>
  <li><code>[∀v : False]</code> is unsat, while "intuitively" it holds for an empty model.</li>
  <li>Checking <code>[∃v : v = v]</code> yields an empty model while that does not have a satisfying assignment.</li>
  <li>Some formulas, seemingly equivalent to <code>[∃v : v = v]</code>, somehow prevent z3 from producing empty models. <code>[∃v, v1 : v = v1]</code> is one such example.  E.g., if we add such formula to a solver and then try to create something resembling an allsat procedure (adding more and more constraints to rule out more and more models), we would run into unsat before getting an empty model.</li>
  </ol>
  
  <p>So, could you please refer me to any documents/papers describing how z3 handles quantifiers and empty models?
  Also, if I choose to restrict my attention to nonempty models only, what is the correct way to ask z3 for that? Things like <code>[∃v, v1 : v = v1]</code> seem to do the trick, but is there a better way?</p>