Commit 799d6987 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 27512907
Pipeline #12167 failed with stage
in 2 minutes and 59 seconds
......@@ -3,7 +3,6 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -29,7 +28,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="steps_non_neg" proved="true">
<proof prover="1" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="4" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.31"/></proof>
</goal>
</theory>
<theory name="TestSemantics" proved="true" sum="dd8bb0c0f827d977f4ca0784ddce1af8">
......@@ -101,7 +100,7 @@
<proof prover="0"><result status="valid" time="0.06" steps="205"/></proof>
</goal>
<goal name="eval_type_term.0.3" proved="true">
<proof prover="1" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="4" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="0.38"/></proof>
</goal>
</transf>
</goal>
......@@ -215,7 +214,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="eval_swap_term.0.1" proved="true">
<proof prover="1" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="0.93"/></proof>
<proof prover="4" edited="blocking_semantics5_FreshVariables_eval_swap_term_1.v"><result status="valid" time="0.93"/></proof>
</goal>
<goal name="eval_swap_term.0.2" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
......@@ -361,10 +360,10 @@
<goal name="many_steps_seq">
<proof prover="4" edited="blocking_semantics5_HoareLogic_many_steps_seq_1.v"><result status="unknown" time="0.91"/></proof>
<transf name="induction" arg1="n">
<goal name="many_steps_seq.0" proved="true">
<goal name="many_steps_seq.0" expl="base case" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="many_steps_seq.1">
<goal name="many_steps_seq.1" expl="recursive case">
</goal>
</transf>
</goal>
......@@ -427,7 +426,7 @@
<proof prover="0"><result status="valid" time="0.34" steps="1384"/></proof>
</goal>
<goal name="while_rule" proved="true">
<proof prover="1" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="4" edited="blocking_semantics5_HoareLogic_while_rule_1.v"><result status="valid" time="0.46"/></proof>
</goal>
</theory>
<theory name="WP" sum="6d31ca24f5b34970df8292d003018d4a">
......@@ -483,7 +482,7 @@
<proof prover="3"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="monotonicity.0.5" proved="true">
<proof prover="1" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="0.40"/></proof>
<proof prover="4" edited="blocking_semantics5_WP_monotonicity_3.v"><result status="valid" time="0.40"/></proof>
</goal>
</transf>
</goal>
......@@ -509,7 +508,7 @@
<proof prover="0"><result status="valid" time="0.04" steps="175"/></proof>
</goal>
<goal name="distrib_conj.0.5" proved="true">
<proof prover="1" edited="blocking_semantics5_WP_distrib_conj_3.v"><result status="valid" time="0.63"/></proof>
<proof prover="4" edited="blocking_semantics5_WP_distrib_conj_3.v"><result status="valid" time="0.63"/></proof>
</goal>
</transf>
</goal>
......@@ -526,35 +525,35 @@
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="progress.0.1" proved="true">
<proof prover="1" edited="blocking_semantics5_WP_progress_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="4" edited="blocking_semantics5_WP_progress_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="10"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="progress.0.2">
<proof prover="4" edited="blocking_semantics5_WP_progress_2.v"><result status="unknown" time="0.67"/></proof>
<transf name="case" arg1="(x1 = Sskip)">
<goal name="progress.0.2.0" proved="true">
<goal name="progress.0.2.0" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="progress.0.2.1">
<goal name="progress.0.2.1" expl="false case">
</goal>
</transf>
</goal>
<goal name="progress.0.3" proved="true">
<proof prover="1" edited="blocking_semantics5_WP_progress_3.v"><result status="valid" time="0.35"/></proof>
<proof prover="4" edited="blocking_semantics5_WP_progress_3.v"><result status="valid" time="0.35"/></proof>
<proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="3.91"/></proof>
</goal>
<goal name="progress.0.4" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="179"/></proof>
</goal>
<goal name="progress.0.5" proved="true">
<proof prover="1" edited="blocking_semantics5_WP_progress_5.v"><result status="valid" time="0.39"/></proof>
<proof prover="4" edited="blocking_semantics5_WP_progress_5.v"><result status="valid" time="0.39"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="wp_soundness" proved="true">
<proof prover="1" timelimit="30" edited="blocking_semantics5_WP_wp_soundness_1.v"><result status="valid" time="0.44"/></proof>
<proof prover="4" timelimit="30" edited="blocking_semantics5_WP_wp_soundness_1.v"><result status="valid" time="0.44"/></proof>
</goal>
</theory>
</file>
......
......@@ -14,7 +14,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="0dff6db6a97904cd70ecb8a6e2b35ea3">
<theory name="BinarySearchInt32" proved="true" sum="909f26be7787adc1464e7f847a908692">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="2.53" steps="3682"/></proof>
</goal>
......
......@@ -14,7 +14,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="6b53bfa0cd2753aea9e2ff848afc0c27">
<theory name="BinarySearchInt32" proved="true" sum="c9f0cf881df8be787d964ba3de51306f">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......
......@@ -9,7 +9,7 @@
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../bitcount.mlw" proved="true">
<theory name="BitCount8bit_fact" proved="true" sum="6b90b77a59ff933245169afa6731e6bb">
<theory name="BitCount8bit_fact" proved="true" sum="efb7c951014c6f701cd5a5b6603d09fd">
<goal name="nth_as_bv_is_int" proved="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.16" steps="166"/></proof>
......@@ -234,7 +234,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" proved="true" sum="725e90b8e5b2c3ca7b0b24d4d76a67b6">
<theory name="BitCounting32" proved="true" sum="36a25c3680ec5f18a9c1df70600fed22">
<goal name="VC proof0" expl="VC for proof0" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC proof0.0" expl="assertion" proved="true">
......@@ -427,7 +427,7 @@
<proof prover="1"><result status="valid" time="0.03" steps="92"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="93"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="0.78"/></proof>
<proof prover="5"><result status="valid" time="0.44"/></proof>
</goal>
</transf>
</goal>
......@@ -525,7 +525,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="96"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="97"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="5"><result status="valid" time="1.87"/></proof>
<proof prover="5"><result status="valid" time="4.72"/></proof>
</goal>
<goal name="VC proof3.11.1" expl="VC for proof3" proved="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
......@@ -535,7 +535,7 @@
<proof prover="1"><result status="valid" time="0.03" steps="95"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="96"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="1.56"/></proof>
<proof prover="5"><result status="valid" time="3.61"/></proof>
</goal>
</transf>
</goal>
......@@ -700,7 +700,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" proved="true" sum="ca006a2107fa925dac932da06dafcb56">
<theory name="Hamming" proved="true" sum="37fb69ba48c96019a185e0ef310cb658">
<goal name="VC hammingD" expl="VC for hammingD" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC hammingD.0" expl="assertion" proved="true">
......@@ -788,7 +788,7 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="AsciiCode" proved="true" sum="cb04e28ca4735541679a76ab10890ca5">
<theory name="AsciiCode" proved="true" sum="8984a858936e4964cb9643d8ffed3278">
<goal name="VC bv_even" expl="VC for bv_even" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bv_even.0" expl="assertion" proved="true">
......@@ -806,7 +806,7 @@
<goal name="VC bv_even.3" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bv_even.3.0" expl="VC for bv_even" proved="true">
<proof prover="3"><result status="valid" time="1.33" steps="1341"/></proof>
<proof prover="3"><result status="valid" time="1.08" steps="933"/></proof>
</goal>
<goal name="VC bv_even.3.1" expl="VC for bv_even" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="142"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitvector_examples.mlw" proved="true">
<theory name="Test_proofinuse" proved="true" sum="0c229b80848632134a0bf56a9a516ce1">
<theory name="Test_proofinuse" proved="true" sum="b381d834e5c277f8dc05bdae8b299c46">
<goal name="VC shift_is_div" expl="VC for shift_is_div" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="117"/></proof>
</goal>
......@@ -19,7 +19,7 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" proved="true" sum="089ee73f758849907670684f19fd2329">
<theory name="Hackers_delight" proved="true" sum="ea80e954b2ac9a9c9c2507b43d5e6d9e">
<goal name="DM1" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -78,7 +78,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" proved="true" sum="47481ccbf7e19da7ad2d451a09af1da3">
<theory name="Hackers_delight_mod" proved="true" sum="46acd1921636538bca64c517d7e2c03e">
<goal name="VC dm1" expl="VC for dm1" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -130,7 +130,7 @@
<goal name="VC bp1" expl="VC for bp1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC bp1&apos;" expl="VC for bp1'" proved="true">
<goal name="VC bp1&#39;" expl="VC for bp1'" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC bp2" expl="VC for bp2" proved="true">
......@@ -140,7 +140,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" proved="true" sum="82e83dd69d448ddd1c4871cb2ea904c7">
<theory name="Test_imperial_violet" proved="true" sum="4e2bdcbea51830917c9997009c023511">
<goal name="bv32_bounds_bv" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -180,7 +180,7 @@
<proof prover="3"><result status="valid" time="0.02" steps="137"/></proof>
</goal>
<goal name="VC add.7" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.36" steps="2809"/></proof>
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.36" steps="2919"/></proof>
</goal>
<goal name="VC add.8" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......@@ -191,7 +191,7 @@
</transf>
</goal>
</theory>
<theory name="Test_from_bitvector_example" proved="true" sum="6469533d7f0f17a11454be11d4f2f604">
<theory name="Test_from_bitvector_example" proved="true" sum="bd327798169780f33626a580402507fe">
<goal name="Test1" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="11" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bitwalker.mlw" proved="true">
<theory name="Bitwalker" proved="true" sum="95b868ec6211afe981272221e196a33f">
<theory name="Bitwalker" proved="true" sum="0efcbd982faa8c64c2d86689d8f43c03">
<goal name="nth64" proved="true">
<proof prover="10"><result status="valid" time="0.02" steps="91"/></proof>
</goal>
......@@ -188,7 +188,7 @@
<proof prover="12"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC peek_64bit.3" expl="postcondition" proved="true">
<proof prover="11"><result status="valid" time="0.18"/></proof>
<proof prover="11"><result status="valid" time="0.41"/></proof>
</goal>
</transf>
</goal>
......@@ -264,7 +264,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.5" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.6" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
......@@ -279,7 +279,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.10" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.11" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../15_destruct_alg.mlw">
<theory name="Issue15" sum="e66dc991ed1c7476749af7ab45982f63">
<theory name="Issue15" sum="0413eaf885c11105096ec062b84ee4c1">
<goal name="g">
<transf name="destruct_alg" arg1="l">
<goal name="g.0">
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../33_reload_trans.mlw">
<theory name="T" sum="f6c01df1ed5265da509017649b093f5e">
<theory name="T" sum="741527cb712ca9e6bb5919aef55b3c53">
<goal name="G">
<transf name="assert" arg1="(1 = 1)">
<goal name="G.0">
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../esterel.mlw" proved="true">
<theory name="Esterel" proved="true" sum="ec76c3c04e3f256382afd9b342d8ce0a">
<theory name="Esterel" proved="true" sum="a9a3281e9c75b754b62ff24704176e72">
<goal name="VC s" expl="VC for s" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../hackers-delight.mlw" proved="true">
<theory name="Utils" proved="true" sum="13023cdacdc7b4ae442516ddb4836ce2">
<theory name="Utils" proved="true" sum="972c3075733fe9f31d38e91fcbaf519e">
<goal name="VC one" expl="VC for one" proved="true">
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -21,7 +21,7 @@
<proof prover="9"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="Utils_Spec" proved="true" sum="6423b7395423f252a88c7b4fcc1e9d4a">
<theory name="Utils_Spec" proved="true" sum="1a44322a4c14c032381964bab04cbb16">
<goal name="countZero" proved="true">
<proof prover="9"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -31,7 +31,7 @@
<goal name="countStep" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="countStep.0" proved="true">
<proof prover="9"><result status="valid" time="1.62"/></proof>
<proof prover="9"><result status="valid" time="1.35"/></proof>
</goal>
<goal name="countStep.1" proved="true">
<proof prover="9"><result status="valid" time="0.08"/></proof>
......@@ -120,7 +120,7 @@
<proof prover="3"><result status="valid" time="0.55" steps="635"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" proved="true" sum="f7afa5432ee0c251fd5b815a72195581">
<theory name="Hackers_delight" proved="true" sum="8e10c18280320677d8bd71ff4ab7a3a7">
<goal name="VC ascii" expl="VC for ascii" proved="true">
<proof prover="9"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -29,7 +29,7 @@
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="Bits" proved="true" sum="674d744870b194a226c3b2fb61cb6825">
<theory name="Bits" proved="true" sum="6c62e04243120c79ca8d250f6d3a2909">
<goal name="VC t" expl="VC for t" proved="true">
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -91,7 +91,7 @@
<proof prover="6"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC rightmost_bit_trick.3" expl="assertion" proved="true">
<proof prover="8"><result status="valid" time="0.42"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC rightmost_bit_trick.4" expl="assertion" proved="true">
<proof prover="4" timelimit="1"><result status="valid" time="0.05" steps="146"/></proof>
......@@ -103,7 +103,7 @@
<proof prover="5"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC rightmost_bit_trick.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.56" steps="426"/></proof>
<proof prover="0"><result status="valid" time="0.56" steps="422"/></proof>
</goal>
<goal name="VC rightmost_bit_trick.8" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -118,7 +118,7 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="NQueensBits" proved="true" sum="141a3e9b2ebf15c61c5e40e8bde5b403">
<theory name="NQueensBits" proved="true" sum="758a7663eed2f4fcd885dbfdc36e417b">
<goal name="VC t" expl="VC for t" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC t.0" expl="assertion" proved="true">
......@@ -302,7 +302,7 @@
</goal>
<goal name="VC t.46.2" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="60"><result status="valid" time="19.94"/></proof>
<proof prover="6" timelimit="60"><result status="valid" time="13.13"/></proof>
<proof prover="6" timelimit="60"><result status="valid" time="15.12"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,7 +6,7 @@
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" proved="true">
<theory name="Rmbt" proved="true" sum="1b2c0471a8d60827baa3f3cce5528735">
<theory name="Rmbt" proved="true" sum="56adb784f9e137dcae55be610e66d665">
<goal name="VC rightmost_position_set" expl="VC for rightmost_position_set" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC rightmost_position_set.0" expl="loop invariant init" proved="true">
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment