Issues · Why3 / why3 · GitLab

Pattern matching with record leads to a crash for CVC4 & Z3

#644 · created May 05, 2022 by Guillaume Cluzel component: drivers
- 2
updated May 05, 2022
Examples missing from the gallery 0 of 10 tasks completed

#643 · created Apr 29, 2022 by Guillaume Melquiond component: website
- 0
updated Apr 29, 2022
Use Python's type variables

#642 · created Apr 28, 2022 by Guillaume Melquiond component: syntax
- 0
updated Apr 28, 2022
Mlw_printer should print source locations

#641 · created Apr 22, 2022 by MARCHE Claude ProofInUse/TrustInSoft
- 0
updated Apr 22, 2022
Model term without location leads to a failure of the rac prover

#640 · created Apr 20, 2022 by Guillaume Cluzel ProofInUse/TrustInSoft component: counterexample
- 3
updated May 13, 2022
MLCFG: allow arbitrary `let .. in ..` at the top of cfg function bodies

#639 · created Apr 15, 2022 by MARCHE Claude
- 0
updated Apr 15, 2022
fix usage of optional argument `me_name_trans` in functions on models

#638 · created Apr 11, 2022 by MARCHE Claude component: counterexample
- 0
updated Apr 11, 2022
provide axioms for sdiv and smod in theory bitvector theory

#637 · created Apr 08, 2022 by MARCHE Claude ProofInUse/TrustInSoft
- 0
updated Apr 08, 2022
Review the set of 'old versions' of provers 0 of 6 tasks completed

#633 · created Apr 06, 2022 by MARCHE Claude 1.6.0
- 1
- 0
updated Apr 25, 2022
Document [@vc:xxx] attributes

#627 · created Mar 24, 2022 by MARCHE Claude ProofInUse/TrustInSoft component: documentation
- 0
updated Apr 08, 2022
Variants on custom relations always introduce polymorphism

#626 · created Mar 17, 2022 by MARCHE Claude ProofInUse/TrustInSoft
- 2
updated Apr 22, 2022
Allow running prover in parallel in strategies

#625 · created Mar 17, 2022 by MARCHE Claude ProofInUse/TrustInSoft
- 0
updated Apr 08, 2022
Check counterexamples classification benchmark 28 of 38 tasks completed

#623 · created Mar 15, 2022 by MOREAU Solene ProofInUse/AdaCore component: counterexample
- 0
updated Apr 08, 2022
Improve IDE for counterexamples 0 of 2 tasks completed

#622 · created Mar 14, 2022 by MOREAU Solene component: counterexample component: graphical user interface
- 0
updated Mar 14, 2022
Allow giant-step only in `Check_ce.select_model`

#619 · created Mar 09, 2022 by MARCHE Claude ProofInUse/AdaCore ProofInUse/TrustInSoft component: counterexample
- 1
- 1
updated Apr 22, 2022
make bench fails without Alt-Ergo 2.3.3

#618 · created Mar 09, 2022 by MARCHE Claude
- 0
updated Mar 09, 2022
Add a ``File > Export...`` feature

#617 · created Mar 02, 2022 by MONTAGU Benoit component: graphical user interface
- 0
updated Mar 02, 2022
Extend Ptree helpers 0 of 3 tasks completed

#616 · created Feb 28, 2022 by MARCHE Claude ProofInUse/MERCE ProofInUse/TrustInSoft
- 0
updated Apr 22, 2022
z3 driver should not unfold definitions

#611 · created Feb 04, 2022 by MARCHE Claude ProofInUse/TrustInSoft component: drivers
- 1
updated Apr 08, 2022
add a notion of label in MLCFG

#608 · created Jan 05, 2022 by MARCHE Claude
- 0
updated Jan 05, 2022

Prev
1
2
3
4
5
…
7
Next