14 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
MARCHE Claude	174c9a01f5	do not allow implicit inference of partial	2024-10-31 15:27:09 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
Jacques-Henri Jourdan	1b9ff7667a	Fix session timings on moloch	2023-10-23 09:18:45 +02:00
Jacques-Henri Jourdan	28369ea1c3	Fix sessions for nightly bench.	2023-10-22 15:49:03 +02:00
BONNOT Paul	2444f6c60a	Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.	2023-09-07 18:05:01 +00:00
BONNOT Paul	617b6db4e6	Resolve "Remove axioms in Z3 and CVC4 drivers"	2023-09-01 15:47:33 +00: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
Matteo Manighetti	6bf507f32d	upgrade bench scripts with CVC5 from 1.0.0 to 1.0.5, upgrade sessions	2023-07-11 15:13:50 +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
Jean-Christophe Filliatre	110fc6f4d5	space-saving example: general case	2023-05-10 20:34:28 +02:00
Jean-Christophe Filliatre	458db577d6	space-saving example: better use map instead of seq	2023-05-10 11:20:26 +02:00
Jean-Christophe Filliatre	d350e39fd2	new example: space saving algorithm	2023-05-09 15:54:05 +02:00