title: Z3: finding all satisfying models
body: <p>I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:</p>
  
  <pre><code>(declare-const f Bool)
  (assert (or (= f true) (= f false)))
  </code></pre>
  
  <p>In this propositional case there are two satisfying assignments: <code>f-&gt;true</code> and <code>f-&gt;false</code>. Because Z3 (and SMT solvers in general) will only try to find one satisfying model, finding all solutions is not directly possible. <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/smt__command.html#smt2_next_sat_example" rel="noreferrer">Here</a> I found a useful command called <code>(next-sat)</code>, but it seems that the latest version of Z3 no longer supports this. This is bit unfortunate for me, and in general I think the command is quite useful. Is there another way of doing this?</p>