Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit f2f1007c authored by Martin Clochard's avatar Martin Clochard

Repairing few sessions

parent 698ca990
......@@ -3,8 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="30" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="0"/>
<file name="../max_matrix.mlw" expanded="true">
<theory name="Bitset">
</theory>
......@@ -14,32 +15,32 @@
<goal name="sum_ind" sum="72dcb2e9ca4de20e5648d8fb72d105f5">
<proof prover="1" timelimit="47" memlimit="0"><result status="valid" time="0.79"/></proof>
</goal>
<goal name="WP_parameter maximum" expl="VC for maximum" sum="f22543c872116d927c2201277a727afd" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter maximum" expl="VC for maximum" sum="f22543c872116d927c2201277a727afd">
<transf name="split_goal">
<goal name="WP_parameter maximum.1" expl="1. postcondition" sum="eff3b319c05aad4c355a3c62af2890a7">
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter maximum.2" expl="2. assertion" sum="35f6e7612b31bbac7f101d3dd846c581">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maximum.3" expl="3. postcondition" sum="dcff9bc175d0ecb53acb4fe822caceba">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maximum.4" expl="4. loop invariant init" sum="2737fabf304f248970e1280b0f3a1f5f">
<proof prover="1" timelimit="5"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter maximum.5" expl="5. variant decrease" sum="a25a9622298fac2022deffda7145f025">
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter maximum.6" expl="6. precondition" sum="5cb8487f9c298124bca36b65712f266c">
<proof prover="1" timelimit="5"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter maximum.7" expl="7. loop invariant preservation" sum="8e04971d54fa8f535f92677081ca000d" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter maximum.7.1" expl="1." sum="d1a92fe069b817bcd03b2d53d722107e" expanded="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter maximum.7" expl="7. loop invariant preservation" sum="8e04971d54fa8f535f92677081ca000d">
<transf name="split_goal_wp">
<goal name="WP_parameter maximum.7.1" expl="1." sum="d1a92fe069b817bcd03b2d53d722107e">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maximum.7.2" expl="2." sum="c7001f0950113485024a198ff29a469a" expanded="true">
<goal name="WP_parameter maximum.7.2" expl="2." sum="c7001f0950113485024a198ff29a469a">
<proof prover="2"><result status="valid" time="2.26"/></proof>
</goal>
</transf>
......@@ -48,90 +49,90 @@
<proof prover="0"><result status="valid" time="5.66"/></proof>
</goal>
<goal name="WP_parameter maximum.9" expl="9. loop invariant preservation" sum="45f07f510356497d6d1617e7fead834e">
<proof prover="1" timelimit="5"><result status="valid" time="0.30"/></proof>
<proof prover="1"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter maximum.10" expl="10. assertion" sum="b01070ab689a0beaba10a1c8df4fc9db">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maximum.11" expl="11. postcondition" sum="8ace4d2d8dab412cb4d6f6bcf980d38b">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter memo" expl="VC for memo" sum="e69785457a3b690b43a6cc4c9feb1754">
<transf name="split_goal">
<goal name="WP_parameter memo.1" expl="1. postcondition" sum="36eff218ba65ab6a10cf2d9ce55bfd13">
<transf name="split_goal">
<goal name="WP_parameter memo.1.1" expl="1." sum="b3e6409800e6b568c5bc8572d1bc474b">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter memo" expl="VC for memo" sum="f2ee11d5ee3eb331d270a29d6b7c968c" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter memo.1" expl="1. postcondition" sum="36eff218ba65ab6a10cf2d9ce55bfd13" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter memo.1.1" expl="1." sum="b3e6409800e6b568c5bc8572d1bc474b" expanded="true">
<proof prover="3" timelimit="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter memo.1.2" expl="2." sum="893149a2745668d1094e504281e32ac6">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="30" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter memo.2" expl="2. variant decrease" sum="d0fc421f038668a72f9e79c58ec70f27">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter memo.3" expl="3. precondition" sum="e1888765076b3353d0a551ac739580c0">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<proof prover="1" timelimit="30" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter memo.4" expl="4. postcondition" sum="b57c9888a6489a3bea81cb1b27c08d8d">
<proof prover="1" memlimit="0"><result status="valid" time="0.04"/></proof>
<goal name="WP_parameter memo.4" expl="4. postcondition" sum="136858d31a79c5abc734e4a6eb9178cf">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxmat" expl="VC for maxmat" sum="f7e7d1664480178f5035ce283b5f08ee" expanded="true">
<transf name="split_goal" expanded="true">
<goal name="WP_parameter maxmat.1" expl="1. assertion" sum="a3e78cc7a711857c1ca6118ecb05ec73">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.1.1" expl="1. assertion" sum="95798f370c76ff52b7cbb2afdfbc8892">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
<goal name="WP_parameter maxmat" expl="VC for maxmat" sum="4cf0a2699674f2b653a6165cb92893a0">
<transf name="split_goal">
<goal name="WP_parameter maxmat.1" expl="1. assertion" sum="cc95d36933d8b60c09248b39c3ac7e6f">
<proof prover="3" timelimit="5" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.2" expl="2. precondition" sum="91a3b3f8f2706e79aa4ed9219e85c235">
<goal name="WP_parameter maxmat.2" expl="2. precondition" sum="f328fdf40c77e56b4e5d95f7777bc61c">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.2.1" expl="1. precondition" sum="45ca61447705e7bfac1e5f21739b1443">
<goal name="WP_parameter maxmat.2.1" expl="1. precondition" sum="f967594a259f30d76c771db89f4b5c55">
<transf name="split_goal">
<goal name="WP_parameter maxmat.2.1.1" expl="1." sum="4d4a4911a08d09e5147f34ca92ebfcb7">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter maxmat.2.1.1" expl="1." sum="7d6abbf17efc40ab0105779b37db119b">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.2" expl="2." sum="02b10069320889e13f7a2bc190e8d49a">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter maxmat.2.1.2" expl="2." sum="904744a3d7b39082be137b250ba8113f">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.3" expl="3." sum="f648ace5ed0b97d9e87bbe7a72f84646">
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter maxmat.2.1.3" expl="3." sum="9debaac4bac5d74d951bc2c52433ed06">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.4" expl="4." sum="9b0fb75c575eccd82a2530de28a7e0d6">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter maxmat.2.1.4" expl="4." sum="75a0cb578a4ddf4cc33577416a1815aa">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.5" expl="5." sum="ef2a4dd2da12eca06c248eb0a862d561">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter maxmat.2.1.5" expl="5." sum="011a825dd218743761d37082d7e12122">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.6" expl="6." sum="f3797a30aad278bec33e1bb829a3d0c2">
<proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter maxmat.2.1.6" expl="6." sum="d034de90b7624c1353da4a7e7d416553">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxmat.3" expl="3. postcondition" sum="14dda238b684d40e85a0be220dd1dc62">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter maxmat.4" expl="4. postcondition" sum="c6e85a18323b3ed4a23a777e0655bfff">
<goal name="WP_parameter maxmat.3" expl="3. postcondition" sum="839797288e675333811cdf9b006a953a">
<transf name="split_goal">
<goal name="WP_parameter maxmat.4.1" expl="1. postcondition" sum="c6e85a18323b3ed4a23a777e0655bfff">
<goal name="WP_parameter maxmat.3.1" expl="1. postcondition" sum="839797288e675333811cdf9b006a953a">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.4.1.1" expl="1. postcondition" sum="2cff3fcd600ccbfea9b97a8de419b917">
<proof prover="1" memlimit="0"><result status="valid" time="0.10"/></proof>
<goal name="WP_parameter maxmat.3.1.1" expl="1. postcondition" sum="40ce3e55c28b9f38685e6e2cfcfdcb3d">
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxmat.4" expl="4. postcondition" sum="5ec57f54b78889f0e646c89bdcc2d9ce">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.4.1" expl="1. postcondition" sum="a3e4bdd4a21d9a506b7af2c183947611">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
......
......@@ -6,11 +6,11 @@
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="20" memlimit="0"/>
<prover id="2" name="Z3" version="3.2" timelimit="8" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl3" timelimit="20" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="0"/>
<file name="../vstte10_queens.mlw" expanded="true">
<theory name="NQueens" expanded="true">
<goal name="eq_board_set" sum="e90922715e479af636c8b75d1bca5bf5" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="eq_board_sym" sum="637819644163011d3643168b993182c1" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -31,14 +31,14 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3" edited="vstte10_queens_NQueens_solution_eq_board_1.v"><result status="valid" time="1.31"/></proof>
</goal>
<goal name="WP_parameter bt_queens" expl="VC for bt_queens" sum="77d4d232822bacc03aba77962a5ccaad" expanded="true">
<goal name="WP_parameter bt_queens" expl="VC for bt_queens" sum="ad2b322585e35d80d2c78c57e19b433c" expanded="true">
<proof prover="0"><result status="valid" time="1.22"/></proof>
</goal>
<goal name="WP_parameter queens" expl="VC for queens" sum="be9085123de1cfc77f45a330f2c2e3c0" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter queens" expl="VC for queens" sum="d0355b23d34bacd346b20ac1c8363015" expanded="true">
<proof prover="4" timelimit="20"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter test8" expl="VC for test8" sum="82a42a4c395dd56dc217087f030da199" expanded="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
......
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