Remove axioms in int.MinMax only for z3
The axioms in int.MinMax
were removed from the SMT output in !407 (merged) because they are implied by the definitions.
But with this change some tests could not be replayed (e.g., multiprecision/div
), because only newer versions of z3 are able to deduce the lemmas on the fly.
We should remove the axioms only from the SMT output for Z3 and keep it for other provers.