Merge requests · Why3 / why3 · GitLab

Attention une mise à jour du service Gitlab va être effectuée le mardi 07 février entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes (habituellement de l'ordre de trois minutes).

SMTLIB theory of sequences

!803 · created Jan 31, 2023 by Jacques-Henri Jourdan
- 15
updated Jan 31, 2023
Native algebraic data types even in the presence of polymorphism 1 of 1 checklist item completed

!802 · created Jan 31, 2023 by Jacques-Henri Jourdan
- Approved
- 5
updated Feb 01, 2023
Draft: [driver] Exposes call-on-buffer API from driver

!801 · created Jan 30, 2023 by Loïc Correnson
- 6
updated Feb 01, 2023
[Colibri2] adds mapping for abs div mod cdiv cmod builtins

!800 · created Jan 26, 2023 by François Bobot
- 0
updated Jan 26, 2023
Try to use nicer name when compiling pattern

!790 · created Jan 09, 2023 by François Bobot
- 0
updated Jan 09, 2023
Resolve "Support for ADT in Alt-Ergo"

!786 · created Dec 06, 2022 by BONNOT Paul 1.6.0 ProofInUse/OCamlPro
- 8
updated Jan 18, 2023
micro-Python: global variables and logic functions

!775 · created Nov 17, 2022 by Jean-Christophe Filliâtre
- 0
updated Nov 17, 2022
Draft: Resolve "Add support for Colibri2 prover"

!761 · created Oct 26, 2022 by BONNOT Paul ProofInUse/TrustInSoft
updated Oct 26, 2022
Loc: enumerate columns starting from 1, not from 0

!760 · created Oct 26, 2022 by Andrei Paskevich To be discussed
- 1
- 11
updated Jan 11, 2023
Draft: Resolve "rac prover should be executed on a task before transformation compute"

!743 · created Oct 04, 2022 by MARCHE Claude 1.6.0 ProofInUse/AdaCore ProofInUse/TrustInSoft To be discussed
- 0
updated Oct 04, 2022
Changed the unsecure trusted_wf attribute mechanism into a more secure one

!736 · created Sep 14, 2022 by MARCHE Claude 1.6.0
updated Nov 15, 2022
Draft: New model parser for SMTv2 outputs, with stronger type checking

!728 · created Aug 29, 2022 by MARCHE Claude
updated Feb 01, 2023
Draft: Resolve "Attributes in variant clause"

!713 · created Jul 21, 2022 by MARCHE Claude ProofInUse/TrustInSoft
updated Jul 21, 2022
Draft: Collect functional values from prover model

!683 · created May 30, 2022 by MARCHE Claude ProofInUse/AdaCore
- 0
updated Jul 06, 2022
[Env] Generalize env with resolver

!674 · created May 09, 2022 by François Bobot
updated May 09, 2022
Subregion Analysis

!667 · created Apr 29, 2022 by Xavier Denis
updated Jan 11, 2023
Draft: Add support for Odoc

!592 · created Sep 24, 2021 by Guillaume Melquiond component: build system component: documentation
- 1
- 0
updated Sep 03, 2022
Draft: Predicate `list.Sorted.sorted` recursively-defined.

!571 · created Sep 03, 2021 by Mário Pereira
- 6
updated Sep 08, 2021
Draft: Resolve "New function for conversion from real to float"

!570 · created Sep 03, 2021 by MARCHE Claude
- 0
updated Sep 29, 2021
Draft: Resolve "Interface for Module" 2 of 4 checklist items completed

!557 · created Jun 30, 2021 by Benjamin Terra-Jorge component: syntax
updated May 25, 2022