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

300 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
Guillaume Melquiond
479fc1a339 Remove unused proofs. 2024-12-07 09:01:55 +01:00
Claude Marche
3076170027 update sessions 2024-11-03 11:48:13 +01:00
MARCHE Claude
7e819237a6 unused dependencies on Euclidean div/mod 2024-10-23 15:10:58 +02:00
MARCHE Claude
24baef2ce5 fix closure computation in remove_unused 2024-10-22 21:25:49 +02:00
PATAULT Paul
b3cc1652fc Do not remove properties of bv.Pow2 systematically 2024-10-04 16:35:37 +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
Claude Marche
58f515c5d3 fix sessions 2024-02-19 08:27:06 +01:00
Loïc Correnson
e2afddb11d Resolve "Add injectivity for type invariant" 2024-01-31 13:02:13 +00:00
Jacques-Henri Jourdan
1b9ff7667a Fix session timings on moloch 2023-10-23 09:18:45 +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
Matteo Manighetti
d31c53d53c Move CVC4 proofs to CVC5 2023-08-28 14:31:08 +02:00
Matteo Manighetti
92d760c7a4 Upgrade CVC3 proofs 2023-08-28 14:28:03 +02:00
Matteo Manighetti
63fc2cfe55 Upgrade Alt-Ergo 2.0.0 proofs 2023-08-28 14:22:55 +02:00
Matteo Manighetti
eddcb30d72 Update Alt-Ergo 2.3.x proofs 2023-08-28 14:17:52 +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
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
Xavier Denis
87af5d805b Initial bulk upgrade of z3 2023-04-13 09:43:18 +00:00
Claude Marche
e38489deed get rid of Eprover 1.4, Alt-Ergo 0.95, CVC4-1-5 "alt" 2023-04-11 11:42:24 +02:00
MARCHE Claude
2f66628fa8 upgrade proofs with Z3 4.6.0 to 4.7.1 2023-04-07 09:37:36 +00:00