Skip to content

GitLab

why3
why3
Closed
Opened by Johannes Kanig@kanigDeveloper

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