title: z3: Is it possible to adjust the branching heuristics in Z3?
body: <p>This is a follow-up question of <a href="https://stackoverflow.com/questions/24346226/what-is-the-importance-of-the-order-of-the-assertions-in-z3">What is the importance of the order of the assertions in Z3?</a></p>
  
  <p>Given that Z3 uses DPLL algorithms. Suppose I have some knowledge about which variables are more critical. Is it possible that I make Z3 solver to branch on these variables first when evaluating my logic problem so as to boost the performance or efficiency?</p>