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 20
    • Merge Requests 20
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar

Mise à jour terminée. Pour connaître les apports de la version 13.10.3 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/03/22/gitlab-13-10-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/
https://about.gitlab.com/releases/2021/04/01/gitlab-13-10-2-released/
https://about.gitlab.com/releases/2021/04/14/security-release-gitlab-13-10-3-released/

  • Why3
  • why3why3
  • Issues
  • #362

Closed
Open
Created Jul 04, 2019 by Johannes Kanig@kanigDeveloper

overly generic logics declaration causes slowdown of cvc4 proof

Florian had identified a long time ago an issue where cvc4 would take much longer to prove a given VC if a non-linear arithmetic was specified compared to a linear one. See this ticket and the example in the ticket:

https://github.com/CVC4/CVC4/issues/1276

On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA and UFBVDTNIRA when using cvc4 on the example in the issue.

We were wondering if Why3 could be more precise, e.g. detecting when only linear operators are used. Given the potentially large speedups it seems worthwhile. The other idea mentioned in the TN to specify --inst-when-strict-interleave isn't an option for us.

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