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?
3
votes
I dare say that you won't get a definite answer for your question, given that you don't give any details about the theories your constraints fall into. And even if you did, it will probably still be difficult to give a satisfying. I suggest you run experiments first (generate both shapes), and if need be, come back here to report on your findings and to refine your question in light of those findings.
– Malte Schwerhoff
1 Answers
3
votes
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?
