Merge requests · Why3 / why3 · GitLab

Mentions légales du service

Support for Coq 8.19.2

!1140 · created Oct 03, 2024 by MARCHE Claude 1.8.0
- Merged
updated Oct 03, 2024
Resolve "Add support for Alt-Ergo 2.6 and last versions of Z3 and cvc5"

!1137 · created Oct 02, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 03, 2024
Resolve "effect is now a keyword in OCaml 5.3"

!1136 · created Oct 02, 2024 by PATAULT Paul 1.8.0
component: build system
updated Oct 04, 2024
Drivers: fix issue #879

!1134 · created Oct 02, 2024 by PATAULT Paul
component: provers
- Merged
- 6
- Approved
updated Oct 04, 2024
Draft: Coma in TryWhy3

!1142 · created Oct 06, 2024 by PATAULT Paul
component: trywhy3 feature wish priority: low
- 1
updated Oct 07, 2024
Draft: Resolve "Improve documentation of extraction to C"

!1069 · created May 15, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Closed
updated Oct 07, 2024
Draft: Resolve "Driver FPA for AE 2.5 should map the rounding fct of ieee_float to its builtin"

!1133 · created Oct 01, 2024 by MARCHE Claude 1.8.0
Décysif
- Closed
- 1
updated Oct 08, 2024
Resolve "Alt-Ergo 2.6 don't need FPA alternative. But BV and CE should be added"

!1141 · created Oct 03, 2024 by MARCHE Claude 1.8.0
Décysif
- Merged
updated Oct 08, 2024
do not take resource limits from more than one source

!1145 · created Oct 07, 2024 by MARCHE Claude 1.8.0
ProofInUse/AdaCore
- Merged
updated Oct 08, 2024
Ensures filenames in spans are relative to the file they occur in

!1146 · created Oct 11, 2024 by MARCHE Claude 1.8.0
Creusot
- Merged
updated Oct 11, 2024
Evaluate impact of intro_vc_vars_counterexmp

!1070 · created May 15, 2024 by Matteo Manighetti 1.8.0
Décysif ProofInUse/AdaCore
- Merged
- 8
- 1
updated Oct 11, 2024
Make it easier to support statically linked commands.

!1139 · created Oct 02, 2024 by Guillaume Melquiond 1.8.0
component: tools
- Merged
- 1
updated Oct 11, 2024
ensure step limit has priority over time limit

!1148 · created Oct 11, 2024 by MARCHE Claude
- Merged
updated Oct 12, 2024
Resolve "Span file resolution logic different for module identifiers"

!1147 · created Oct 11, 2024 by MARCHE Claude 1.8.0
Creusot Décysif
- Merged
updated Oct 12, 2024
gallery: a small result about Fibonacci numbers

!1149 · created Oct 16, 2024 by Jean-Christophe Filliâtre
- Merged
updated Oct 16, 2024
Coma fixes

!1150 · created Oct 16, 2024 by Andrei Paskevich
- Merged
updated Oct 16, 2024
Coma: update examples

!1143 · created Oct 06, 2024 by PATAULT Paul
component: examples
updated Oct 17, 2024
Extend `why3 pp` so as to also output type definitions and logic definitions

!1151 · created Oct 18, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Merged
updated Oct 18, 2024
Make projections bind tighter than applications (fix #884).

!1152 · created Oct 21, 2024 by Guillaume Melquiond 1.7.3
component: core
- Merged
updated Oct 21, 2024
Draft: Resolve "keep less unused symbols"

!859 · created Apr 18, 2023 by MARCHE Claude
Hackathon component: counterexample
updated Oct 22, 2024

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