ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

72 Commits

Author SHA1 Message Date
Claude Marche
7620017bbf upgraded provers in examples 2025-12-09 10:43:46 +01:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Guillaume Melquiond
35601b77e7 Switch to zarith (fix #298). 2024-11-08 22:05:42 +01:00
MARCHE Claude
85916f62c6 never encode enums and records for Alt-Ergo 2024-05-22 12:18:37 +02:00
BONNOT Paul
617b6db4e6 Resolve "Remove axioms in Z3 and CVC4 drivers" 2023-09-01 15:47:33 +00:00
Matteo Manighetti
bd4beefa5c Upgrade Z3 proofs 2023-08-28 14:29:51 +02:00
Matteo Manighetti
92d760c7a4 Upgrade CVC3 proofs 2023-08-28 14:28:03 +02:00
Matteo Manighetti
63fc2cfe55 Upgrade Alt-Ergo 2.0.0 proofs 2023-08-28 14:22:55 +02:00
BONNOT Paul
29c71dbd51 add a meta to mark a symbol as never removed by remove_unused* 
mark some lemmas on division of real as removable if not needed
 2023-06-15 15:18:48 +00:00
Xavier Denis
87af5d805b Initial bulk upgrade of z3 2023-04-13 09:43:18 +00:00
MARCHE Claude
2f66628fa8 upgrade proofs with Z3 4.6.0 to 4.7.1 2023-04-07 09:37:36 +00:00
Claude Marche
75f8a9584a update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible 2023-04-05 13:48:22 +02:00
Nightly Build
0f4686159f update sessions 2022-10-07 12:40:08 +02:00
Claude Marche
db96723fd9 fix sessions 2022-07-07 15:49:23 +02:00
Claude Marche
ecb497d98a Merge branch 'master' into eliminate_unused_symbols 2022-06-23 07:51:51 +02:00
Claude Marche
33115df1c9 fix sessions 2022-06-22 15:39:14 +02:00
Claude Marche
8abedf035e fix sessions 2022-06-02 17:59:27 +02:00
Claude Marche
e7efe033be fix sessions 2021-10-30 11:11:24 +02:00
Claude Marche
62e1037ff1 fix sessions 2021-09-03 11:59:11 +02:00
Claude Marche
62d925e898 fix sessions 2021-06-25 10:26:57 +02:00
Guillaume Melquiond
dada254134 Update sessions. 2020-02-11 23:47:40 +01:00
Cláudio Belo Lourenço
a931ddb5a5 Sessions updated. 
In most cases the proof in CVC4 takes one step more than before due to
the why3 string built-in type. In a few cases the proof was updated.
 2019-10-29 22:37:11 +01:00
Sylvain Dailler
336a478250 Update session, ce-bench and coq files for "VC" -> "vc" in goal name 2019-10-11 21:01:43 +02:00
Sylvain Dailler
32d7cfe8de Rerun all sessions to update the file formats 
This also updates some of the "VC name" to "name'VC" that were never
updated.
 2019-09-24 17:58:31 +02:00
MARCHE Claude
1f766d2549 Remove all usages of obsolete library why3extract.cma 
Two of the three examples which are extracted to ocaml code and then to
javascript are not working, but they were broken since the new extraction
which is bound to the use of Zarith and not Num. They should be
repaired when js_of_ocaml supports Zarith
 2019-06-21 20:47:38 +02:00