Issues · Why3 / why3 · GitLab

Apply with x

#19 · opened Oct 31, 2017 by DAILLER Sylvain Nov 15, 2017 component: transformations priority: high
- CLOSED
- 2
updated Nov 16, 2017
"why3 config detect" detects every binary executable only once

#561 · opened Mar 03, 2021 by Guillaume Melquiond 1.4.0 component: configuration
- CLOSED
- 1
- 0
updated Mar 04, 2021
document mutually recursive types

#560 · opened Mar 02, 2021 by Jean-Christophe Filliâtre 1.4.0 component: documentation
- 1
- 0
updated Mar 02, 2021
Vanished invariant "expl" attribute

#559 · opened Feb 24, 2021 by Denis Cousineau
- 2
updated Feb 24, 2021
Overzealous positivity checker?

#558 · opened Feb 23, 2021 by Raphaël Rieu-Helft component: core
- CLOSED
- 5
updated Mar 03, 2021
Build a glossary of error messages

#557 · opened Feb 23, 2021 by MARCHE Claude component: documentation
- 0
updated Mar 01, 2021
Unused variable

#556 · opened Feb 22, 2021 by Guillaume Cluzel
- 1
updated Feb 23, 2021
Add support for `string` type and module `io` in `why3 execute`

#555 · opened Feb 19, 2021 by MARCHE Claude 1.5.0 component: execution
- 1
updated Mar 01, 2021
Document the modulo `io`, document printing capabilities

#554 · opened Feb 19, 2021 by MARCHE Claude 1.5.0 component: documentation
- 0
updated Mar 01, 2021
Broken uninstalled prover window

#553 · opened Feb 18, 2021 by Raphaël Rieu-Helft component: graphical user interface
- CLOSED
- 1
- 4
updated Feb 19, 2021
RFC: binders for tuple components in function prototype

#552 · opened Feb 10, 2021 by Jean-Christophe Filliâtre component: syntax feature wish
- 2
updated Feb 11, 2021
Module `mach.bv` should provide purely bitvector-based pre-conditions

#551 · opened Feb 09, 2021 by MARCHE Claude 1.5.0 component: theories
- 1
updated Feb 12, 2021
Add support for recent versions of Z3

#550 · opened Feb 08, 2021 by MARCHE Claude 1.4.0 component: drivers
- CLOSED
- 1
- 0
updated Feb 11, 2021
z3 4.5.1

#549 · opened Feb 07, 2021 by Bas Spitters
- CLOSED
- 2
updated Feb 07, 2021
Incorrect representation of float literal -1

#548 · opened Feb 03, 2021 by Guillaume Cluzel
- CLOSED
- 1
- 1
updated Feb 04, 2021
Syntactic sugar for lemma functions

#547 · opened Feb 03, 2021 by Loïc Correnson component: syntax feature wish
- 2
updated Feb 11, 2021
Inductive proofs on inductives

#546 · opened Feb 03, 2021 by Loïc Correnson component: core feature wish
- 10
updated Feb 11, 2021
why3 execute computes out of range values

#545 · opened Feb 03, 2021 by Guillaume Melquiond 1.4.0 component: execution soundness
- CLOSED
- 1
- 2
updated Feb 11, 2021
transformation `compute` is too permissive with respect to division

#544 · opened Feb 03, 2021 by MARCHE Claude 1.4.0 component: execution soundness
- CLOSED
- 1
- 0
updated Feb 11, 2021
why3 execute fails with "anomaly: Not_found"

#543 · opened Feb 02, 2021 by Guillaume Melquiond component: execution
- CLOSED
- 1
- 1
updated Feb 11, 2021

Prev
1
2
3
4
5
…
28
Next