title: z3py, give random solution using seed
body: <pre><code>from z3 import *
  
  a = Int('a')
  
  s = Solver()
  s.add(a &gt; 0)
  set_option('smt.arith.random_initial_value', True)
  set_option('auto_config', False)
  set_option('smt.phase_selection', 5)
  set_option('smt.random_seed', 1)
  
  while s.check() == sat:
      m = s.model()
      print m[a]
      s.add(a != m[a])
  </code></pre>
  
  <p>The result is </p>
  
  <pre><code>1
  2
  3
  4
  5
  ...
  </code></pre>
  
  <p>How can I make the random work? <strong>Please provide an example in Python using z3py...</strong>
  I already know how to do this in smt... But I am having a real hard time figuring it out how to translate the smt script to python.</p>