29 Commits

Author	SHA1	Message	Date
David Ewert	5f54fca95f	Add "remove_unused:dependency" to int.ComputerDivision	2022-09-21 20:15:46 +00:00
Guillaume Melquiond	4d2d1c7183	Merge branch 'bugfix/v1.5'	2022-09-12 20:04:13 +02:00
Jean-Christophe Filliatre	f95a5214f6	fixed Python example and proof session	2022-09-09 14:56:11 +02:00
Jean-Christophe Filliatre	c891d2b87f	updated proof sessions	2022-09-08 16:00:29 +02: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
MARCHE Claude	c6f793011c	introduce_premises also "dequant" the let-ins	2022-04-21 16:23:20 +00:00
Jean-Christophe Filliatre	f31498beda	fixed Python lexer ... empty comment lines were not accepted by the lexer	2021-12-09 08:48:51 +01:00
Jean-Christophe Filliatre	6efdd5c9d5	micro-Python: new example	2021-12-06 10:34:17 +01:00
Claude Marche	e7efe033be	fix sessions	2021-10-30 11:11:24 +02:00
Jean-Christophe Filliatre	08712c15ac	micro-Python: added support for built-in function pow	2021-10-29 15:57:14 +02:00
Jean-Christophe Filliatre	d517234610	micro Python: type annotations in programs	2021-09-24 18:27:07 +02:00
Jean-Christophe Filliatre	cd46b54253	micrp Python: more types	2021-09-24 18:14:59 +02:00
Claude Marche	62e1037ff1	fix sessions	2021-09-03 11:59:11 +02:00
Claude Marche	cec915c4f1	fix obsolete sessions	2021-08-24 09:26:20 +02:00
MARCHE Claude	9c90a59ae3	Merge branch 'call-results-for-ce-cleaner' into 'master' ... Keep a logic variable for the result of the function calls See merge request why3/why3!561	2021-07-12 13:01:07 +00:00
Claude Marche	9674c541d7	fix session	2021-07-12 14:24:52 +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
Jean-Christophe Filliâtre	6b427d7458	Merge branch 'internship-2021-LMF' into 'master' ... TryWhy3: All in one See merge request why3/why3!553	2021-07-08 13:42:09 +00:00
Jean-Christophe Filliatre	c999f70d56	bench of Python/Micro-C files ... added sessions for Python examples	2021-07-08 14:45:49 +02:00
Quentin Garchery	2966bb7ee2	fix obsolete sessions	2021-06-30 10:37:36 +02:00