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

98 Commits

Author SHA1 Message Date
Claude Marche
2095b61181 eprover and spass and Z3 4.14 2025-12-11 12:03:25 +01:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Claude Marche
27fb33580e Support for Coq 8.19.2 2024-10-03 11:19:54 +02:00
MARCHE Claude
6e3d21b5f0 check that real.FromInt.from_int is correctly sent to Alt-Ergo 
updated sessions
 2024-09-17 10:44:53 +02:00
Claude Marche
341f530df1 update Coq proofs using lia instead of omega 2024-06-18 13:38:53 +02:00
Claude Marche
bcf91c0e6e updated coq proofs 2024-05-31 14:17:56 +02:00
MARCHE Claude
85916f62c6 never encode enums and records for Alt-Ergo 2024-05-22 12:18:37 +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
MARCHE Claude
2f66628fa8 upgrade proofs with Z3 4.6.0 to 4.7.1 2023-04-07 09:37:36 +00: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
bf7b08a7ff fix proofs 2022-06-02 14:56:20 +02:00
Claude Marche
22c68ef4fe update sessions 2022-05-24 11:34:40 +02:00
Claude Marche
47d57c2c39 update sessions 2022-03-25 15:49:33 +01:00
Guillaume Melquiond
8be9988d38 Update Coq proofs. 2022-03-20 20:34:51 +01: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
benedikt becker
a5e42659e9 Update sessions and proofs 2021-01-15 15:02:37 +01:00
Guillaume Melquiond
65618aa004 Avoid splitting between "path" and "name", as it makes scripting painful. 2020-03-04 15:33:07 +01: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