CODEWITHSUNDEEP
z3smt
zenna
zenna

Reputation: 9206

Z3 performance: many assertions vs large conjunction

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?

Upvotes: 3

Views: 286

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8402

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?

Upvotes: 3

Related Questions