title: Force Z3 to explore certain candidate space first?
body: <p>I had a question on smt-solvers (like Z3) and was wondering if you know any Z3-tactic which can help me achieve my objective.</p>
  
  <p>I want to know whether it is possible to force Z3 to explore some variables before exploring other variables.</p>
  
  <p>For examples, I have a scenario where my MaxSMT problem has the following hard constraints </p>
  
  <pre><code>X1 + X4 &gt;=3
  X2 + 7  &gt;=3
  X3 + 8  &gt;=3
  </code></pre>
  
  <p>And the soft-constraint is </p>
  
  <pre><code>X4 == 0
  </code></pre>
  
  <p>Here I want to force the smt-solver to first explore candidate space with different values for variable X1. (I believe by default Z3 will randomly explore different values of X1, X2, X3, X4)</p>
  
  <p>So my question is - is there any tactic in Z3 that allows me to tell the Z3-solver what candidate space (set of variables) should it try exploring first?</p>