Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • why3 why3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 134
    • Issues 134
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 18
    • Merge requests 18
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3
  • why3why3
  • Issues

  • Open 134
  • Closed 508
  • All 642
New issue
  • Priority Created date Updated date Milestone due date Due date Popularity Label priority Manual Title
  • Pattern matching with record leads to a crash for CVC4 & Z3
    #644 · created May 05, 2022 by Guillaume Cluzel   component: drivers
    • 2
    updated May 05, 2022
  • Examples missing from the gallery   0 of 10 tasks completed
    #643 · created Apr 29, 2022 by Guillaume Melquiond   component: website
    • 0
    updated Apr 29, 2022
  • Use Python's type variables
    #642 · created Apr 28, 2022 by Guillaume Melquiond   component: syntax
    • 0
    updated Apr 28, 2022
  • Mlw_printer should print source locations
    #641 · created Apr 22, 2022 by MARCHE Claude   ProofInUse/TrustInSoft
    • 0
    updated Apr 22, 2022
  • Model term without location leads to a failure of the rac prover
    #640 · created Apr 20, 2022 by Guillaume Cluzel   ProofInUse/TrustInSoft component: counterexample
    • 3
    updated May 13, 2022
  • MLCFG: allow arbitrary `let .. in ..` at the top of cfg function bodies
    #639 · created Apr 15, 2022 by MARCHE Claude
    • 0
    updated Apr 15, 2022
  • fix usage of optional argument `me_name_trans` in functions on models
    #638 · created Apr 11, 2022 by MARCHE Claude   component: counterexample
    • 0
    updated Apr 11, 2022
  • provide axioms for sdiv and smod in theory bitvector theory
    #637 · created Apr 08, 2022 by MARCHE Claude   ProofInUse/TrustInSoft
    • 0
    updated Apr 08, 2022
  • Review the set of 'old versions' of provers   0 of 6 tasks completed
    #633 · created Apr 06, 2022 by MARCHE Claude   1.6.0
    • 1
    • 0
    updated Apr 25, 2022
  • Document [@vc:xxx] attributes
    #627 · created Mar 24, 2022 by MARCHE Claude   ProofInUse/TrustInSoft component: documentation
    • 0
    updated Apr 08, 2022
  • Variants on custom relations always introduce polymorphism
    #626 · created Mar 17, 2022 by MARCHE Claude   ProofInUse/TrustInSoft
    • 2
    updated Apr 22, 2022
  • Allow running prover in parallel in strategies
    #625 · created Mar 17, 2022 by MARCHE Claude   ProofInUse/TrustInSoft
    • 0
    updated Apr 08, 2022
  • Check counterexamples classification benchmark   28 of 38 tasks completed
    #623 · created Mar 15, 2022 by MOREAU Solene   ProofInUse/AdaCore component: counterexample
    • 0
    updated Apr 08, 2022
  • Improve IDE for counterexamples   0 of 2 tasks completed
    #622 · created Mar 14, 2022 by MOREAU Solene   component: counterexample component: graphical user interface
    • 0
    updated Mar 14, 2022
  • Allow giant-step only in `Check_ce.select_model`
    #619 · created Mar 09, 2022 by MARCHE Claude   ProofInUse/AdaCore ProofInUse/TrustInSoft component: counterexample
    • 1
    • 1
    updated Apr 22, 2022
  • make bench fails without Alt-Ergo 2.3.3
    #618 · created Mar 09, 2022 by MARCHE Claude
    • 0
    updated Mar 09, 2022
  • Add a ``File > Export...`` feature
    #617 · created Mar 02, 2022 by MONTAGU Benoit   component: graphical user interface
    • 0
    updated Mar 02, 2022
  • Extend Ptree helpers   0 of 3 tasks completed
    #616 · created Feb 28, 2022 by MARCHE Claude   ProofInUse/MERCE ProofInUse/TrustInSoft
    • 0
    updated Apr 22, 2022
  • z3 driver should not unfold definitions
    #611 · created Feb 04, 2022 by MARCHE Claude   ProofInUse/TrustInSoft component: drivers
    • 1
    updated Apr 08, 2022
  • add a notion of label in MLCFG
    #608 · created Jan 05, 2022 by MARCHE Claude
    • 0
    updated Jan 05, 2022
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • …
  • 7
  • Next