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

51 Commits

Author SHA1 Message Date
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Claude Marche
2e1d53f51b fix sessions and CE oracles 2024-11-14 14:48:30 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Jacques-Henri Jourdan
1b9ff7667a Fix session timings on moloch 2023-10-23 09:18:45 +02:00
Jacques-Henri Jourdan
28369ea1c3 Fix sessions for nightly bench. 2023-10-22 15:49:03 +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
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
33115df1c9 fix sessions 2022-06-22 15:39:14 +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
Jean-Christophe Filliatre
144865a118 no more libraries appmap and impmap 
fixes #409
 2020-02-11 17:56:34 +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
dcad042d95 Fix session and counterexamples bench 2019-09-27 11:02:33 +02:00
DAILLER Sylvain
08857a1e85 Naming of ident: remove space in favor of "'" 
- change prefix "mk " into suffix "'mk"
- change prefix "VC " into suffix "'VC"
 2019-08-23 14:47:32 +02:00
Guillaume Melquiond
ac5b459da5 Update sessions. 2019-07-15 18:58:31 +02:00
Sylvain Dailler
1b71ca59c5 Update session and shapes 2019-05-20 17:09:01 +02:00
Sylvain Dailler
4fe56b451c Update obsolete session 2019-05-07 18:49:07 +02:00
Claude Marche
c4366cb352 update sessions 2019-05-06 22:35:38 +02:00
Jean-Christophe Filliatre
8a7974cf74 stdlib: set library revamped 2019-03-07 11:13:49 +01:00
DAILLER Sylvain
ebd8d5c6d2 Model record 2019-02-01 17:08:46 +01:00
Sylvain Dailler
25411b404d Update ce-bench and obsolete sessions 2018-10-24 12:38:38 +02:00