title: How is model generated with Z3?
body: <p>I'm currently working on a model counting approach with the SMT solver Z3. Does anyone know how Z3 does generate the models for e.g. the sort of linear arithmetics (LIA)? Which algorithm is used and where can I find the source code for that algorithm?</p>
  
  <p>Thanks,
  Yannic</p>