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

24 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
174c9a01f5 do not allow implicit inference of partial 2024-10-31 15:27:09 +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
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
Andrei Paskevich
fe3bf96cd1 stdlib: proper postcondition for (=) on bounded integers 2023-06-17 00:16:27 +00: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
David Ewert
5f54fca95f Add "remove_unused:dependency" to int.ComputerDivision 2022-09-21 20:15:46 +00: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
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
Quentin Garchery
235e8dede9 fix examples euler_sieve and multiprecision/mpz_mul 2021-04-29 12:44:16 +02:00
Guillaume Melquiond
a07854cb17 Move tests/test-extraction to bench/extraction. 
This commit also cleans the bench infrastructure for extraction.
 2021-02-05 19:57:12 +01:00
Raphael Rieu-Helft
0f6909765d Fix c_cursor session and add it to regression tests 2020-08-27 11:37:07 +02:00
Raphael Rieu-Helft
c24a53f7f8 C extraction: use resets to detect array/struct escaping 2019-02-19 14:48:14 +01:00
Raphael Rieu-Helft
6a2a53eaa2 Improve extraction of arrays and mutable structs 2019-02-15 11:18:29 +01:00
Raphael Rieu-Helft
cc98359968 C cursor example 2019-02-08 10:27:49 +01:00