59 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
Guillaume Melquiond	35601b77e7	Switch to zarith (fix #298).	2024-11-08 22:05:42 +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
MARCHE Claude	85916f62c6	never encode enums and records for Alt-Ergo	2024-05-22 12:18:37 +02:00
Loïc Correnson	e2afddb11d	Resolve "Add injectivity for type invariant"	2024-01-31 13:02:13 +00: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
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
Andrei Paskevich	fe3bf96cd1	stdlib: proper postcondition for (=) on bounded integers	2023-06-17 00:16:27 +00: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
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	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	bcfef9818c	Resolve "Fix drivers for SMT-LIB strings"	2022-04-06 14:29:41 +00:00
Claude Marche	e7efe033be	fix sessions	2021-10-30 11:11:24 +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	d2fb0befca	examples: recompute broken v6 shapes	2020-08-26 19:32:11 +02:00
Cláudio Belo Lourenço	c05d96a102	minor cosmetic fix base64 example	2020-07-28 15:05:45 +02:00