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
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
MARCHE Claude
4d04b4f698 add metas for unused-dependencies on sequences 
also fix split_full that was losing metas for unused dependency
 2024-10-29 16:12:46 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
MARCHE Claude
7e819237a6 unused dependencies on Euclidean div/mod 2024-10-23 15:10:58 +02:00
Loïc Correnson
e2afddb11d Resolve "Add injectivity for type invariant" 2024-01-31 13:02:13 +00:00
BONNOT Paul
2444f6c60a Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers. 2023-09-07 18:05:01 +00:00
BONNOT Paul
617b6db4e6 Resolve "Remove axioms in Z3 and CVC4 drivers" 2023-09-01 15:47:33 +00: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
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
Claude Marche
22c68ef4fe update sessions 2022-05-24 11:34:40 +02:00
Benedikt Becker
64219c68e9 Fix sessions and update oracles for result variables in VC SP 2021-10-04 15:53:08 +02:00
Claude Marche
62e1037ff1 fix sessions 2021-09-03 11:59:11 +02:00
Claude Marche
500feab5d0 Merge branch 'master' into keep-vc-decls 2021-09-02 15:12:58 +02:00
MARCHE Claude
c6321cd5db Add a initial comment in shapes files 2021-08-25 10:49:04 +00:00
Benedikt Becker
b1a3e81a8b Update sessions 2021-08-04 10:31:28 +02:00
Claude Marche
62d925e898 fix sessions 2021-06-25 10:26:57 +02:00
Quentin Garchery
dda4dd1547 fix sessions 2021-04-29 09:10:56 +02:00
Andrei Paskevich
f4ca81247d Repair discriminate2 2021-04-08 12:26:07 +00:00
Guillaume Melquiond
dada254134 Update sessions. 2020-02-11 23:47:40 +01:00