1202 Commits

Author	SHA1	Message	Date
Johannes Kanig	25b13e2cab	merge commit	2025-12-15 10:45:08 +09:00
Benjamin Jorge	25bf09e53a	Reproduce #894	2025-11-20 14:14:24 +01:00
Johannes Kanig	a2807b3ddb	Merge 1.8.2 into AdaCore master	2025-10-14 10:32:03 +09:00
Claude Marche	d344b75294	fix proofs in subdir numeric ... make them replayed in bench	2025-09-30 13:34:10 +02:00
Claude Marche	71fed79f48	update oracles	2025-09-16 13:53:09 +02:00
Claude Marche	d5cedf4c44	check-ce are done with AE 2.6.0	2025-09-16 10:37:15 +02: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
Paul Patault	6e847f2de7	coma: apply updated syntax in tests	2025-08-27 11:45:58 +02: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
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
Guillaume Melquiond	751ff8f3f7	Avoid mistakenly run the java bench if there is a runtime but no compiler.	2025-04-30 10:41:34 +02:00
Matteo Manighetti	2e931cf017	Update oracles	2025-03-27 10:28:05 +01:00
MARCHE Claude	52cc1f8f72	Merge branch 'rac-failure-log-environment' into 'master' ... Log entire environment at RAC failure See merge request why3/why3!1200	2025-03-27 08:36:53 +01:00
MARCHE Claude	997bdc53c1	add simple examples of iterators on sets with extraction to OCaml ... The stdlib is augmented with iterator mechanisms The OCaml extraction driver is augmented accordingly, using OCaml Seq	2025-03-26 17:20:01 +01:00
Claude Marche	222b2e0fcd	fix printing of execution logs	2025-03-26 17:18:53 +01:00
Claude Marche	534bd32d04	Do not introduce program variables for zero and one in int.Int module	2025-03-26 15:17:05 +01:00
Matteo Manighetti	9d2cf502df	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2025-03-25 18:02:22 +01:00
Matteo Manighetti	399658bd65	Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel	2025-03-25 17:55:52 +01:00
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
Benjamin Jorge	763b4f7f75	Expose bug	2025-03-13 15:53:52 +01:00
Matteo Manighetti	b8a4cfb714	Update oracles	2025-03-13 11:16:18 +01:00
Matteo Manighetti	5cec133cd5	Improve counterexample parsing: reconstruct polymorphic instances	2025-03-07 11:28:42 +01:00
Claude Marche	3ded61b16b	fix remaining warnings and CE oracles for UNDEFINED value	2025-03-03 11:26:10 +01:00