Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 17
    • Merge Requests 17
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #512

Closed
Open
Opened Oct 28, 2020 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
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#512