Which is better practice in SMT: to add multiple a

Question

Lets say I have two clauses that I want to model in SMT, is it better to add them as separate assertions like

(assert (> x y))
(assert (< y 2))

or to add one assertion with and operator like this

(assert (and 
(> x y)
(< y 2)
))

Does this matter for large scale problems in terms of SMT solver performance. I am using Z3.

Answer 1

The conjunction gets split into multiple assertions, so it doesn't really matter too much. If you introduce a large conjunction, Z3's parser will create a term that contains all the conjuncts, but this is just a constant overhead on top of maintaining the conjuncts.