Ensure that Z3 uses the correct SMT-LIB2 syntax for push and pop

[aytey]

Issue

According to The SMT-LIB Standard Version 2.6, the operators push and pop are defined as follows:

| ( pop ⟨numeral ⟩ )
| ( push ⟨numeral ⟩ )

That is, they take an unsigned integer value for the number of "assertion levels" to push and pop.

However, if you ask Z3 to dump the SMT2 from the current instance (e.g., using the logFile kwarg in Python for a Solver) then this instance will contain (push) and (pop) with no integer arguments.

This makes it hard to re-use these SMT-LIB2 instances against other solvers (e.g., to submit benchmarks to SMT-LIB benchmarks) because the instances are not well-formed.

Solution

This PR changes all instance of (push) and (pop) with no arguments to be (push 1) and (pop 1), therefore making the instances usable across other SMT solvers, which are more strict on the syntax they accept.