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

367 Commits

Author SHA1 Message Date
Matteo Manighetti
445595866e Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel 2025-03-25 17:48:51 +01:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Matteo Manighetti
c04b008016 Merge remote-tracking branch 'why3-inria/master' into why3-devel 2024-12-13 17:34:11 +01:00
Guillaume Melquiond
137c1472a4 Remove some trailing spaces. 2024-12-07 09:01:55 +01:00
Claude Marche
2e1d53f51b fix sessions and CE oracles 2024-11-14 14:48:30 +01:00
Claude Marche
3076170027 update sessions 2024-11-03 11:48:13 +01:00
Matteo Manighetti
dca6530002 Merge remote-tracking branch 'why3-inria/master' into why3-devel 2024-10-30 14:11:24 +01:00
Claude Marche
8683c09ef2 fix obsolete sessions 2024-10-27 17:46:42 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Matteo Manighetti
1c65544ddb Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac 2024-10-23 16:51:58 +02: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
MARCHE Claude
25a128513d drivers for Alt-Ergo 2.6: FPA implicit, CE and BV 2024-10-08 15:11:12 +02:00
PATAULT Paul
b3cc1652fc Do not remove properties of bv.Pow2 systematically 2024-10-04 16:35:37 +02:00
MARCHE Claude
33f94a61d4 Merge branch '880-add-support-for-alt-ergo-2-6-and-last-versions-of-z3-and-cvc5' into 'master' 
Resolve "Add support for Alt-Ergo 2.6 and last versions of Z3 and cvc5"

Closes #880

See merge request why3/why3!1137
 2024-10-03 14:24:06 +02:00
Claude Marche
e48d2d01de Support for Alt-Ergo 2.6.0 2024-10-03 11:32:26 +02:00
Claude Marche
27fb33580e Support for Coq 8.19.2 2024-10-03 11:19:54 +02:00
Claude Marche
cc2b44edeb Support for Z3 4.13 and cvc5 1.1 and 1.2 2024-10-03 09:47:17 +02:00
Claude Marche
55e3d335ca fix session having extra edited files 2024-09-18 15:42:05 +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
Jacques-Henri Jourdan
3f74341ea3 Remove redondancy of bv_size definition in mach.bv. 
This was essentially defined twice : once in bv and once in mach.bv.
 2024-07-15 13:48:41 +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
Paul
a51c564919 Support for colibri2 
Added test where we prove false in version < 0.4
 2024-05-28 11:15:53 +02:00
Claude Marche
4d68a5a802 disabled Alt-Ergo FPA for versions < 2.5.4 (bug known) 2024-05-23 11:17:31 +02:00