112 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	4d04b4f698	add metas for unused-dependencies on sequences ... also fix split_full that was losing metas for unused dependency	2024-10-29 16:12:46 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
Jean-Christophe Filliatre	fab3de34b1	gallery: a small result about Fibonacci numbers	2024-10-16 10:48:25 +02:00
Jacques-Henri Jourdan	1b9ff7667a	Fix session timings on moloch	2023-10-23 09:18:45 +02:00
BONNOT Paul	2444f6c60a	Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.	2023-09-07 18:05:01 +00:00
Matteo Manighetti	d31c53d53c	Move CVC4 proofs to CVC5	2023-08-28 14:31:08 +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
MARCHE Claude	2f66628fa8	upgrade proofs with Z3 4.6.0 to 4.7.1	2023-04-07 09:37:36 +00:00
Jacques-Henri Jourdan	a24e70ed0c	Fix sessions.	2023-01-31 01:50:53 +01:00
David Ewert	5f54fca95f	Add "remove_unused:dependency" to int.ComputerDivision	2022-09-21 20:15:46 +00:00
Claude Marche	3d6f0636b0	fix sessions	2022-07-30 11:40:25 +02:00
MARCHE Claude	bec4f19215	Resolve "z3 driver should not unfold definitions"	2022-07-09 09:12:15 +00: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	3a42b3fed2	fix proof	2022-06-02 17:36:45 +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	e7efe033be	fix sessions	2021-10-30 11:11:24 +02:00
Quentin Garchery	b0965805f9	simplifies fib tail rec proof and add counterexample to regalloc as a comment	2021-09-16 16:33:30 +02:00
Quentin Garchery	35b0899eca	tail rec fibonacci example	2021-09-15 17:51:33 +02:00