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

336 Commits

Author SHA1 Message Date
Claude Marche
6f2e594fa1 reproducer and fix 2025-09-29 18:16:21 +02:00
Matteo Manighetti
7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 2025-01-14 19:48:35 +01:00
Claude Marche
2e1d53f51b fix sessions and CE oracles 2024-11-14 14:48:30 +01:00
Claude Marche
0e86c23d93 add regression test from BTS 2024-11-13 19:04:53 +01:00
Claude Marche
3076170027 update sessions 2024-11-03 11:48:13 +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
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
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
Claude Marche
27fb33580e Support for Coq 8.19.2 2024-10-03 11:19:54 +02:00
MARCHE Claude
97c6cacdfd take type variables instances into account in execution engine 2024-10-01 11:44:59 +02:00
MARCHE Claude
7dd2b50449 Pmodule: t->t->t functions can be overloaded as X->X->t functions 
allows to add program equality on Booleans
 2024-09-19 10:54:24 +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
4d68a5a802 disabled Alt-Ergo FPA for versions < 2.5.4 (bug known) 2024-05-23 11:17:31 +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
BONNOT Paul
2410ff364d Added missing prover alternative FPA for Alt-Ergo 2.5.x 2024-01-08 20:14:24 +00: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
Claude Marche
d08d6c287d reinforce pre-conditions of safe machine floats operations 2023-09-18 17:42:25 +02:00
BONNOT Paul
2444f6c60a Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers. 2023-09-07 18:05:01 +00:00