Useless axioms for min and max in SMT output
The axioms in theory
int.MinMax should not be used by SMT solvers. So the following snippet should be added to
smt-libv2.gen, similar to what is already done for
theory int.MinMax syntax function min "(ite (< %1 %2) %1 %2)" syntax function max "(ite (< %1 %2) %2 %1)" remove allprops end
We have already put this in our Why3 repo, @bbecker could you take care of merging this in the INRIA repo if Why3 team agrees? The commit in AdaCore repo is 6cf79069ee96d8162c8d63031b21772f021f0b7b.