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,278 Commits 65 Branches 1 Tag
fsf
Commit Graph

28 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
Claude Marche
5f9169e032 fis sessions 2024-11-16 09:41:34 +01:00
Claude Marche
ae24b5d7fd added LSE examples with fixed values for size 2024-11-15 17:29:45 +01:00
MARCHE Claude
9161acda8e Add metas for unused dependencies in generated axioms 2024-10-25 18:34:29 +02:00
Claude Marche
27fb33580e Support for Coq 8.19.2 2024-10-03 11:19:54 +02:00
MARCHE Claude
6813754dce clarify ghost and non-ghost for reals and ufloats 2024-10-01 15:38:42 +02:00
Claude Marche
3bb628674d new example for numeric strategy 2024-09-24 15:14:35 +02:00
Claude Marche
052edfd29e no need for FPa for these proofs 2024-09-02 11:13:06 +02:00
Paul Bonnot
4615f31920 Correct issue 2024-07-01 17:24:15 +02:00
Claude Marche
45f773f588 improve readibility, and various small improvements 2024-06-21 14:38:55 +02:00
Claude Marche
8dc497a29b nicer post-condition for raytracer 2024-06-20 15:43:25 +02:00
Claude Marche
2cbd37f344 cleaning kinematics example 2024-06-20 12:01:06 +02:00
BONNOT Paul
f24be4fce6 SLSE example : simplify proof 2024-06-18 13:41:01 +02:00
Claude Marche
fb9cc77d53 clean the strategy code, use more reasonable approx of sin and cos 2024-06-11 14:06:18 +02:00
Paul Bonnot
fa655adbbf Some LSE improvements 2024-06-10 17:48:06 +02:00
Paul Bonnot
2b743b654c Correct sessions 2024-06-10 17:43:15 +02:00
Paul Bonnot
86b958793f Merge branch 'master' into 861-forward-propagation-strategy-remove-higher-order-for-sin-cos-log-exp 2024-06-10 17:06:30 +02:00
Paul Bonnot
7c3e02999d Remove higher order 2024-06-10 16:44:04 +02:00
BONNOT Paul
c602729144 New proofs of LSE and SLSE with modified strategy 2024-06-10 15:56:47 +02:00
MARCHE Claude
0b76901deb Reduce the size of the formula produced, using let bindings so as to share common subterms 2024-05-28 15:10:42 +02:00
MARCHE Claude
4e2a198484 Merge branch '851-forward-propagation-strategy-some-cleanup-and-improvements' into 'master' 
Resolve "Forward propagation strategy : Some cleanup and improvements"

Closes #851

See merge request why3/why3!1067
 2024-05-27 13:48:51 +02:00
Claude Marche
4d68a5a802 disabled Alt-Ergo FPA for versions < 2.5.4 (bug known) 2024-05-23 11:17:31 +02:00
Paul Bonnot
6a228532f2 Add sqrt test 2024-05-14 12:00:04 +02:00
Paul Bonnot
103af257d0 Removed inline_trivial 2024-04-22 17:41:45 +02:00
BONNOT Paul
79666d1218 Resolve "forward_propagation strategy : sin and cos support" 2024-03-28 15:49:24 +01:00