Merge requests · Why3 / why3 · GitLab

Mentions légales du service

Get counterexample values from the log of RAC executions

!1106 · created Jul 24, 2024 by Matteo Manighetti 1.8.0
Décysif ProofInUse/AdaCore
- Merged
- 3
updated Oct 22, 2024
fix closure computation in `remove_unused`

!1154 · created Oct 22, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 22, 2024
unused dependencies on Euclidean div/mod

!1153 · created Oct 22, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 23, 2024
Resolve "Mlw printer incorrect for Eoptexn"

!1156 · created Oct 25, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 25, 2024
Add metas for unused dependencies in generated axioms

!1155 · created Oct 25, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 25, 2024
fix obsolete sessions

!1157 · created Oct 27, 2024 by MARCHE Claude
- Merged
updated Oct 27, 2024
Draft: Resolve "Usage of `Map.const` triggers polymorphism"

!956 · created Sep 18, 2023 by MARCHE Claude 1.9.0
updated Oct 30, 2024
add metas for unused-dependencies on sequences

!1159 · created Oct 29, 2024 by MARCHE Claude 1.8.0
Creusot Décysif
- Merged
updated Oct 30, 2024
Resolve "Extend Ptree helpers"

!1161 · created Oct 30, 2024 by MARCHE Claude 1.8.0
Décysif ProofInUse/MERCE ProofInUse/TrustInSoft
- Merged
updated Oct 31, 2024
do not allow implicit inference of partial

!1116 · created Sep 13, 2024 by MARCHE Claude 1.8.0
- Merged
- 4
updated Oct 31, 2024
Whyml2java

!1064 · created May 07, 2024 by Jean-Christophe Filliâtre 1.8.0
component: extraction
- Merged
- 2
- Approved
updated Oct 31, 2024
Bench add category java extract

!1162 · created Nov 03, 2024 by MARCHE Claude 1.8.0
- Merged
updated Nov 03, 2024
update sessions

!1163 · created Nov 03, 2024 by MARCHE Claude 1.8.0
- Merged
updated Nov 03, 2024
Resolve "New function for conversion from real to float"

!570 · created Sep 03, 2021 by MARCHE Claude 1.8.0
ProofInUse/AdaCore ProofInUse/TrustInSoft
- Merged
- 1
- 1
updated Nov 03, 2024
improved proof of rightmost bit trick

!1164 · created Nov 03, 2024 by MARCHE Claude 1.8.0
- Merged
updated Nov 03, 2024
remove use of cvc5 1.2.0

!1165 · created Nov 04, 2024 by MARCHE Claude 1.8.0
- Merged
updated Nov 04, 2024
Resolve "provide axioms for sdiv and smod in theory bitvector theory"

!1160 · created Oct 30, 2024 by MARCHE Claude 1.8.0
Décysif ProofInUse/TrustInSoft component: theories
- Merged
updated Nov 08, 2024
Add a transformation "extensionality" to help with proofs of equality.

!1158 · created Oct 28, 2024 by Guillaume Melquiond 1.8.0
component: transformations
- Merged
- 6
updated Nov 13, 2024
ease the proof of coincidence count

!1172 · created Nov 15, 2024 by MARCHE Claude 1.8.0
- Merged
updated Nov 15, 2024
fix Isab real for sets

!1170 · created Nov 13, 2024 by MARCHE Claude 1.8.0
- Closed
- 1
updated Nov 15, 2024

Prev
1
…
54
55
56
57
58
59
60
61
Next