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 real.MinMax
:
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information