Z3 performance: many assertions vs large conjunction

Question

In my research I automatically generate SMT2, which I then pass to Z3. The generated code is basically one very large conjunction (and ...) of many different constraints. Will I be losing (or gaining?) any significant performance by doing this, as opposed to generating many assertions?

Answer 1

You won't be losing or gaining. In almost all settings, Z3 splits any conjunction into multiple assertions and the time it takes to do so is negligible.

This questions has also come up before: Which is better practice in SMT: to add multiple assertions or single and?