49 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	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	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
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	2f66628fa8	upgrade proofs with Z3 4.6.0 to 4.7.1	2023-04-07 09:37:36 +00:00
Claude Marche	91a8a26fde	fix obsolete sessions and one failed session	2023-02-07 12:25:21 +01: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
Claude Marche	25b0c47cad	compile_match and eliminate_algebraic now preserve attributes	2022-02-13 11:35:50 +01: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	c67d119b10	fix sessions	2021-07-12 13:26:40 +02:00
Claude Marche	745a2eb3f4	Merge branch 'master' into call-results-for-ce-cleaner ... # Conflicts: # bench/check-ce/oracles/anonymous1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/anonymous2_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous2_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous2_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous2_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/anonymous3_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous3_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous3_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous3_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/anonymous4_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous4_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous4_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous4_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/anonymous5_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous5_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous5_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous5_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/anonymous6_CVC4,1.7_SP.oracle # bench/check-ce/oracles/anonymous6_CVC4,1.7_WP.oracle # bench/check-ce/oracles/anonymous6_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/anonymous6_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/falseCE_CVC4,1.7_SP.oracle # bench/check-ce/oracles/falseCE_CVC4,1.7_WP.oracle # bench/check-ce/oracles/falseCE_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/falseCE_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/for1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/for1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/for1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/for1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/for_CVC4,1.7_SP.oracle # bench/check-ce/oracles/for_CVC4,1.7_WP.oracle # bench/check-ce/oracles/for_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/for_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call2_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call2_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call2_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call2_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call3_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call3_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call3_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call3_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call4_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call4_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call4_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call4_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call5_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call5_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call5_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call5_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call6_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call6_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call6_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call6_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/func_call_CVC4,1.7_SP.oracle # bench/check-ce/oracles/func_call_CVC4,1.7_WP.oracle # bench/check-ce/oracles/func_call_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/func_call_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/global_logic_constant_CVC4,1.7_SP.oracle # bench/check-ce/oracles/global_logic_constant_CVC4,1.7_WP.oracle # bench/check-ce/oracles/global_logic_constant_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/global_logic_constant_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/jlamp0_CVC4,1.7_SP.oracle # bench/check-ce/oracles/jlamp0_CVC4,1.7_WP.oracle # bench/check-ce/oracles/jlamp0_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/jlamp0_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/multifile1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/multifile1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/multifile2_CVC4,1.7_SP.oracle # bench/check-ce/oracles/multifile2_CVC4,1.7_WP.oracle # bench/check-ce/oracles/multifile2_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/multifile2_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/ref1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/ref1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/ref1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/ref1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/ref2_CVC4,1.7_SP.oracle # bench/check-ce/oracles/ref2_CVC4,1.7_WP.oracle # bench/check-ce/oracles/ref2_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/ref2_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/tuple1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/tuple1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/tuple1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/tuple1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/tuple_CVC4,1.7_SP.oracle # bench/check-ce/oracles/tuple_CVC4,1.7_WP.oracle # bench/check-ce/oracles/tuple_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/underspec_CVC4,1.7_SP.oracle # bench/check-ce/oracles/underspec_CVC4,1.7_WP.oracle # bench/check-ce/oracles/underspec_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/underspec_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/var_clones_CVC4,1.7_SP.oracle # bench/check-ce/oracles/var_clones_CVC4,1.7_WP.oracle # bench/check-ce/oracles/var_clones_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/var_clones_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/while1_CVC4,1.7_SP.oracle # bench/check-ce/oracles/while1_CVC4,1.7_WP.oracle # bench/check-ce/oracles/while1_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/while1_Z3,4.8.4_WP.oracle # bench/check-ce/oracles/while_CVC4,1.7_SP.oracle # bench/check-ce/oracles/while_CVC4,1.7_WP.oracle # bench/check-ce/oracles/while_Z3,4.8.4_SP.oracle # bench/check-ce/oracles/while_Z3,4.8.4_WP.oracle # examples/prover/FormulaTransformations/why3session.xml # examples/prover/FormulaTransformations/why3shapes.gz # examples/prover/Prover/why3session.xml # examples/prover/Prover/why3shapes.gz # examples/prover/ProverMain/why3shapes.gz # examples/prover/ProverTest/why3shapes.gz # examples/python/dicho/why3session.xml # examples/python/dicho/why3shapes.gz # examples/python/fact/why3shapes.gz # examples/python/isqrt/why3shapes.gz # examples/python/isqrt_fun/why3shapes.gz # examples/python/mult/why3shapes.gz # examples/python/nim/why3shapes.gz # examples/python/pgcd/why3shapes.gz # examples/python/sort/why3session.xml # examples/python/sort/why3shapes.gz # examples/python/triangular/why3shapes.gz # examples/verifythis_2016_tree_traversal/why3session.xml # examples/verifythis_2016_tree_traversal/why3shapes.gz	2021-07-12 11:05:29 +02:00
Quentin Garchery	2966bb7ee2	fix obsolete sessions	2021-06-30 10:37:36 +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