1209 Commits

Author	SHA1	Message	Date
Johannes Kanig	25b13e2cab	merge commit	2025-12-15 10:45:08 +09:00
Johannes Kanig	a2807b3ddb	Merge 1.8.2 into AdaCore master	2025-10-14 10:32:03 +09:00
Claude Marche	7650683aed	There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6	2025-09-15 13:53:30 +02:00
Johannes Kanig	4e4e13edaa	Alt-Ergo 2.6 driver, functions on reals, float rounding	2025-09-15 13:47:04 +02:00
Johannes Kanig	2ffed5e451	Adopt upstream changes for alt-ergo driver	2025-06-18 10:57:20 +09:00
Johannes Kanig	c0d28bd80c	Alt-Ergo 2.6 driver, functions on reals, float rounding	2025-06-18 10:45:39 +09:00
MARCHE Claude	89a894b47a	do not map IEEE floats theory to Alt-Ergo's own theory ... Upgrade to AE 2.6.2	2025-06-18 10:45:29 +09:00
Claude Marche	116c0aa789	There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6	2025-06-13 08:23:33 +02:00
MARCHE Claude	ff86d53bf2	Produce special float values in counterexamples	2025-06-11 13:09:37 +02:00
Johannes Kanig	0082a6412a	Alt-Ergo 2.6 driver, functions on reals, float rounding	2025-06-06 12:00:50 +02:00
MARCHE Claude	d547f17f49	do not map IEEE floats theory to Alt-Ergo's own theory ... Upgrade to AE 2.6.2	2025-05-22 19:49:00 +02:00
Matteo Manighetti	f39e24ed74	Merge branch 'master' into why3-devel	2025-03-25 17:47:35 +01:00
Johannes Kanig	57742895f4	New driver for Alt-ergo SMT, gnatprove style	2025-03-14 11:30:53 +09:00
Matteo Manighetti	c04b008016	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-12-13 17:34:11 +01:00
Matteo Manighetti	8d9026f3ac	Move CE oracles to Alt-Ergo 2.6.0	2024-12-06 16:09:37 +01:00
Claude Marche	cabea44347	fix realizations	2024-11-13 19:10:42 +01:00
Claude Marche	37bd944fa5	two forms of transformation extensionality	2024-11-13 19:04:53 +01:00
Guillaume Melquiond	94a1bb848f	Factor out the sequence "inline_trivial" to "remove_unused", and add "extensionality" to it.	2024-11-13 19:04:53 +01:00
Guillaume Melquiond	a7d0370df3	Add missing Coq definition for BuiltIn.string.	2024-11-08 13:48:11 +01:00
MARCHE Claude	6ce01d8b7e	Resolve "provide axioms for sdiv and smod in theory bitvector theory"	2024-11-02 08:36:31 +01:00
Matteo Manighetti	eaa5f2a6e7	Comment out prepare_for_counterexmp from drivers	2024-10-28 11:22:39 +01:00
Matteo Manighetti	1c65544ddb	Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac	2024-10-23 16:51:58 +02:00
Johannes Kanig	bfad32e47b	Add remove_unused transform to colibri driver ... This transformation is now needed for soundness	2024-10-16 18:25:22 +09:00
Matteo Manighetti	4ef9300722	Disable completely prepare_for_counterexamples	2024-10-11 13:30:51 +02:00
MARCHE Claude	25a128513d	drivers for Alt-Ergo 2.6: FPA implicit, CE and BV	2024-10-08 15:11:12 +02:00