43 Commits

Author	SHA1	Message	Date
Claude Marche	5f9169e032	fis sessions	2024-11-16 09:41:34 +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
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
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
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	8abedf035e	fix sessions	2022-06-02 17:59:27 +02:00
MARCHE Claude	c6f793011c	introduce_premises also "dequant" the let-ins	2022-04-21 16:23:20 +00:00
Benedikt Becker	64219c68e9	Fix sessions and update oracles for result variables in VC SP	2021-10-04 15:53:08 +02: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
Andrei Paskevich	f4ca81247d	Repair discriminate2	2021-04-08 12:26:07 +00:00
Guillaume Melquiond	dada254134	Update sessions.	2020-02-11 23:47:40 +01:00
Cláudio Belo Lourenço	b7962ce27d	Avoid CVC4 1.6 instead of CVC4 1.4 noBV	2019-11-04 14:29:20 +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
Sylvain Dailler	32d7cfe8de	Rerun all sessions to update the file formats ... This also updates some of the "VC name" to "name'VC" that were never updated.	2019-09-24 17:58:31 +02:00
DAILLER Sylvain	08857a1e85	Naming of ident: remove space in favor of "'" ... - change prefix "mk " into suffix "'mk" - change prefix "VC " into suffix "'VC"	2019-08-23 14:47:32 +02:00
Sylvain Dailler	1b71ca59c5	Update session and shapes	2019-05-20 17:09:01 +02:00