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

106 Commits

Author SHA1 Message Date
MARCHE Claude
89a894b47a do not map IEEE floats theory to Alt-Ergo's own theory 
Upgrade to AE 2.6.2
 2025-06-18 10:45:29 +09:00
Matteo Manighetti
8d9026f3ac Move CE oracles to Alt-Ergo 2.6.0 2024-12-06 16:09:37 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Jacques-Henri Jourdan
28369ea1c3 Fix sessions for nightly bench. 2023-10-22 15:49:03 +02:00
Matteo Manighetti
d31c53d53c Move CVC4 proofs to CVC5 2023-08-28 14:31:08 +02:00
Matteo Manighetti
bd4beefa5c Upgrade Z3 proofs 2023-08-28 14:29:51 +02:00
Claude Marche
9451890c1f updated sessions 2023-08-24 16:29:59 +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
MARCHE Claude
715fa89d16 separate transformations for intros, dequant, and remove_unused 
remove unused before reflection transformation

avoid subst to a unused symbol
 2023-04-25 12:20:08 +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
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
Nightly Build
9e5eb47599 Vc: keep sp_if's splittable (and update sessions) 2022-05-02 18:29:28 +02:00
MARCHE Claude
c6f793011c introduce_premises also "dequant" the let-ins 2022-04-21 16:23:20 +00: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
Jean-Christophe Filliatre
9f37e5db2f insertion_sort: lower versions of provers 2021-03-18 21:46:52 +01:00
Jean-Christophe Filliatre
1961800592 insertion_sort: cleaning up, auto deref, swap version 2021-03-18 18:33:45 +01:00
benedikt becker
a5e42659e9 Update sessions and proofs 2021-01-15 15:02:37 +01:00
Jean-Christophe Filliatre
49626575fa updated proof sessions on moloch 2021-01-13 12:02:58 +01:00