Issues · Why3 / why3 · GitLab

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
- 4
updated Feb 23, 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
Execution of "division by zero" succeeds

#542 · opened Feb 02, 2021 by Guillaume Melquiond component: execution soundness
- CLOSED
- 12
updated Feb 11, 2021
The execute button in TryWhy3 no longer works

#541 · opened Feb 02, 2021 by Guillaume Melquiond 1.4.0 component: trywhy3 priority: blocker
- CLOSED
- 1
- 0
updated Feb 02, 2021
TryWhy3 crashes at startup: "caml_thread_initialize not implemented"

#540 · opened Feb 02, 2021 by Guillaume Melquiond 1.4.0 component: trywhy3 priority: blocker
- CLOSED
- 1
- 2
updated Feb 02, 2021

Prev
1
2
3
4
5
…
28
Next