Size of constraints in the Z3 Solver()

Question

Is there a way for us to get how many constraints were added into the solver? For example, we initialize a z3 solver s = Solver() and then adding constraints to it using s.add(). How can we get the number of constraints which were finally added to the solver?

Answer 1

You can use the assertions method:

from z3 import *

s = Solver()

i = Int('i')
s.add (i > 1)
s.add (i < 12)

print s.assertions()
print len(s.assertions())

This prints:

[i > 1, i < 12]
2