39 Commits

Author	SHA1	Message	Date
Claude Marche	ef62a72810	more upgraded sessions	2025-12-09 10:43:49 +01:00
Jean-Christophe Filliatre	500312de2a	minimum excludant example ... added two other implementations: a naive quadratic scan, and a version where we assume the array to be sorted	2025-02-01 21:22:20 +01:00
Matteo Manighetti	7ae65be566	Upgrade sessions to use Alt-Ergo 2.6.0	2025-01-14 19:48:35 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
Jean-Christophe Filliatre	9c4224a603	improve mex example ... simplified code better variant, to prove the linear complexity	2024-01-29 12:11:27 +01:00
Jacques-Henri Jourdan	28369ea1c3	Fix sessions for nightly bench.	2023-10-22 15:49:03 +02:00
Matteo Manighetti	bd4beefa5c	Upgrade Z3 proofs	2023-08-28 14:29:51 +02:00
Claude Marche	9451890c1f	updated sessions	2023-08-24 16:29:59 +02:00
BONNOT Paul	29c71dbd51	add a meta to mark a symbol as never removed by remove_unused* ... mark some lemmas on division of real as removable if not needed	2023-06-15 15:18:48 +00:00
MARCHE Claude	715fa89d16	separate transformations for intros, dequant, and remove_unused ... remove unused before reflection transformation avoid subst to a unused symbol	2023-04-25 12:20:08 +00:00
Xavier Denis	87af5d805b	Initial bulk upgrade of z3	2023-04-13 09:43:18 +00:00
MARCHE Claude	2f66628fa8	upgrade proofs with Z3 4.6.0 to 4.7.1	2023-04-07 09:37:36 +00:00
Claude Marche	75f8a9584a	update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible	2023-04-05 13:48:22 +02:00
Claude Marche	db96723fd9	fix sessions	2022-07-07 15:49:23 +02:00
Claude Marche	ecb497d98a	Merge branch 'master' into eliminate_unused_symbols	2022-06-23 07:51:51 +02:00
Claude Marche	33115df1c9	fix sessions	2022-06-22 15:39:14 +02:00
Claude Marche	33dad25066	fix proofs	2022-06-02 17:14:50 +02:00
Nightly Build	9e5eb47599	Vc: keep sp_if's splittable (and update sessions)	2022-05-02 18:29:28 +02:00
MARCHE Claude	c6f793011c	introduce_premises also "dequant" the let-ins	2022-04-21 16:23:20 +00:00
Claude Marche	62e1037ff1	fix sessions	2021-09-03 11:59:11 +02:00
Claude Marche	62d925e898	fix sessions	2021-06-25 10:26:57 +02:00
benedikt becker	a5e42659e9	Update sessions and proofs	2021-01-15 15:02:37 +01:00
Guillaume Melquiond	dada254134	Update sessions.	2020-02-11 23:47:40 +01:00
Cláudio Belo Lourenço	a931ddb5a5	Sessions updated. ... In most cases the proof in CVC4 takes one step more than before due to the why3 string built-in type. In a few cases the proof was updated.	2019-10-29 22:37:11 +01:00
Sylvain Dailler	336a478250	Update session, ce-bench and coq files for "VC" -> "vc" in goal name	2019-10-11 21:01:43 +02:00