17 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
Claude Marche	2e1d53f51b	fix sessions and CE oracles	2024-11-14 14:48:30 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
Loïc Correnson	e2afddb11d	Resolve "Add injectivity for type invariant"	2024-01-31 13:02:13 +00:00
Jacques-Henri Jourdan	28369ea1c3	Fix sessions for nightly bench.	2023-10-22 15:49:03 +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
David Ewert	5f54fca95f	Add "remove_unused:dependency" to int.ComputerDivision	2022-09-21 20:15:46 +00:00
Claude Marche	db96723fd9	fix sessions	2022-07-07 15:49:23 +02:00
Claude Marche	33115df1c9	fix sessions	2022-06-22 15:39:14 +02:00
Claude Marche	62e1037ff1	fix sessions	2021-09-03 11:59:11 +02:00
Claude Marche	e449b99c44	fix sessions	2021-06-25 14:15:38 +02:00
Claude Marche	62d925e898	fix sessions	2021-06-25 10:26:57 +02:00
Andrei Paskevich	a28847b073	examples/wrap_lines: extended challenge	2021-03-27 19:48:42 +01:00
Jean-Christophe Filliatre	634119aba2	new example: wrap_lines ... micro challenge proposed by Mattias Ulbrich at VerifyThis 2021	2021-03-27 13:39:59 +01:00