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

118 Commits

Author SHA1 Message Date
Claude Marche
1558726fcb proper renaming of E prover 2.6 2025-12-11 13:58:58 +01:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Claude Marche
5f9169e032 fis sessions 2024-11-16 09:41:34 +01:00
Claude Marche
2e1d53f51b fix sessions and CE oracles 2024-11-14 14:48:30 +01:00
Guillaume Melquiond
35601b77e7 Switch to zarith (fix #298). 2024-11-08 22:05:42 +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
6e3d21b5f0 check that real.FromInt.from_int is correctly sent to Alt-Ergo 
updated sessions
 2024-09-17 10:44:53 +02:00
Guillaume Melquiond
09a71c74c0 Fix occurrences of "occurences". 2023-11-23 19:04:11 +01: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
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
578a7b15c8 fix corrupted session 2023-08-28 16:53:11 +02:00
Matteo Manighetti
bd4beefa5c Upgrade Z3 proofs 2023-08-28 14:29:51 +02:00
Matteo Manighetti
63fc2cfe55 Upgrade Alt-Ergo 2.0.0 proofs 2023-08-28 14:22:55 +02:00
Claude Marche
9451890c1f updated sessions 2023-08-24 16:29:59 +02:00
Matteo Manighetti
6bf507f32d upgrade bench scripts with CVC5 from 1.0.0 to 1.0.5, upgrade sessions 2023-07-11 15:13:50 +02:00
BONNOT Paul
58313caa48 Resolve "Give values to BV constants when cloning" 2023-06-16 08:44:32 +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
Claude Marche
9348513425 resurrect mark-obsolete and filters in why3 session update 2023-05-05 10:16:48 +02: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
5eef121a50 fix sessions 2023-04-09 18:33:02 +02: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