372 Commits

Author	SHA1	Message	Date
Johannes Kanig	25b13e2cab	merge commit	2025-12-15 10:45:08 +09:00
Jean-Christophe Filliatre	4bc892fd02	a better theory seq.Sum ... do not sum the elements, but rather the application of a function to the elements	2025-12-03 19:01:11 +01:00
Claude Marche	fc857b2fc2	proved udivexact generique	2025-11-25 11:26:25 +01:00
Claude Marche	b9feb6aece	proved mul generique	2025-11-25 10:49:15 +01:00
Claude Marche	d17a7b64b7	redone sum_accuracy and g_accuracy	2025-11-24 11:33:09 +01:00
Claude Marche	13410bfc8f	cleaning	2025-11-24 11:22:11 +01:00
Claude Marche	9c60b5f0d6	add propagation in any format	2025-11-24 10:51:55 +01:00
Benjamin Jorge	febb62d125	Fix mach/bv.mlw	2025-11-05 11:22:34 +01:00
Claude Marche	d344b75294	fix proofs in subdir numeric ... make them replayed in bench	2025-09-30 13:34:10 +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
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
Jean-Christophe Filliâtre	53b3249062	list.Distinct using a recursive definition	2025-05-14 17:32:28 +02:00
Jean-Christophe Filliatre	c928811d2d	map.MapPermut is a permutation	2025-05-07 23:43:38 +02: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	534bd32d04	Do not introduce program variables for zero and one in int.Int module	2025-03-26 15:17:05 +01:00
Claude Marche	e1d543c06f	SLSE full proof ... generalize hypothesis on size, depending on value of eps	2025-03-10 16:00:09 +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	cabea44347	fix realizations	2024-11-13 19:10:42 +01:00
Guillaume Melquiond	46d53c02a9	Mark some types as having an extensional equality.	2024-11-13 19:04:52 +01:00
Claude Marche	c000797178	Additional operators for fmaps	2024-11-08 10:15:33 +01:00
MARCHE Claude	5ced5ae2b7	Adding a function from_real in the theory of IEEE floats	2024-11-03 21:13:10 +01:00
MARCHE Claude	6ce01d8b7e	Resolve "provide axioms for sdiv and smod in theory bitvector theory"	2024-11-02 08:36:31 +01:00