15 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
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
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
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
Nightly Build
9e5eb47599 Vc: keep sp_if's splittable (and update sessions) 2022-05-02 18:29:28 +02: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
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
Jean-Christophe Filliatre
c999f70d56 bench of Python/Micro-C files
added sessions for Python examples
2021-07-08 14:45:49 +02:00