title: What is the importance of the order of the assertions in Z3?
body: <p>I have two files whose content is identical except for the order in which I placed the assertions: in one file, the assertions are placed in the reverse order of the other. The first file (po-9.z3) is declared unsatifiable by Z3 in less than a second while the other (po.z3) cannot be verified within a minute.</p>
  
  <p>What could be the reason for this difference? I assumed that placing the assertions that will be involved in the verification earlier in the file would improve performances. However, the one that passes verification (po-9.z3) has most of the relevent / problem specific assertions at the bottom of the file. Also, in po.z3, while the theorem to be proved and the assumptions are at the top of the file, one important assertion (a first order formulation for a lambda expression) is put at the bottom of the file. When I bring it to the top, po.z3 verifies within less than a second.</p>
  
  <p>What would be the best order for me to produce the assertions in a z3 smt2 file?</p>